Document Open Access Logo

On the Formal Verification of the Stellar Consensus Protocol

Authors Giuliano Losa, Mike Dodds

PDF
Thumbnail PDF

File

OASIcs.FMBC.2020.9.pdf
  • Filesize: 397 kB
  • 9 pages

Document Identifiers

Author Details

Giuliano Losa
  • Galois, Inc., Portland, Oregon, USA
Mike Dodds
  • Galois, Inc., Portland, Oregon, USA

Funding

This work was supported by the Stellar Development Foundation.

Cite AsGet BibTex

Giuliano Losa and Mike Dodds. On the Formal Verification of the Stellar Consensus Protocol. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 9:1-9:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/OASIcs.FMBC.2020.9

Abstract

The Stellar Consensus Protocol (SCP) is a quorum-based BFT consensus protocol. However, instead of using threshold-based quorums, SCP is permissionless and its quorum system emerges from participants’ self-declared trust relationships. In this paper, we describe the methodology we deploy to formally verify the safety and liveness of SCP for arbitrary but fixed configurations. The proof uses a combination of Ivy and Isabelle/HOL. In Ivy, we model SCP in first-order logic, and we verify safety and liveness under eventual synchrony. In Isabelle/HOL, we prove the validity of our first-order encoding with respect to a more direct higher-order model. SCP is currently deployed in the Stellar Network, and we believe this is the first mechanized proof of both safety and liveness, specified in LTL, for a deployed BFT protocol.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
  • Networks → Protocol testing and verification
Keywords
  • Consensus
  • Blockchains
  • First-Order Logic
  • Stellar
  • Ivy Prover
  • Decidability

Metrics

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

References

  1. Ittai Abraham, Guy Gueta, Dahlia Malkhi, Lorenzo Alvisi, Rama Kotla, and Jean-Philippe Martin. Revisiting fast practical byzantine fault tolerance. arXiv preprint arXiv:1712.01367, 2017. Google Scholar
  2. Musab A Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña, and Grigore Roşu. Towards a verified model of the algorand consensus protocol in coq. arXiv preprint arXiv:1907.05523, 2019. Google Scholar
  3. Idan Berkovits, Marijana Lazić, Giuliano Losa, Oded Padon, and Sharon Shoham. Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification, Lecture Notes in Computer Science, pages 245-266, Cham, 2019. Springer International Publishing. Google Scholar
  4. Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Consensus in the presence of partial synchrony. Journal of the ACM (JACM), 35(2):288-323, 1988. Google Scholar
  5. Yeting Ge and Leonardo De Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Computer Aided Verification, pages 306-320. Springer, 2009. Google Scholar
  6. Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. IronFleet: Proving Practical Distributed Systems Correct. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP '15, pages 1-17, New York, NY, USA, 2015. ACM. Google Scholar
  7. 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, New York, NY, USA, October 2019. Association for Computing Machinery. Google Scholar
  8. Giuliano Losa. https://github.com/stellar/scp-proofs, 2019.
  9. 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 Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1-27:15, Dagstuhl, Germany, 2019. Schloss Dagstuhlendash Leibniz-Zentrum fuer Informatik. Google Scholar
  10. Kenneth L. McMillan and Oded Padon. Deductive verification in decidable fragments with Ivy. In International Static Analysis Symposium, pages 43-55. Springer, 2018. Google Scholar
  11. Ryuya Nakamura, Takayuki Jimba, and Dominik Harz. Refinement and Verification of CBC Casper. In 2019 Crypto Valley Conference on Blockchain Technology (CVCBT), pages 26-38, June 2019. Google Scholar
  12. Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. Reducing Liveness to Safety in First-Order Logic. In 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018), Los Angeles, 2018. Google Scholar
  13. Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. Temporal prophecy for proving temporal properties of infinite-state systems. In 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1-11. IEEE, 2018. Google Scholar
  14. Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. Paxos Made EPR: Decidable Reasoning About Distributed Protocols. Proc. ACM Program. Lang., 1(OOPSLA):108:1-108:31, October 2017. Google Scholar
  15. Karl Palmskog, Milos Gligoric, Brandon Moore, Lucas Peña, and Grigore Roşu. Verification of Casper in the Coq Proof Assistant, 2018. URL: http://hdl.handle.net/2142/102075.
  16. Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Esteves-Verissimo. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Amal Ahmed, editor, Programming Languages and Systems, Lecture Notes in Computer Science, pages 619-650, Cham, 2018 . Springer International Publishing. Google Scholar
  17. Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. Modularity for decidability of deductive verification with applications to distributed systems. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pages 662-677, New York, NY, USA, June 2018. Association for Computing Machinery. 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