Holistic Verification of Blockchain Consensus
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazi\'c,, Pierre Tholoniat, Josef Widder

TL;DR
This paper presents the first holistic model checking verification of an industry-used blockchain consensus algorithm, ensuring its safety and liveness properties for any number of processes and Byzantine participants.
Contribution
It introduces a novel approach to verify blockchain consensus algorithms holistically using model checking, applied specifically to the Red Belly Blockchain.
Findings
Successfully verified safety and liveness properties in about 70 seconds.
Verified the consensus algorithm for any number of processes and Byzantine participants.
Decomposed the algorithm into two parts modeled as threshold automata.
Abstract
Blockchain has recently attracted the attention of the industry due, in part, to its ability to automate asset transfers. It requires distributed participants to reach a consensus on a block despite the presence of malicious (a.k.a. Byzantine) participants. Malicious participants exploit regularly weaknesses of these blockchain consensus algorithms, with sometimes devastating consequences. In fact, these weaknesses are quite common and are well illustrated by the flaws in the hand-written proofs of existing blockchain consensus protocols [63]. Paradoxically, until now, no blockchain consensus has been holistically verified using model checking. In this paper, we remedy this paradox by model checking for the first time a blockchain consensus used in industry. We propose a holistic approach to verify the consensus algorithm of the Red Belly Blockchain [20], for any number of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Blockchain Technology Applications and Security · Formal Methods in Verification
