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/