License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.DISC.2022.10
URN: urn:nbn:de:0030-drops-172019
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17201/
Go to the corresponding LIPIcs Volume Portal

Bertrand, Nathalie ; Gramoli, Vincent ; Konnov, Igor ; Lazić, Marijana ; Tholoniat, Pierre ; Widder, Josef

Holistic Verification of Blockchain Consensus

pdf-format:
LIPIcs-DISC-2022-10.pdf (0.9 MB)

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 various blockchain consensus algorithms [Pierre Tholoniat and Vincent Gramoli, 2019]. 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 Red Belly Blockchain [Tyler Crain et al., 2021], 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 [Igor Konnov et al., 2017], 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 Red Belly Blockchain consensus but also its liveness in less than 70 seconds.

BibTeX - Entry

@InProceedings{bertrand_et_al:LIPIcs.DISC.2022.10,
  author =	{Bertrand, Nathalie and Gramoli, Vincent and Konnov, Igor and Lazi\'{c}, Marijana and Tholoniat, Pierre and Widder, Josef},
  title =	{{Holistic Verification of Blockchain Consensus}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{10:1--10:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-255-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{246},
  editor =	{Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/17201},
  URN =		{urn:nbn:de:0030-drops-172019},
  doi =		{10.4230/LIPIcs.DISC.2022.10},
  annote =	{Keywords: Model checking, automata, logic, byzantine failure}
}

Keywords: Model checking, automata, logic, byzantine failure
Collection: 36th International Symposium on Distributed Computing (DISC 2022)
Issue Date: 2022
Date of publication: 17.10.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI