Geodesic
InnoChain: a distributed ledger for industry with formal verification on all implementation levels
Modelirovanie i analiz informacionnyh sistem, Tome 27 (2020) no. 4, pp. 454-471.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: Byzantine fault tolerance, distributed consensus, blockchain, TLA+, verification, model checking. 
@article{MAIS_2020_27_4_a6,
     author = {V. A. Kukharenko and K. V. Ziborov and R. F. Sadykov and A. V. Naumchev and R. M. Rezin and L. A. Merkin-Janson},
     title = {InnoChain: a distributed ledger for industry with formal verification on all implementation levels},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {454--471},
     publisher = {mathdoc},
     volume = {27},
     number = {4},
     year = {2020},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2020_27_4_a6/}
}
TY  - JOUR
AU  - V. A. Kukharenko
AU  - K. V. Ziborov
AU  - R. F. Sadykov
AU  - A. V. Naumchev
AU  - R. M. Rezin
AU  - L. A. Merkin-Janson
TI  - InnoChain: a distributed ledger for industry with formal verification on all implementation levels
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2020
SP  - 454
EP  - 471
VL  - 27
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2020_27_4_a6/
LA  - ru
ID  - MAIS_2020_27_4_a6
ER  - 
%0 Journal Article
%A V. A. Kukharenko
%A K. V. Ziborov
%A R. F. Sadykov
%A A. V. Naumchev
%A R. M. Rezin
%A L. A. Merkin-Janson
%T InnoChain: a distributed ledger for industry with formal verification on all implementation levels
%J Modelirovanie i analiz informacionnyh sistem
%D 2020
%P 454-471
%V 27
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2020_27_4_a6/
%G ru
%F MAIS_2020_27_4_a6
V. A. Kukharenko; K. V. Ziborov; R. F. Sadykov; A. V. Naumchev; R. M. Rezin; L. A. Merkin-Janson. InnoChain: a distributed ledger for industry with formal verification on all implementation levels. Modelirovanie i analiz informacionnyh sistem, Tome 27 (2020) no. 4, pp. 454-471. http://geodesic.mathdoc.fr/item/MAIS_2020_27_4_a6/

[1] M. Fazlali, S. M. Eftekhar, M. M. Dehshibi, H. T. Malazi, M. Nosrati, Raft Consensus Algorithm: an Effective Substitute for Paxos in Highroughput P2P-based Systems, 2019, arXiv: 1911.01231

[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, 151:2014 (2014), 1–32

[4] E. Elrom, “EOS.IO Wallets, Smart Contracts”, Thee Blockchain Developer, Springer, 2019, 213–256 | DOI

[5] F. Muratov, A. Lebedev, N. Iushkevich, B. Nasrulin, M. Takemiya, YAC: BFT Consensus Algorithm for Blockchain, 2018, arXiv: 1809.00554

[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”, EuroSys, ACM, 2018, 30:1–30:15

[7] T. Gauthier, C. Kaliszyk, J. Urban, “TacticToe: Learning to Reason with HOL4 Tactics”, LPAR, EPiC Series in Computing, 46, 2017, 125–143 (EasyChair) | MR

[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, S. Winwood, “seL4: formal verification of an OS kernel”, SOSP, ACM, 2009, 207–220 | DOI | MR

[9] L. Lamport, R. Shostak, M. Pease, “The Byzantine Generals Problem”, ACM Trans. Program. Lang. Syst., 4:3 (1982), 382–401 | DOI | MR | Zbl

[10] M. Castro, B. Liskov, “Practical Byzantine Fault Tolerance”, OSDI, USENIX Association, 1999, 173–186

[11] A. Miller, Y. Xia, K. Croman, E. Shi, D. Song, “The honey badger of BFT protocols”, Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016, 31–42 | DOI

[12] J. Baek, Y. Zheng, “Simple and efficient threshold cryptosystem from the Gap Diffie-Hellman group”, GLOBECOM, IEEE, 2003, 1491–1495

[13] M. Ben-Or, B. Kelmer, T. Rabin, “Asynchronous secure computations with optimal resilience”, Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, ACM, 1994, 183–192 | DOI | Zbl

[14] A. Mostefaoui, M. Hamouna, M. Raynal, “Signature-Free Asynchronous Byzantine Consensus with $t/3$ and $O(n^2)$ Messages”, Proceedings of the 2014 ACM symposium on Principles of distributed computing, ACM, 2014, 2–9 | DOI | MR | Zbl

[15] G. Golan-Gueta, I. Abraham, S. Grossman, D. Malkhi, B. Pinkas, M. K. Reiter, D. A. Seredinschi, O. Tamir, A. Tomescu, SBFT: a Scalable Decentralized Trust Infrastructure for Blockchains, 2018, arXiv: 1804.01626

[16] D. Boneh, B. Lynn, H. Shacham, “Short signatures from the Weil pairing”, Journal of cryptology, 17:4 (2004), 297–319 | DOI | MR | Zbl

[17] E. Buchman, J. Kwon, Z. Milosevic, The latest gossip on BFT consensus, 2018, arXiv: 1807.04938

[18] M. Yin, D. Malkhi, M. K. Reiter, G. G. Gueta, I. Abraham, “Hotstuff: Bft consensus with linearity and responsiveness”, Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, 2019, 347–356 | DOI | Zbl

[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, Lecture Notes in Computer Science, 828, 1994 | MR | Zbl

[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, version 6.11, INRIA, 1999

[22] V. Rahli, I. Vukotic, M. Volp, P. Esteves-Verissimo, “Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq”, ESOP, Lecture Notes in Computer Science, 10801, Springer, 2018, 619–650 | DOI

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

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

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

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