Architecture of the Formally-Verified Distributed Ledger System InnoChain
https://doi.org/10.18255/1818-1015-2020-4-472-487
Abstract
In this paper we consider the software architecture of InnoChain, a distributed ledger system (DLS) with 5 levels of formal verification, including a formally-verified underlying operating system (OS). The objective of this architecture is to achieve a higher level of DLS dependability compared to more traditional software architectures and quality assurance (QA) methods. The architecture of InnoChain includes (1) a programming language for smart contracts which is a domain-specific language with formal semantics embedded into CakeML, which is a functional language ofthe ML family; this allows us to carry out formal verification of smart contracts' correctness properties using higher-order logic systems, such as HOL4; (2) trusted compilation of smart contracts into the machine code using the verified compiler available for CakeML, rather than relying on a virtual machine for execution of smart contracts; (3) using CakeML for implementation of InnoChain node functionality which allows for formal verification of code correctness and trusted compilation into the machine code; (4) formal verification of the consensus protocol used InnoChain, namely HotStuff BFT; (5) using seL4, a formally-verified microkernel, as the underlying OS for InnoChain instead of more traditional general-purpose OSes such as Linux. The proposed verified architecture will allow InnoChain to be used in mission-critical applications, such as the decentralized Aircraft Fuelling Control System which is currently under development for JSC Aeroflot, the Russian national air carrier.
Supporting agencies: Ministry of Digital Development, Communications and Mass Media of the Russian Federation and Russian Venture Company (Agreement No. 004/20 dd. 20.03.2020, IGK 0000000007119P190002).
About the Authors
Leonid Al'bertovich Merkin-Janson
Innopolis University
Russian Federation
Russian Federation
Professor, Doctor of Mathematics, Delft University of Technology, Dr.
Ruslan Maratovich Rezin
Innopolis University
Russian Federation
Russian Federation
Head expert in formal verification methods at Innopolis University, Master degree in Computer Science, MSc.
Nikolay Konstantinovich Vasilyev
Innopolis University; National Research University Higher School of Economics
Russian Federation
Russian Federation
Lead Developer.
References
1. A. Burns and A. Wellings, Concurrent and Real-Time Programming in Ada 2005. Cambridge University Press, 2007.
2. A. Burns and A. Wellings, Real-Time Systems and Programming Languages. Addison-Wesley, 2009.
3. Smart Contracts Under Control, 2020. [Online]. Available: https://archetype-lang.org.
4. More Ethereum Attacks: Race-To-Empty is the Real Deal, 2016. [Online]. Available: https://vessenes.com/more-ethereum-attacks-race-to-empty-is-the-real-deal.
5. CakeML: A verified implementation of ML, 2020. [Online]. Available: https://cakeml.org.
6. M. Yin, D. Malkhi, M. K. Reiter, G. G. Gueta, and I. Abraham, «HotStuff: BFT Consensus with Linearity and Responsiveness», in PODC, ACM, 2019, pp. 347-356.
7. G. Heiser, The seL4 Microkernel: An Introduction, 2020. [Online]. Available: https://sel4.systems/About/seL4-whitepaper.pdf .
8. Libra by Facebook. [Online]. Available: https://github.com/libra/libra.
9. S. Owens, M. O. Myreen, R. Kumar, and Y. K. Tan, «Functional Big-step Semantics», in Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, P. Thiemann, Ed., ser. Lecture Notes in Computer Science, vol. 9632, Springer, Apr. 2016, pp. 589-615. doi: 10.1007/978-3-662-49498-1“_23.
10. T. Gauthier, C. Kaliszyk, and J. Urban, «TacticToe: Learning to Reason with HOL4 Tactics», in LPAR, ser. EPiC Series in Computing, vol. 46, EasyChair, 2017, pp. 125-143.
11. C. Baier and J.-P. Katoen, Principles of Model Checking. MIT Press, 2008.
12. J. A. Pohjola, H. Rostedt, and M. O. Myreen, «Characteristic Formulae for Liveness Properties of Non-terminating CakeML Programs», in Interactive Theorem Proving (ITP), To appear, LIPICS, 2019. [Online]. Available: https://cakeml.org/itp19.pdf.
13. M. O. Myreen and S. Owens, «Proof-producing Translation of Higher-order logic into Pure and Stateful ML», Journal of Functional Programming, vol. 24, no. 2-3, pp. 284-315, 2014. doi: 10.1017/S0956796813000282.
14. O. Abrahamsson, S. Ho, H. Kanabar, R. Kumar, M. O. Myreen, M. Norrish, and Y. K. Tan, «Proof-Producing Synthesis of CakeML from Monadic HOL Functions», Springer, 2020. [Online]. Available: https://rdcu.be/b4FrU.
15. P. O'Hearn, «Separation Logic», Communications of the ACM, vol. 62, no. 2, pp. 86-95, 2019. doi: 10.1145/3211968.
16. L. C. Paulson, Isabelle-A GenericTheorem Prover (with a contribution by T. Nipkow), ser. Lecture Notes in Computer Science. Springer, 1994, vol. 828.
17. L. Hupel and T. Nipkow, «A Verified Compiler from Isabelle/HOL to CakeML», in European Symposium on Programming (ESOP), ser. Lecture Notes in Computer Science, vol. 10801, Springer, 2018, pp. 999-1026. doi: 10.1007/978-3-319-89884-1_35. [Online]. Available: https://lars.hupel.info/pub/isabelle-cakeml.pdf.
18. A. W. Appel, «Verified Software Toolchain», in European Symposium on Programming, Springer, 2011, pp. 1-17.
19. CompCert project. [Online]. Available: https://compcert.org.
20. Verification center of the operating system Linux. [Online]. Available: http://linuxtesting.org/publications.
21. Implementation of the network layer for seL4. [Online]. Available: https://github.com/SEL4PROJ/picotcp.
22. C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli, «Handbook of Satisfiability», in, ser. Frontiers in Artificial Intelligence and Applications. IOS Press, 2009, vol. 185, ch. Satisfiability Modulo Theories, pp. 825-885.
23. seL4 deployment using Genode. [Online]. Available: https://genode.org/documentation/articles/sel4_parts_1.
24. Introduction to CAmkES. [Online]. Available: https://docs.sel4.systems/Tutorials/hello-camkes-0.html.
25. R. Rezin, seL4 deploy scripts, 2020. [Online]. Available: https://github.com/RZRussel/seL4-deploy-public.git.
Review
For citations:
Merkin-Janson L.A., Rezin R.M., Vasilyev N.K. Architecture of the Formally-Verified Distributed Ledger System InnoChain. Modeling and Analysis of Information Systems. 2020;27(4):472-487. (In Russ.) https://doi.org/10.18255/1818-1015-2020-4-472-487
Views:
1242
Email this article 