Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)

Authors Sean Braithwaite, Ethan Buchman, Igor Konnov , Zarko Milosevic , Ilina Stoilkovska, Josef Widder , Anca Zamfir



PDF
Thumbnail PDF

File

OASIcs.FMBC.2020.10.pdf
  • Filesize: 0.5 MB
  • 8 pages

Document Identifiers

Author Details

Sean Braithwaite
  • Informal Systems, Lausanne, Switzerland
Ethan Buchman
  • Informal Systems, Toronto, Canada
Igor Konnov
  • Informal Systems, Wien, Austria
Zarko Milosevic
  • Informal Systems, Lausanne, Switzerland
Ilina Stoilkovska
  • Informal Systems, Wien, Austria
Josef Widder
  • Informal Systems, Wien, Austria
Anca Zamfir
  • Informal Systems, Lausanne, Switzerland

Cite AsGet BibTex

Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, and Anca Zamfir. Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 10:1-10:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/OASIcs.FMBC.2020.10

Abstract

Blockchain synchronization is one of the core protocols of Tendermint blockchains. In this short paper, we discuss our recent efforts in formal specification of the protocol and its implementation, as well as some initial model checking results. We demonstrate that the protocol quality and understanding can be improved by writing specifications and model checking them.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
  • Software and its engineering → Software fault tolerance
  • Theory of computation → Logic and verification
Keywords
  • Blockchain
  • Fault Tolerance
  • Byzantine Faults
  • Model Checking

Metrics

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

References

  1. APALACHE: a symbolic model checker for TLAsuperscript+. https://github.com/konnov/apalache/, 2020. Last accessed: May 20, 2020.
  2. Ethan Buchman. Tendermint: Byzantine fault tolerance in the age of Blockchains. Master’s thesis, University of Guelph, 2016. URL: http://hdl.handle.net/10214/9769.
  3. Ethan Buchman and Jae Kwon. Cosmos whitepaper: a network of distributed ledgers, 2016. URL: https://cosmos.network/resources/whitepaper.
  4. Ethan Buchman, Jae Kwon, and Zarko Milosevic. The latest gossip on BFT consensus. arXiv preprint arXiv:1807.04938, 2018. URL: https://arxiv.org/abs/1807.04938.
  5. Vitalik Buterin and Virgil Griffith. Casper the friendly finality gadget. arXiv preprint arXiv:1710.09437, 2017. Google Scholar
  6. Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Consensus in the presence of partial synchrony. J.ACM, 35(2):288-323, 1988. Google Scholar
  7. Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. TLA+ model checking made symbolic. PACMPL, 3(OOPSLA):123:1-123:30, 2019. Google Scholar
  8. Markus Alexander Kuppe, Leslie Lamport, and Daniel Ricketts. The TLA+ toolbox. In F-IDE@FM 2019, pages 50-62, 2019. Google Scholar
  9. Jae Kwon. Tendermint: Consensus without mining. Draft v. 0.6, fall, 1(11), 2014. Google Scholar
  10. Informal Systems. Fastsync - English specification, 2020. URL: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/fastsync/fastsync.md.
  11. Informal Systems. Fastsync - TLA^+ specification, 2020. URL: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/fastsync/fastsync.tla.
  12. Informal Systems. Verification-Driven Development: An Informal Guide, 2020. URL: https://github.com/informalsystems/VDD/blob/master/guide/guide.md.
  13. ADR 043: Blockhchain reactor riri-org, 2020. URL: https://github.com/tendermint/tendermint/blob/master/docs/architecture/adr-043-blockchain-riri-org.md.
  14. Tendermint core, reference implementation in Go, 2020. URL: https://github.com/tendermint/tendermint.
  15. Maofan Yin, Dahlia Malkhi, Michael K Reiter, Guy Golan Gueta, and Ittai Abraham. Hotstuff: BFT consensus with linearity and responsiveness. In PODC, pages 347-356, 2019. 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