maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2020-4-454-471mais-1436Research ArticleTheory of ComputingInnoChain: распределенный реестр для индустриального применения с формальной верификацией на всех уровнях реализацииInnoChain: a Distributed Ledger for Industry with Formal Verification on all Implementation Levelshttps://orcid.org/0000-0001-7377-7548КухаренкоВладимир АлександровичKukharenkoVladimir Aleksandrovich

Студент бакалавриата

Bachelor student

vladimir.a.kukharenko@gmail.comhttps://orcid.org/0000-0002-5676-9105ЗиборовКирилл ВикторовичZiborovKirill Viktorovich

Студент бакалавриата

Bachelor student

an49x00@gmail.comhttps://orcid.org/0000-0002-2792-2465СадыковРафаэль ФаритовичSadykovRafael Faritovich

Аспирант

Ph.D. student

sadykovrf@gmail.comhttps://orcid.org/0000-0002-7683-0751НаумчевАлександр ВладимировичNaumchevAlexandr Vladimirovich

Доцент, кандидат наук

Assistant professor, Ph.D

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

Магистр

MSc.

r.rezin@innopolis.ruhttps://orcid.org/0000-0002-8427-2200МеркинЛеонид АльбертовичMerkin-JansonLeonid Albertovich

Профессор

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

l.merkin@innopolis.ruМосковский физико-технический институтРоссияMoscow Institute of Physics and TechnologyRussian FederationМосковский государственный университет им. М.В. ЛомоносоваРоссияLomonosov Moscow State UniversityRussian FederationМосковский государственный университет им. М.В. Ломоносова; Университет ИннополисРоссияLomonosov Moscow State University; Innopolis UniversityRussian FederationУниверситет ИннополисРоссияInnopolis UniversityRussian Federation202019122020274454471Copyright © Кухаренко В.А., Зиборов К.В., Садыков Р.Ф., Наумчев А.В., Резин Р.М., Меркин Л.А., 20202020Кухаренко В.А., Зиборов К.В., Садыков Р.Ф., Наумчев А.В., Резин Р.М., Меркин Л.А.Kukharenko V.A., Ziborov K.V., Sadykov R.F., Naumchev A.V., Rezin R.M., Merkin-Janson L.A.Данная работа распространяется под лицензией 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/1436

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

The extent of formal verification methods applied to industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain, is rapidly changing the situation. Since the main area of DLSs' application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is required to ensure that the software implementation of the DLS nodes complies with this protocol. The verified software implementation of the protocol must run on a fairly reliable operating system. The so-called “smart contracts”, which are an important part of the applied implementations of specific business processes based on DLSs, must be verifiable as well. In this paper, we describe an ongoing industrial project that will result in a DLS verified at least at the four technological levels described above. We then share our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes.

