Formal Verification of Blockchain Byzantine Fault Tolerance

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.