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

Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации и формальной верификации. Формальная спецификация и верификация протокола консенсуса необходима, но недостаточна. Необходимо удостовериться, что программная реализация узлов СРР соответствует данному протоколу. Верифицированная программная реализация протокола должна запускаться на достаточно надежной операционной системе. Так называемые “умные контракт”, которые являются важной частью прикладных реализаций конкретных бизнес-процессов на основе СРР, также должны быть верифицируемы.В данной работе мы описываем реализующийся в настоящее время индустриальный проект, результатом которого станет СРР, верифицированная по меньшей мере на четырех описанных выше технологических уровнях. Мы также описываем наш опыт формальной спецификации и верификации протокола HotStuff - отказоустойчивого протокола для гарантированного достижения консенсуса в присутствии византийских процессов и лидера.

1. M. Fazlali, S. M. Eftekhar, M. M. Dehshibi, H. T. Malazi, and M. Nosrati, «Raft Consensus Algorithm: an Effective Substitute for Paxos in High Throughput P2P-based Systems», CoRR, vol. abs/1911.01231, 2019.

2. S. Nakamoto, «Bitcoin: A peer-to-peer electronic cash system», Manubot, Tech. Rep., 2019.

3. G. Wood et al., «Ethereum: A secure decentralised generalised transaction ledger», Ethereum project yellow paper, vol. 151, no. 2014, pp. 1-32, 2014.

4. E. Elrom, «EOS. IO Wallets and Smart Contracts», in The Blockchain Developer, Springer, 2019, pp. 213-256.

5. F. Muratov, A. Lebedev, N. Iushkevich, B. Nasrulin, and M. Takemiya, «YAC: BFT Consensus Algorithm for Blockchain», CoRR, vol. abs/1809.00554, 2018.

6. E. Androulaki, A. Barger, V. Bortnikov, C. Cachin, K. Christidis, A. De Caro, D. Enyeart, C. Ferris, G. Laventman, Y. Manevich, et al., «Hyperledger fabric: a distributed operating system for permissioned blockchains», in EuroSys, ACM, 2018, 30:1-30:15.

7. 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.

8. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, «seL4: formal verification of an OS kernel», in SOSP, ACM, 2009, pp. 207-220.

9. L. Lamport, R. Shostak, and M. Pease, «The Byzantine Generals Problem», ACM Trans. Program. Lang. Syst., vol. 4, no. 3, pp. 382-401, 1982.

10. M. Castro and B. Liskov, «Practical Byzantine Fault Tolerance», in OSDI, USENIX Association, 1999, pp. 173-186.

11. A. Miller, Y. Xia, K. Croman, E. Shi, and D. Song, «The honey badger of BFT protocols», in Proceedings of the 2016 ACMSIGSAC Conference on Computerand Communications Security, 2016, pp. 31-42.

12. J. Baek and Y. Zheng, «Simple and efficient threshold cryptosystem from the Gap Diffie-Hellman group», in GLOBECOM, IEEE, 2003, pp. 1491-1495.

13. M. Ben-Or, B. Kelmer, and T. Rabin, «Asynchronous secure computations with optimal resilience», in Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, ACM, 1994, pp. 183-192.

14. A. Mostefaoui, M. Hamouna, and M. Raynal, «Signature-Free Asynchronous Byzantine Consensus with t < n/3 and O(n2) Messages», in Proceedings of the 2014 ACM symposium on Principles of distributed computing, ACM, 2014, pp. 2-9.

15. G. Golan-Gueta, I. Abraham, S. Grossman, D. Malkhi, B. Pinkas, M. K. Reiter, D.-A. Seredinschi, O. Tamir, and A. Tomescu, «SBFT: a Scalable Decentralized Trust Infrastructure for Blockchains», CoRR, vol. abs/1804.01626, 2018.

16. D. Boneh, B. Lynn, and H. Shacham, «Short signatures from the Weil pairing», Journal of cryptology, vol. 17, no. 4, pp. 297-319, 2004.

17. E. Buchman, J. Kwon, and Z. Milosevic, «The latest gossip on BFT consensus», CoRR, vol. abs/1807.04938, 2018.

18. M. Yin, D. Malkhi, M. K. Reiter, G. G. Gueta, and I. Abraham, «Hotstuff: Bft consensus with linearity and responsiveness», in Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, 2019, pp. 347-356.

19. Y. G. Karpov, MODEL CHECKING. Verification of parallel and distributed software systems, 2010.

20. L. C. Paulson, Isabelle: A generic theorem prover. Springer Science & Business Media, 1994, vol. 828.

21. B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filliatre, E. Gimenez, H. Herbelin, et al., «The Coq proof assistant reference manual», INRIA, version, vol. 6, no. 11, 1999.

22. V. Rahli, I. Vukotic, M. Volp, and P. Esteves-Verissimo, «Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq», in ESOP, ser. Lecture Notes in Computer Science, vol. 10801, Springer, 2018, pp. 619-650.

23. I. Konnov, Model Checking Tendermint, 2020. [Online]. Available: https://github.com/informalsystems/verification/tree/igor/fork/spec/fork-cases.

24. V. Kukharenko, K. Ziborov, and R. Rezin, HotStuff TLA+ Specifications. [Online]. Available: https://github.com/RZRussel/hotstuff-model-checking.

25. K. Ziborov, HotStuff TLA+ Specifications, 2020. [Online]. Available: https://github.com/RZRussel/hotstuff-model-checking/blob/master/HotStuffAlpha.tla.

26. V. Kukharenko, HotStuff TLA+ Specifications, 2020. [Online]. Available: https://github.com/RZRussel/hotstuff-model-checking/blob/master/ApalacheHotStuffCutted.tla.