устойчивость к византийским условиямраспределенный консенсусблокчейнTLA+верификацияпроверка моделейByzantine fault tolerancedistributed consensusblockchainTLA+verificationmodel checkingМинистерство цифрового развития, связи и массовых коммуникаций РФ и АО "Российская венчурная компания"(договор №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).ReferencesM. 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.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.S. Nakamoto, «Bitcoin: A peer-to-peer electronic cash system», Manubot, Tech. Rep., 2019.S. Nakamoto, «Bitcoin: A peer-to-peer electronic cash system», Manubot, Tech. Rep., 2019.G. Wood et al., «Ethereum: A secure decentralised generalised transaction ledger», Ethereum project yellow paper, vol. 151, no. 2014, pp. 1-32, 2014.G. Wood et al., «Ethereum: A secure decentralised generalised transaction ledger», Ethereum project yellow paper, vol. 151, no. 2014, pp. 1-32, 2014.E. Elrom, «EOS. IO Wallets and Smart Contracts», in The Blockchain Developer, Springer, 2019, pp. 213-256.E. Elrom, «EOS. IO Wallets and Smart Contracts», in The Blockchain Developer, Springer, 2019, pp. 213-256.F. Muratov, A. Lebedev, N. Iushkevich, B. Nasrulin, and M. Takemiya, «YAC: BFT Consensus Algorithm for Blockchain», CoRR, vol. abs/1809.00554, 2018.F. Muratov, A. Lebedev, N. Iushkevich, B. Nasrulin, and M. Takemiya, «YAC: BFT Consensus Algorithm for Blockchain», CoRR, vol. abs/1809.00554, 2018.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.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.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.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.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.L. Lamport, R. Shostak, and M. Pease, «The Byzantine Generals Problem», ACM Trans. Program. Lang. Syst., vol. 4, no. 3, pp. 382-401, 1982.L. Lamport, R. Shostak, and M. Pease, «The Byzantine Generals Problem», ACM Trans. Program. Lang. Syst., vol. 4, no. 3, pp. 382-401, 1982.M. Castro and B. Liskov, «Practical Byzantine Fault Tolerance», in OSDI, USENIX Association, 1999, pp. 173-186.M. Castro and B. Liskov, «Practical Byzantine Fault Tolerance», in OSDI, USENIX Association, 1999, pp. 173-186.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.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.J. Baek and Y. Zheng, «Simple and efficient threshold cryptosystem from the Gap Diffie-Hellman group», in GLOBECOM, IEEE, 2003, pp. 1491-1495.J. Baek and Y. Zheng, «Simple and efficient threshold cryptosystem from the Gap Diffie-Hellman group», in GLOBECOM, IEEE, 2003, pp. 1491-1495.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.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.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.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.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.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.D. Boneh, B. Lynn, and H. Shacham, «Short signatures from the Weil pairing», Journal of cryptology, vol. 17, no. 4, pp. 297-319, 2004.D. Boneh, B. Lynn, and H. Shacham, «Short signatures from the Weil pairing», Journal of cryptology, vol. 17, no. 4, pp. 297-319, 2004.E. Buchman, J. Kwon, and Z. Milosevic, «The latest gossip on BFT consensus», CoRR, vol. abs/1807.04938, 2018.E. Buchman, J. Kwon, and Z. Milosevic, «The latest gossip on BFT consensus», CoRR, vol. abs/1807.04938, 2018.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.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.Y. G. Karpov, MODEL CHECKING. Verification of parallel and distributed software systems, 2010.Y. G. Karpov, MODEL CHECKING. Verification of parallel and distributed software systems, 2010.L. C. Paulson, Isabelle: A generic theorem prover. Springer Science & Business Media, 1994, vol. 828.L. C. Paulson, Isabelle: A generic theorem prover. Springer Science & Business Media, 1994, vol. 828.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.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.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.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.I. Konnov, Model Checking Tendermint, 2020. [Online]. Available: https://github.com/informalsystems/verification/tree/igor/fork/spec/fork-cases.I. Konnov, Model Checking Tendermint, 2020. [Online]. Available: https://github.com/informalsystems/verification/tree/igor/fork/spec/fork-cases.V. Kukharenko, K. Ziborov, and R. Rezin, HotStuff TLA+ Specifications. [Online]. Available: https://github.com/RZRussel/hotstuff-model-checking.V. Kukharenko, K. Ziborov, and R. Rezin, HotStuff TLA+ Specifications. [Online]. Available: https://github.com/RZRussel/hotstuff-model-checking.K. Ziborov, HotStuff TLA+ Specifications, 2020. [Online]. Available: https://github.com/RZRussel/hotstuff-model-checking/blob/master/HotStuffAlpha.tla.K. Ziborov, HotStuff TLA+ Specifications, 2020. [Online]. Available: https://github.com/RZRussel/hotstuff-model-checking/blob/master/HotStuffAlpha.tla.V. Kukharenko, HotStuff TLA+ Specifications, 2020. [Online]. Available: https://github.com/RZRussel/hotstuff-model-checking/blob/master/ApalacheHotStuffCutted.tla.V. Kukharenko, HotStuff TLA+ Specifications, 2020. [Online]. Available: https://github.com/RZRussel/hotstuff-model-checking/blob/master/ApalacheHotStuffCutted.tla.

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