Document Open Access Logo

Holistic Verification of Blockchain Consensus

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

PDF
Thumbnail PDF

File

LIPIcs.DISC.2022.10.pdf
  • Filesize: 0.91 MB
  • 24 pages

Document Identifiers

Author Details

Nathalie Bertrand
  • INRIA Rennes, France
Vincent Gramoli
  • University of Sydney, Australia
  • Redbelly Network, Sydney, Australia
Igor Konnov
  • Informal Systems, Wien, Austria
Marijana Lazić
  • TU München, Germany
Pierre Tholoniat
  • Columbia University, New York, NY, USA
Josef Widder
  • Informal Systems, Wien, Austria

Funding

This research is supported under Australian Research Council Future Fellowship funding scheme (project number 180100496) entitled "The Red Belly Blockchain: A Scalable Blockchain for Internet of Things", Interchain Foundation (Switzerland), and the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).

Cite AsGet BibTex

Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić, Pierre Tholoniat, and Josef Widder. Holistic Verification of Blockchain Consensus. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.DISC.2022.10

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.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Distributed algorithms
  • Theory of computation → Logic and verification
Keywords
  • Model checking
  • automata
  • logic
  • byzantine failure

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Ittai Abraham, Guy Golan Gueta, Dahlia Malkhi, Lorenzo Alvisi, Rama Kotla, and Jean-Philippe Martin. Revisiting fast practical byzantine fault tolerance. Technical report, arXiv, December 2017. URL: http://arxiv.org/abs/1712.01367.
  2. C. Aiswarya, Benedikt Bollig, and Paul Gastin. An automata-theoretic approach to the verification of distributed algorithms. Information and Computation, 259(3):305-327, 2018. Google Scholar
  3. Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, and Grigore Rosu. Towards a verified model of the algorand consensus protocol in Coq. In International Workshops on Formal Methods (FM'19), pages 362-367, 2019. Google Scholar
  4. Rajeev Alur and Thomas A. Henzinger. Finitary fairness. In Annual IEEE Symposium on Logic in Computer Science (LICS'94), pages 52-61. IEEE Computer Society Press, 1994. Google Scholar
  5. Elli Androulaki, Artem Barger, Vita Bortnikov, Christian Cachin, Konstantinos Christidis, Angelo De Caro, David Enyeart, Christopher Ferris, Gennady Laventman, Yacov Manevich, Srinivasan Muralidharan, Chet Murthy, Binh Nguyen, Manish Sethi, Gari Singh, Keith Smith, Alessandro Sorniotti, Chrysoula Stathakopoulou, Marko Vukolić, Sharon Weed Cocco, and Jason Yellick. Hyperledger Fabric: A distributed operating system for permissioned blockchains. In ACM European Conference on Computer Systems (CCS'18), 2018. Google Scholar
  6. Krzysztof R Apt and Dexter C Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307-309, May 1986. Google Scholar
  7. A. R. Balasubramanian, Javier Esparza, and Marijana Lazic. Complexity of verification and synthesis of threshold automata. In International Symposium on Automated Technology for Verification and Analysis (ATVA'20), pages 144-160, 2020. Google Scholar
  8. Michael Ben-Or. Another advantage of free choice (extended abstract): Completely asynchronous agreement protocols. In Annual ACM Symposium on Principles of Distributed Computing (PODC'83), pages 27-30, 1983. Google Scholar
  9. Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, and Sharon Shoham. Verification of threshold-based distributed algorithms by decomposition to decidable logics. In International Conference on Computer Aided Verification (CAV'19), pages 245-266, 2019. Google Scholar
  10. Nathalie Bertrand, Igor Konnov, Marijana Lazic, and Josef Widder. Verification of randomized consensus algorithms under round-rigid adversaries. In International Conference on Concurrency Theory (CONCUR'19), pages 33:1-33:15, 2019. Google Scholar
  11. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. Google Scholar
  12. Richard Gendal Brown, James Carlyle, Ian Grigg, and Mike Hearn. Corda: An introduction. R3 CEV, August, 2016. Google Scholar
  13. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 10^20 states and beyond. In Annual Symposium on Logic in Computer Science (LICS'90), pages 428-439, 1990. Google Scholar
  14. Christian Cachin, Daniel Collins, Tyler Crain, and Vincent Gramoli. Anonymity preserving Byzantine vector consensus. In European Symposium on Research in Computer Security (ESORICS'20), pages 133-152, September 2020. Google Scholar
  15. Christian Cachin and Luca Zanolini. Asymmetric Byzantine consensus. Technical Report 2005.08795, arXiv, 2020. Google Scholar
  16. Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz. A reduction theorem for the verification of round-based distributed algorithms. In International Workshop on Reachability Problems (RP'09), pages 93-106, 2009. Google Scholar
  17. Bernadette Charron-Bost, Henri Debrat, and Stephan Merz. Formal verification of consensus algorithms tolerating malicious faults. In SSS, pages 120-134, 2011. Google Scholar
  18. Pierre Civit, Seth Gilbert, and Vincent Gramoli. Polygraph: Accountable Byzantine agreement. In Proceedings of the 41st IEEE International Conference on Distributed Computing Systems (ICDCS'21), July 2021. Google Scholar
  19. Tyler Crain, Vincent Gramoli, Mikel Larrea, and Michel Raynal. DBFT: Efficient leaderless Byzantine consensus and its applications to blockchains. In International Symposium on Network Computing and Applications (NCA'18), 2018. URL: http://gramoli.redbellyblockchain.io/web/doc/pubs/DBFT-preprint.pdf.
  20. Tyler Crain, Christopher Natoli, and Vincent Gramoli. Red Belly: A secure, fair and scalable open blockchain. In IEEE Symposium on Security and Privacy (S&P'21), 2021. Google Scholar
  21. Andrei Damian, Cezara Drăgoi, Alexandru Militaru, and Josef Widder. Communication-closed asynchronous protocols. In International Conference on Computer Aided Verification (CAV'19), pages 344-363, 2019. Google Scholar
  22. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'08), pages 337-340, 2008. Google Scholar
  23. Rodney G. Downey and Michael R. Fellows. Parameterized Complexity. Monographs in Computer Science. Springer, 1999. Google Scholar
  24. Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. A logic-based framework for verifying consensus algorithms. In International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'14), pages 161-181, 2014. Google Scholar
  25. Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Consensus in the presence of partial synchrony. J. ACM, 35(2):288-323, April 1988. Google Scholar
  26. Ali Ebnenasir and Alex P. Klinkhamer. Topology-specific synthesis of self-stabilizing parameterized systems with constant-space processes. IEEE Trans. Software Eng., 47(3):614-629, 2021. Google Scholar
  27. Tzilla Elrad and Nissim Francez. Decomposition of distributed programs into communication-closed layers. Science of Computer Programming, 2(3):155-173, 1982. Google Scholar
  28. E. Allen Emerson and Vineet Kahlon. Reducing model checking of the many to the few. In International Conference on Automated Deduction (CADE'17), pages 236-254, 2000. Google Scholar
  29. Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM, 32(2):374-382, April 1985. Google Scholar
  30. Dana Fisman, Orna Kupferman, and Yoad Lustig. On verifying fault tolerance of distributed protocols. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'08), pages 315-331, 2008. Google Scholar
  31. Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. Ironfleet: proving practical distributed systems correct. In Symposium on Operating Systems Principles (SOSP'15), pages 1-17, 2015. Google Scholar
  32. Gerard Holzmann. The SPIN Model Checker. Addison-Wesley, 2003. Google Scholar
  33. Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, and Josef Widder. Towards modeling and model checking fault-tolerant distributed algorithms. In International Symposium on Model Checking Software (SPIN'13), volume 7976 of LNCS, pages 209-226, 2013. Google Scholar
  34. Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. TLA+ model checking made symbolic. Proceedings of the ACM on Programming Languages, 3(OOPSLA):123:1-123:30, 2019. Google Scholar
  35. Igor Konnov, Marijana Lazic, Ilina Stoilkovska, and Josef Widder. Tutorial: Parameterized verification with byzantine model checker. In International Conference on Formal Techniques for (Networked and) Distributed Systems (FORTE'20), pages 189-207, 2020. Google Scholar
  36. Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder. Para^2: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Methods in System Design, 51(2):270-307, 2017. Google Scholar
  37. Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Symposium on Principles of Programming Languages (POPL'17), pages 719-734. ACM, 2017. Google Scholar
  38. Igor Konnov, Helmut Veith, and Josef Widder. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation, 252:95-109, 2017. Google Scholar
  39. Igor Konnov and Josef Widder. ByMC: Byzantine model checker. In ISoLA, pages 327-342, 2018. Google Scholar
  40. Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer. Inductive sequentialization of asynchronous programs. In ACM-SIGPLAN Symposium on Programming Language Design and Implementation (PLDI'20), pages 227-242, 2020. Google Scholar
  41. Leslie Lamport. Byzantizing paxos by refinement. In International Symposium on Distributed Computing (DISC'11), pages 211-224, 2011. Google Scholar
  42. Marijana Lazic, Igor Konnov, Josef Widder, and Roderick Bloem. Synthesis of distributed algorithms with parameterized threshold guards. In International Conference on Principles of Distributed Systems (OPODIS'17), pages 32:1-32:20, 2017. Google Scholar
  43. Richard J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717-721, 1975. Google Scholar
  44. Marta Lokhava, Giuliano Losa, David Mazières, Graydon Hoare, Nicolas Barry, Eli Gafni, Jonathan Jove, Rafał Malinowsky, and Jed McCaleb. Fast and secure global payments with stellar. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19, pages 80-96, 2019. Google Scholar
  45. Giuliano Losa and Mike Dodds. On the formal verification of the stellar consensus protocol. In Workshop on Formal Methods for Blockchains (FMBC@CAV'20), pages 9:1-9:9, 2020. Google Scholar
  46. Giuliano Losa, Eli Gafni, and David Mazières. Stellar consensus by instantiation. In Jukka Suomela, editor, 33rd International Symposium on Distributed Computing, DISC 2019, volume 146 of LIPIcs, pages 27:1-27:15, 2019. Google Scholar
  47. Andrew Miller, Yu Xia, Kyle Croman, Elaine Shi, and Dawn Song. The honey badger of BFT protocols. In Conference on Computer and Communications Security (CCS'16), 2016. Google Scholar
  48. Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs, and Borzoo Bonakdarpour. Parameterized synthesis of self-stabilizing protocols in symmetric networks. Acta Informatica, 57(1-2):271-304, 2020. Google Scholar
  49. Hadi Moloodi, Fathiyeh Faghih, and Borzoo Bonakdarpour. Parameterized distributed synthesis of fault-tolerance using counter abstraction. In Proceedings of the 40th International Symposium on Reliable Distributed Systems (SRDS), pages 67-77. IEEE, 2021. Google Scholar
  50. Achour Mostéfaoui, Hamouna Moumen, and Michel Raynal. Signature-free asynchronous Byzantine consensus with T < N/3 and O(N²) messages. In Symposium on Principles of Distributed Computing (PODC'14), pages 2-9, 2014. Google Scholar
  51. Achour Mostéfaoui, Hamouna Moumen, and Michel Raynal. Signature-free asynchronous binary Byzantine consensus with t < n/3, O(n²) messages and O(1) expected time. Journal of the ACM, 2015. Google Scholar
  52. Achour Mostéfaoui, Eric Mourgaya, Philippe Raipin Parvédy, and Michel Raynal. Evaluating the condition-based approach to solve consensus. In Dependable Systems and Networks (DSN'03), pages 541-550, 2003. Google Scholar
  53. Achour Mostéfaoui, Sergio Rajsbaum, and Michel Raynal. Conditions on input vectors for consensus solvability in asynchronous distributed systems. Journal of the ACM, 50(6):922-954, November 2003. Google Scholar
  54. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  55. Tatsuya Noguchi, Tatsuhiro Tsuchiya, and Tohru Kikuno. Safety verification of asynchronous consensus algorithms with model checking. In International Symposium on Dependable Computing (PRDC'12), pages 80-88, 2012. Google Scholar
  56. Marshall C. Pease, Robert E. Shostak, and Leslie Lamport. Reaching agreement in the presence of faults. Journal of the ACM, 27(2):228-234, 1980. Google Scholar
  57. Amir Pnueli. The temporal logic of programs. In IEEE Annual Symposium on Foundations of Computer Science (FOCS'77), pages 46-57, 1977. Google Scholar
  58. Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du congrès de Mathématiciens des Pays Slaves, pages 92-101, 1929. Google Scholar
  59. Vincent Rahli, David Guaspari, Mark Bickford, and Robert L. Constable. Formal specification, verification, and implementation of fault-tolerant systems using EventML. Electronic Communication of the European Association of Software Science and Technology, 72, 2015. Google Scholar
  60. Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Jorge Esteves Veríssimo. Velisarios: Byzantine fault-tolerant protocols powered by coq. In Amal Ahmed, editor, Proceedings of the 27th European Symposium on Programming (ESOP), volume 10801 of Lecture Notes in Computer Science, pages 619-650. Springer, 2018. Google Scholar
  61. Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru, and Sébastien Tixeuil. Parameterized verification of algorithms for oblivious robots on a ring. Formal Methods in System Design, 56(1):55-89, 2020. Google Scholar
  62. Ilya Sergey, James R. Wilcox, and Zachary Tatlock. Programming and proving with distributed protocols. Proceedings of the ACM on Programming Languages, 2(POPL):28:1-28:30, 2018. Google Scholar
  63. Yee Jiun Song and Robbert van Renesse. Bosco: One-step Byzantine asynchronous consensus. In International Symposium on Distributed Computing (DISC'08), pages 438-450, 2008. Google Scholar
  64. Ilina Stoilkovska, Igor Konnov, Josef Widder, and Florian Zuleger. Eliminating message counters in threshold automata. In International Symposium on Automated Technology for Verification and Analysis (ATVA'20), pages 196-212, 2020. Google Scholar
  65. Pierre Sutra. On the correctness of egalitarian paxos. Information Processing Letters, 156:105901, 2020. URL: https://doi.org/10.1016/j.ipl.2019.105901.
  66. Amer Tahat and Ali Ebnenasir. A hybrid method for the verification and synthesis of parameterized self-stabilizing protocols. In Maurizio Proietti and Hirohisa Seki, editors, 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), volume 8981 of Lecture Notes in Computer Science, pages 201-218. Springer, 2014. Google Scholar
  67. Pierre Tholoniat and Vincent Gramoli. Formal verification of blockchain Byzantine fault tolerance. In Workshop on Formal Reasoning in Distributed Algorithms (FRIDA'19), October 2019. URL: http://arxiv.org/abs/1909.07453.
  68. Tatsuhiro Tsuchiya and André Schiper. Using bounded model checking to verify consensus algorithms. In Gadi Taubenfeld, editor, Distributed Computing, pages 466-480, 2008. Google Scholar
  69. Tatsuhiro Tsuchiya and André Schiper. Verification of consensus algorithms using satisfiability solving. Distributed Computing, 23(5-6):341-358, 2011. Google Scholar
  70. Klaus von Gleissenthall, Rami Gökhan Kici, Alexander Bakst, Deian Stefan, and Ranjit Jhala. Pretend synchrony: synchronous verification of asynchronous distributed programs. Proceedings of the ACM on Programming Languages, 3(POPL):59:1-59:30, 2019. Google Scholar
  71. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson. Verdi: a framework for implementing and formally verifying distributed systems. In ACM-SIGPLAN Symposium on Programming Language Design and Implementation (PLDI'15), pages 357-368, 2015. Google Scholar
  72. Yuan Yu, Panagiotis Manolios, and Leslie Lamport. Model checking TLA^+ specifications. In CHARME, pages 54-66, 1999. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact