Document Open Access Logo

Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol

Authors M. Praveen , Raghavendra Ramesh , Isaac Doidge

PDF
Thumbnail PDF

File

OASIcs.FMBC.2024.3.pdf
  • Filesize: 0.62 MB
  • 16 pages

Document Identifiers

Author Details

M. Praveen
  • Chennai Mathematical Institute, India
  • ReLaX, Chennai, India
Raghavendra Ramesh
  • Supra Research, Brisbane, Australia
Isaac Doidge
  • Supra Research, Brisbane, Australia

Funding

  • Praveen, M.: Funded by Supra

Acknowledgements

We acknowledge and thank Chandradeep Dey and Namrata Reddy, who were part of this project during its initial phase. We acknowledge Supra Research for funding M. Praveen, the academic partner of this project and providing other support.

Cite AsGet BibTex

M. Praveen, Raghavendra Ramesh, and Isaac Doidge. Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/OASIcs.FMBC.2024.3

Abstract

Decentralized Finance (DeFi) has emerged as a contemporary competitive as well as complementary to traditional centralized finance systems. As of 23rd January 2024, per Defillama approximately USD 55 billion is the total value locked on the DeFi applications on all blockchains put together. A Byzantine Fault Tolerant (BFT) State Machine Replication (SMR) protocol, popularly known as the consensus protocol, is the central component of a blockchain. If forks are possible in a consensus protocol, they can be misused to carry out double spending attacks and can be catastrophic given high volumes of finance that are transacted on blockchains. Formal verification of the safety of consensus protocols is the golden standard for guaranteeing that forks are not possible. However, it is considered complex and challenging to do. This is reflected by the fact that not many complex consensus protocols are formally verified except for Tendermint and QBFT. We focus on Supra’s Pipelined Moonshot consensus protocol. Similar to Tendermint’s formal verification, we too model Pipelined Moonshot using IVy and formally prove that for all network sizes, as long as the number of Byzantine validators is less than 1/3, the protocol does not allow forks, thus proving that Pipelined Moonshot is safe and double spending cannot be done using forks. The IVy model and proof of safety is available on y. https://github.com/Entropy-Foundation/suprabft-fv/tree/master/suprabft.

Subject Classification

ACM Subject Classification
  • Networks → Protocol testing and verification
  • Theory of computation → Logic and verification
  • Theory of computation → Automated reasoning
Keywords
  • Blockchain consensus
  • Safety
  • Formal verification

Metrics

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

Supplementary Materials

References

  1. IVy modeling of Pipelined Moonshot and its proof of safety. URL: https://github.com/Entropy-Foundation/suprabft-fv/tree/master/suprabft.
  2. SPIN. URL: https://spinroot.com/spin/whatispin.html.
  3. TLA+. URL: https://lamport.azurewebsites.net/tla/tla.html.
  4. Defillama. https://galois.com/blog/2021/07/formally-verifying-the-tendermint-blockchain-protocol/, 2021.
  5. Formal Verification of QBFT Safety. https://github.com/Consensys/qbft-formal-spec-and-verification, 2021.
  6. Defillama. https://defillama.com, 2024.
  7. Moonshot Formal Verification in IVy - GitHub Repository. https://github.com/Entropy-Foundation/suprabft-fv/tree/master/suprabft, 2024.
  8. Z3 SMT Solver. https://www.microsoft.com/en-us/research/project/z3-3/, 2024.
  9. 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. In Bruno Bernardo and Diego Marmsoler, editors, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020), volume 84 of Open Access Series in Informatics (OASIcs), pages 10:1-10:8, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/OASIcs.FMBC.2020.10.
  10. Ethan Buchman. Tendermint: Byzantine fault tolerance in the age of blockchains. PhD thesis, University of Guelph, 2016. Google Scholar
  11. Miguel Castro, Barbara Liskov, et al. Practical byzantine fault tolerance. In OSDI, volume 99, pages 173-186, 1999. URL: https://dl.acm.org/citation.cfm?id=296824.
  12. Isaac Doidge, Raghavendra Ramesh, Nibesh Shrestha, and Joshua Tobkin. Moonshot: Optimizing chain-based rotating leader bft via optimistic proposals, 2024. URL: https://doi.org/10.48550/arXiv.2401.01791.
  13. Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Consensus in the presence of partial synchrony. J. ACM, 35(2):288-323, apr 1988. URL: https://doi.org/10.1145/42282.42283.
  14. Yotam MY Feldman, James R Wilcox, Sharon Shoham, and Mooly Sagiv. Inferring inductive invariants from phase structures. In Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II 31, pages 405-425. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_23.
  15. Rati Gelashvili, Lefteris Kokoris-Kogias, Alberto Sonnino, Alexander Spiegelman, and Zhuolun Xiang. Jolteon and ditto: Network-adaptive efficient consensus with asynchronous fallback. In FC, pages 296-315, 2022. URL: https://doi.org/10.1007/978-3-031-18283-9_14.
  16. Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. Tla+ model checking made symbolic. Proc. ACM Program. Lang., 3(OOPSLA), oct 2019. URL: https://doi.org/10.1145/3360549.
  17. Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17, pages 719-734, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3009837.3009860.
  18. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 348-370, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-17511-4_20.
  19. Kenneth L. McMillan and Oded Padon. Deductive verification in decidable fragments with ivy. In Andreas Podelski, editor, Static Analysis, pages 43-55, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-99725-4_4.
  20. Henrique Moniz. The istanbul bft consensus algorithm, 2020. URL: https://doi.org/10.48550/arXiv.2002.03613.
  21. Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang., 2(POPL), 2017. URL: https://doi.org/10.1145/3158114.
  22. Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: safety verification by interactive generalization. SIGPLAN Not., 51(6):614-630, jun 2016. URL: https://doi.org/10.1145/2980983.2908118.
  23. Supra Research. Moonshot: Optimistic proposal for blockchain-based state machine replication. URL: https://supraoracles.com/news/moonshot-consensus/.
  24. Ion Stoica, Robert Morris, David Karger, M. Frans Kaashoek, and Hari Balakrishnan. Chord: A scalable peer-to-peer lookup service for internet applications. In Proceedings of the 2001 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, SIGCOMM '01, pages 149-160, New York, NY, USA, 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/383059.383071.
  25. Pierre Tholoniat and Vincent Gramoli. Formal Verification of Blockchain Byzantine Fault Tolerance, pages 389-412. Springer International Publishing, Cham, 2022. URL: https://doi.org/10.1007/978-3-031-07535-3_12.
  26. Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala. Pretend synchrony: synchronous verification of asynchronous distributed programs. Proc. ACM Program. Lang., 3(POPL), jan 2019. URL: https://doi.org/10.1145/3290372.
  27. 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. URL: https://doi.org/10.1145/3293611.3331591.
  28. Yuan Yuan, Zeng Fanping, Zhu Guanmiao, Deng Chaoqiang, and Xiong Neng. Test case generation based on program invariant and adaptive random algorithm. In Advances in Information Technology and Education: International Conference, CSE 2011, Qingdao, China, July 9-10, 2011, Proceedings, Part I, pages 274-282. Springer, 2011. Google Scholar
  29. Pamela Zave. Using lightweight modeling to understand chord. SIGCOMM Comput. Commun. Rev., 42(2):49-57, mar 2012. URL: https://doi.org/10.1145/2185376.2185383.
  30. Fanping Zeng, Qing Cao, Liangliang Mao, and Zhide Chen. Test case generation based on invariant extraction. In 2009 5th International Conference on Wireless Communications, Networking and Mobile Computing, pages 1-4. IEEE, 2009. 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