Certifying Blockchain Byzantine Fault Tolerance
share
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 decade 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 certified. In this paper, 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 certify two Byzantine fault tolerant components of Red Belly Blockchain using the ByMC model checker: First, we specify a simple broadcast primitive in 116 lines that is certified in 40 seconds on a 2-core Intel machine and a blockchain consensus algorithm written in 309 lines of code and certified, using MPI, in 17 minutes on a 64-core AMD machine. To conclude, we argue that it has now become both relatively simple and crucial to certify the correctness of blockchain consensus protocols.
READ FULL TEXT