Архитектура формально-верифицированной системы распределенного реестра InnoChain

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

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.