Architecture of the Formally-Verified Distributed Ledger System InnoChain
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 m...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2020-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1437 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849338876426977280 |
|---|---|
| author | Leonid Al'bertovich Merkin-Janson Ruslan Maratovich Rezin Nikolay Konstantinovich Vasilyev |
| author_facet | Leonid Al'bertovich Merkin-Janson Ruslan Maratovich Rezin Nikolay Konstantinovich Vasilyev |
| author_sort | Leonid Al'bertovich Merkin-Janson |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-e4daf88db8424357903fb6359667208c |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2020-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-e4daf88db8424357903fb6359667208c2025-08-20T03:44:17ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172020-12-0127447248710.18255/1818-1015-2020-4-472-4871093Architecture of the Formally-Verified Distributed Ledger System InnoChainLeonid Al'bertovich Merkin-Janson0Ruslan Maratovich Rezin1Nikolay Konstantinovich Vasilyev2Innopolis UniversityInnopolis UniversityInnopolis University; National Research University Higher School of EconomicsIn 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.https://www.mais-journal.ru/jour/article/view/1437distributed ledger systemsformal verificationhol4cakemlsel4 |
| spellingShingle | Leonid Al'bertovich Merkin-Janson Ruslan Maratovich Rezin Nikolay Konstantinovich Vasilyev Architecture of the Formally-Verified Distributed Ledger System InnoChain Моделирование и анализ информационных систем distributed ledger systems formal verification hol4 cakeml sel4 |
| title | Architecture of the Formally-Verified Distributed Ledger System InnoChain |
| title_full | Architecture of the Formally-Verified Distributed Ledger System InnoChain |
| title_fullStr | Architecture of the Formally-Verified Distributed Ledger System InnoChain |
| title_full_unstemmed | Architecture of the Formally-Verified Distributed Ledger System InnoChain |
| title_short | Architecture of the Formally-Verified Distributed Ledger System InnoChain |
| title_sort | architecture of the formally verified distributed ledger system innochain |
| topic | distributed ledger systems formal verification hol4 cakeml sel4 |
| url | https://www.mais-journal.ru/jour/article/view/1437 |
| work_keys_str_mv | AT leonidalbertovichmerkinjanson architectureoftheformallyverifieddistributedledgersysteminnochain AT ruslanmaratovichrezin architectureoftheformallyverifieddistributedledgersysteminnochain AT nikolaykonstantinovichvasilyev architectureoftheformallyverifieddistributedledgersysteminnochain |