maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2020-4-472-487mais-1437Research ArticleTheory of ComputingАрхитектура формально-верифицированной системы распределенного реестра InnoChainArchitecture of the Formally-Verified Distributed Ledger System InnoChainhttps://orcid.org/0000-0002-8427-2200МеркинЛеонид АльбертовичMerkin-JansonLeonid Al'bertovich

Профессор, научный руководитель Лидирующего исследовательского центра в области формально-верифицированных систем распределенного реестра

Professor, Doctor of Mathematics, Delft University of Technology, Dr.

l.merkin@innopolis.ruhttps://orcid.org/0000-0002-0604-2645РезинРуслан МаратовичRezinRuslan Maratovich

Главный эксперт формальных методов верификации, степень магистра по направлению “Информатика и вычислительная техника”

Head expert in formal verification methods at Innopolis University, Master degree in Computer Science, MSc.

r.rezin@innopolis.ruhttps://orcid.org/0000-0003-3112-5482ВасильевНиколай КонстантиновичVasilyevNikolay Konstantinovich

Ведущий разработчик

Lead Developer.

n.vasilev@innopolis.ruУниверситет ИннополисРоссияInnopolis UniversityRussian FederationУниверситет Иннополис, Университетская; Национальный исследовательский университет «Высшая школа экономики»РоссияInnopolis University; National Research University Higher School of EconomicsRussian Federation202019122020274472487Copyright © Меркин Л.А., Резин Р.М., Васильев Н.К., 20202020Меркин Л.А., Резин Р.М., Васильев Н.К.Merkin-Janson L.A., Rezin R.M., Vasilyev N.K.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1437

В настоящей работе рассматривается архитектура системы распределенного реестра (СРР) InnoChain. Основной целью этой архитектуры является реализуемость 5-ти уровней формальной верификации программного обеспечения (ПО) системы InnoChain, включая операционное окружение. Методы формальной верификации являются основными методами обеспечения качества ПО с критическими требованиями по надежности, но до сих пор онине находилиширокого применения в СРР. Архитектура InnoChain включает (1) предметно-ориентированный язык смарт-контрактов с формальной семантикой, встроенный в функциональный язык CakeML (диалект языка ML), что позволяет осуществлять формальную верификацию свойств корректности смарт-контрактов в системах логики высших порядков (например, HOL4); (2) верифицированную трансляцию смарт-контрактов в машинный код с использованием компилятора CakeML вместо использования виртуальных машин для исполнения смарт-контрактов; (3) реализацию функционала узла СРР также на CakeML с формальной верификацией свойств корректности и с верифицированной трансляцией исходного кода узла в машинный код; (4) формальную верификацию протокола консенсуса СРР (HotStuff BFT); (5) использование формально-верифицированного микроядра seL4 в качестве операционного окружения СРР вместо операционных систем общего назначения. Предлагаемая архитектура открывает возможности для использования СРР 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 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.

системы распределенного реестраформальная верификацияHOL4CakeMLseL4distributed ledger systemsformal verificationHOL4CakeMLseL4Министерство цифрового развития, связи и массовых коммуникаций РФ и АО "Российская венчурная компания"(договор №004/20 от 20.03.2020, ИГК 0000000007119P190002).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).ReferencesA. Burns and A. Wellings, Concurrent and Real-Time Programming in Ada 2005. Cambridge University Press, 2007.A. Burns and A. Wellings, Concurrent and Real-Time Programming in Ada 2005. Cambridge University Press, 2007.A. Burns and A. Wellings, Real-Time Systems and Programming Languages. Addison-Wesley, 2009.A. Burns and A. Wellings, Real-Time Systems and Programming Languages. Addison-Wesley, 2009.Smart Contracts Under Control, 2020. [Online]. Available: https://archetype-lang.org.Smart Contracts Under Control, 2020. [Online]. Available: https://archetype-lang.org.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.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.CakeML: A verified implementation of ML, 2020. [Online]. Available: https://cakeml.org.CakeML: A verified implementation of ML, 2020. [Online]. Available: https://cakeml.org.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.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.G. Heiser, The seL4 Microkernel: An Introduction, 2020. [Online]. Available: https://sel4.systems/About/seL4-whitepaper.pdf .G. Heiser, The seL4 Microkernel: An Introduction, 2020. [Online]. Available: https://sel4.systems/About/seL4-whitepaper.pdf .Libra by Facebook. [Online]. Available: https://github.com/libra/libra.Libra by Facebook. [Online]. Available: https://github.com/libra/libra.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.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.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.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.C. Baier and J.-P. Katoen, Principles of Model Checking. MIT Press, 2008.C. Baier and J.-P. Katoen, Principles of Model Checking. MIT Press, 2008.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.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.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.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.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.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.P. O'Hearn, «Separation Logic», Communications of the ACM, vol. 62, no. 2, pp. 86-95, 2019. doi: 10.1145/3211968.P. O'Hearn, «Separation Logic», Communications of the ACM, vol. 62, no. 2, pp. 86-95, 2019. doi: 10.1145/3211968.L. C. Paulson, Isabelle-A GenericTheorem Prover (with a contribution by T. Nipkow), ser. Lecture Notes in Computer Science. Springer, 1994, vol. 828.L. C. Paulson, Isabelle-A GenericTheorem Prover (with a contribution by T. Nipkow), ser. Lecture Notes in Computer Science. Springer, 1994, vol. 828.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.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.A. W. Appel, «Verified Software Toolchain», in European Symposium on Programming, Springer, 2011, pp. 1-17.A. W. Appel, «Verified Software Toolchain», in European Symposium on Programming, Springer, 2011, pp. 1-17.CompCert project. [Online]. Available: https://compcert.org.CompCert project. [Online]. Available: https://compcert.org.Verification center of the operating system Linux. [Online]. Available: http://linuxtesting.org/publications.Verification center of the operating system Linux. [Online]. Available: http://linuxtesting.org/publications.Implementation of the network layer for seL4. [Online]. Available: https://github.com/SEL4PROJ/picotcp.Implementation of the network layer for seL4. [Online]. Available: https://github.com/SEL4PROJ/picotcp.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.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.seL4 deployment using Genode. [Online]. Available: https://genode.org/documentation/articles/sel4_parts_1.seL4 deployment using Genode. [Online]. Available: https://genode.org/documentation/articles/sel4_parts_1.Introduction to CAmkES. [Online]. Available: https://docs.sel4.systems/Tutorials/hello-camkes-0.html.Introduction to CAmkES. [Online]. Available: https://docs.sel4.systems/Tutorials/hello-camkes-0.html.R. Rezin, seL4 deploy scripts, 2020. [Online]. Available: https://github.com/RZRussel/seL4-deploy-public.git.R. Rezin, seL4 deploy scripts, 2020. [Online]. Available: https://github.com/RZRussel/seL4-deploy-public.git.

The authors declare that there are no conflicts of interest present.