Formal Verification of Blockchain Byzantine Fault Tolerance

Pierre Tholoniat () and Vincent Gramoli ()
Additional contact information
Pierre Tholoniat: Columbia University
Vincent Gramoli: University of Sydney

A chapter in Handbook on Blockchain, 2022, pp 389-412 from Springer

Abstract: Abstract To implement a blockchain, the trend is now to integrate a non-trivial Byzantine fault-tolerant consensus algorithm instead of the seminal idea of waiting to receive blocks to decide upon the longest branch. After a dozen years of existence, blockchains trade now large amounts of valuable assets and a simple disagreement could lead to disastrous losses. Unfortunately, Byzantine consensus solutions used in blockchains are at best proved correct “by hand” as we are not aware of any of them having been automatically verified. We propose two contributions: (i) we illustrate the severity of the problem by listing six vulnerabilities of blockchain consensus including two new counter-examples; (ii) we then formally verify two Byzantine fault-tolerant components of Red Belly Blockchain (Crain et al. in Red belly: a secure, fair and scalable open blockchain, 2021, [32]) using the ByMC model checker. First, we specify its simple broadcast primitive in 116 lines of code that is verified in 40 s on a 2-core Intel machine. Then, we specify its blockchain consensus algorithm in 276 lines of code and assume a round-rigid adversary to verify in 17 minutes on a 64-core AMD machine using MPI. To conclude, we argue that it has now become both possible and crucial to formally verify the correctness of blockchain consensus protocols.

Date: 2022
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:spochp:978-3-031-07535-3_12

Ordering information: This item can be ordered from
http://www.springer.com/9783031075353

DOI: 10.1007/978-3-031-07535-3_12

Access Statistics for this chapter

More chapters in Springer Optimization and Its Applications from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().