Geodesic
Architecture of the formally-verified distributed ledger system innochain
Modelirovanie i analiz informacionnyh sistem, Tome 27 (2020) no. 4, pp. 472-487.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: distributed ledger systems, formal verification, HOL4, CakeML
Mots-clés : seL4. 
@article{MAIS_2020_27_4_a7,
     author = {L. A. Merkin-Janson and R. M. Rezin and N. K. Vasilyev},
     title = {Architecture of the formally-verified distributed ledger system innochain},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {472--487},
     publisher = {mathdoc},
     volume = {27},
     number = {4},
     year = {2020},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2020_27_4_a7/}
}
TY  - JOUR
AU  - L. A. Merkin-Janson
AU  - R. M. Rezin
AU  - N. K. Vasilyev
TI  - Architecture of the formally-verified distributed ledger system innochain
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2020
SP  - 472
EP  - 487
VL  - 27
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2020_27_4_a7/
LA  - ru
ID  - MAIS_2020_27_4_a7
ER  - 
%0 Journal Article
%A L. A. Merkin-Janson
%A R. M. Rezin
%A N. K. Vasilyev
%T Architecture of the formally-verified distributed ledger system innochain
%J Modelirovanie i analiz informacionnyh sistem
%D 2020
%P 472-487
%V 27
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2020_27_4_a7/
%G ru
%F MAIS_2020_27_4_a7
L. A. Merkin-Janson; R. M. Rezin; N. K. Vasilyev. Architecture of the formally-verified distributed ledger system innochain. Modelirovanie i analiz informacionnyh sistem, Tome 27 (2020) no. 4, pp. 472-487. http://geodesic.mathdoc.fr/item/MAIS_2020_27_4_a7/

[1] A. Burns, A. Wellings, Concurrent and Real-Time Programming in Ada 2005, Cambridge University Press, 2007 | Zbl

[2] A. Burns, A. Wellings, Real-Time Systems and Programming Languages, Addison-Wesley, 2009

[3] Smart Contracts Under Control, 2020 https://archetype-lang.org/

[4] More Ethereum Attacks: Race-To-Empty is the Real Deal, 2016 https://vessenes.com/more-ethereum-attacks-race-to-empty-is-the-real-deal

[5] CakeML: A verified implementation of ML, 2020 https://cakeml.org/

[6] M. Yin, D. Malkhi, M. K. Reiter, G. G. Gueta, I. Abraham, “HotStuff: BFT Consensus with Linearity and Responsiveness”, PODC, ACM, 2019, 347–356 | Zbl

[7] G. Heiser, The seL4 Microkernel: An Introduction, 2020 https://sel4.systems/About/seL4-whitepaper.pdf

[8] Libra by Facebook, https://github.com/libra/libra

[9] S. Owens, M. O. Myreen, R. Kumar, Y. K. Tan, “Functional Big-step Semantics”, Programming Languages and Systems, 25th European Symposium on Programming, ESOP 2016, Lecture Notes in Computer Science, 9632, ed. P. Thiemann, Springer, 2016, 589–615 | DOI | MR

[10] T. Gauthier, C. Kaliszyk, J. Urban, “TacticToe: Learning to Reason with HOL4 Tactics”, LPAR, EPiC Series in Computing, 46, 2017, 125–143 (EasyChair) | MR

[11] C. Baier, J.-P. Katoen, Principles of Model Checking, MIT Press, 2008 | MR | Zbl

[12] J. A. Pohjola, H. Rostedt, M. O. Myreen, “Characteristic Formulae for Liveness Properties of Non-terminating CakeML Programs”, Interactive Theorem Proving (ITP), LIPICS, 2019 (to appear) https://cakeml.org/itp19.pdf | MR

[13] M. O. Myreen, S. Owens, “Proof-producing Translation of Higher-order logic into Pure and Stateful ML”, Journal of Functional Programming, 24:2-3 (2014), 284–315 | DOI | MR | Zbl

[14] O. Abrahamsson, S. Ho, H. Kanabar, R. Kumar, M. O. Myreen, M. Norrish, Y. K. Tan, “Proof-Producing Synthesis of CakeML from Monadic HOL Functions”, Journal of Automated Reasoning, 64, 1287–1306 https://rdcu.be/b4FrU | DOI | MR | Zbl

[15] P. O'Hearn, “Separation Logic”, Communications of the ACM, 62:2 (2019), 86–95 | DOI

[16] L. C. Paulson, “Isabelle – A Generic theorem Prover (with a contribution by T. Nipkow)”, Lecture Notes in Computer Science, 828, Springer, 1994 | DOI | MR | Zbl

[17] L. Hupel, T. Nipkow, “A Verified Compiler from Isabelle/HOL to CakeML”, European Symposium on Programming (ESOP), Lecture Notes in Computer Science, 10801, Springer, 2018, 999–1026 https://lars.hupel.info/pub/isabelle-cakeml.pdf | DOI | MR | Zbl

[18] A. W. Appel, “Verified Software Toolchain”, European Symposium on Programming, Springer, 2011, 1–17 | Zbl

[19] CompCert project, https://compcert.org/

[20] Verification center of the operating system Linux, http://linuxtesting.org/publications

[21] Implementation of the network layer for seL4, https://github.com/SEL4PROJ/picotcp

[22] C. Barrett, R. Sebastiani, S. Seshia, C. Tinelli, “Satisfiability Modulo Theories”, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, 185, IOS Press, 2009, 825–885 | MR

[23] seL4 deployment using Genode, https://genode.org/documentation/articles/sel4_parts_1

[24] Introduction to CAmkES, https://docs.sel4.systems/Tutorials/hello-camkes-0.html

[25] R. Rezin, seL4 deploy scripts, , 2020 https://github.com/RZRussel/seL4-deploy-public.git