Authored by:
Nathalie Bertrand, INRIA
Vincent Gramoli, University of Sydney
Igor Konnov, Informal Systems
Marijana Lazic, TU Munich
Pierre Tholoniat, Columbia University, NY
Josef Widder, Informal Systems
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 various blockchain consensus algorithms. Paradoxically, until now, no blockchain consensus has been holistically
verified.
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 Redbelly Blockchain, for any number n of processes and any number f < n/3 of Byzantine processes. We decompose directly the algorithm pseudocode in two parts—an inner broadcast algorithm and an outer decision algorithm—each modelled as a threshold automaton [37], and we formalize their expected properties in linear-time temporal logic. We then automatically check the inner broadcasting algorithm, under a carefully identified fairness assumption. For the verification of the outer algorithm, we simplify the model of the inner algorithm by relying on its proven properties. Doing so, we formally verify, for any parameter, not only the safety properties of the Redbelly Blockchain consensus but also its liveness in less than 70 seconds.
Download Paper
This paper was co-authored by our CTO and Founder Professor Vincent Gramoli.
Professor Vincent Gramoli is a full professor at the University of Sydney. He is a researcher in the field of distributed systems and algorithms, with a focus on the design and analysis of distributed systems and algorithms for shared memory and data-centric systems, including distributed hash tables, distributed shared memory and transactional memory. He has published numerous papers in top-tier conferences and journals in the field and has received several awards for his research. He is also currently serving as the Head of Concurrent Systems Research Group at the University of Sydney.