InnoChain: a Distributed Ledger for Industry with Formal Verification on all Implementation Levels

Modelirovanie i Analiz Informacionnyh Sistem

Alexandr Vladimirovich Naumchev¹  Ruslan Maratovich Rezin²  Leonid Albertovich Merkin-Janson²  Rafael Faritovich Sadykov³  Kirill Viktorovich Ziborov³  Vladimir Aleksandrovich Kukharenko⁴ 

[1] Innopolis University;Innopolis University;Lomonosov Moscow State University;Moscow Institute of Physics and Technology;

关键词: byzantine fault tolerance;    distributed consensus;    blockchain;    tla+;    verification;    model checking;   

DOI  :  10.18255/1818-1015-2020-4-454-471

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown