OASIcs.FMBC.2020.10.pdf
- Filesize: 0.5 MB
- 8 pages
Document
Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)
Authors
Igor Konnov 
,
Zarko Milosevic ,
Josef Widder ,
-
Part of:
Volume:
2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Series: Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-12-11
File
Document Identifiers
Author Details
Cite As Get 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)
0PDF Downloads
References
- APALACHE: a symbolic model checker for TLAsuperscript+. https://github.com/konnov/apalache/, 2020. Last accessed: May 20, 2020.
- 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.
- Ethan Buchman and Jae Kwon. Cosmos whitepaper: a network of distributed ledgers, 2016. URL: https://cosmos.network/resources/whitepaper.
- 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.
-
Vitalik Buterin and Virgil Griffith. Casper the friendly finality gadget. arXiv preprint arXiv:1710.09437, 2017.
-
Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Consensus in the presence of partial synchrony. J.ACM, 35(2):288-323, 1988.
-
Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. TLA+ model checking made symbolic. PACMPL, 3(OOPSLA):123:1-123:30, 2019.
-
Markus Alexander Kuppe, Leslie Lamport, and Daniel Ricketts. The TLA+ toolbox. In F-IDE@FM 2019, pages 50-62, 2019.
-
Jae Kwon. Tendermint: Consensus without mining. Draft v. 0.6, fall, 1(11), 2014.
- Informal Systems. Fastsync - English specification, 2020. URL: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/fastsync/fastsync.md.
- Informal Systems. Fastsync - TLA^+ specification, 2020. URL: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/fastsync/fastsync.tla.
- Informal Systems. Verification-Driven Development: An Informal Guide, 2020. URL: https://github.com/informalsystems/VDD/blob/master/guide/guide.md.
- ADR 043: Blockhchain reactor riri-org, 2020. URL: https://github.com/tendermint/tendermint/blob/master/docs/architecture/adr-043-blockchain-riri-org.md.
- Tendermint core, reference implementation in Go, 2020. URL: https://github.com/tendermint/tendermint.
-
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.