[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article
Open access

LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs

Published: 20 June 2024 Publication History

Abstract

Byzantine fault-tolerant state machine replication (SMR) protocols, such as PBFT, HotStuff, and Jolteon, are essential for modern blockchain technologies. However, they are challenging to implement correctly because they have to deal with any unexpected message from byzantine peers and ensure safety and liveness at all times. Many formal frameworks have been developed to verify the safety of SMR implementations, but there is still a gap in the verification of their liveness. Existing liveness proofs are either limited to the network level or do not cover popular partially synchronous protocols.
We introduce LiDO, a consensus model that enables the verification of both safety and liveness of implementations through refinement. We observe that current consensus models cannot handle liveness because they do not include a pacemaker state. We show that by adding a pacemaker state to the LiDO model, we can express the liveness properties of SMR protocols as a few safety properties that can be easily verified by refinement proofs. Based on our LiDO model, we provide mechanized safety and liveness proofs for both unpipelined and pipelined Jolteon in Coq. This is the first mechanized liveness proof for a byzantine consensus protocol with non-trivial optimizations such as pipelining.

References

[1]
Mark Abspoel, Thomas Attema, and Matthieu Rambaud. 2021. Brief Announcement: Malicious Security Comes for Free in Consensus with Leaders. In Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing (PODC’21). Association for Computing Machinery, New York, NY, USA. 195–198. isbn:9781450385480 https://doi.org/10.1145/3465084.3467953
[2]
Idan Berkovits, Marijana Lazić, Giuliano Losa, Oded Padon, and Sharon Shoham. 2019. Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham. 245–266. isbn:978-3-030-25543-5 https://doi.org/10.1007/978-3-030-25543-5_15
[3]
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić, Pierre Tholoniat, and Josef Widder. 2022. Holistic Verification of Blockchain Consensus. In 36th International Symposium on Distributed Computing (DISC 2022), Christian Scheideler (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 246). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 10:1–10:24. isbn:978-3-95977-255-6 issn:1868-8969 https://doi.org/10.4230/LIPIcs.DISC.2022.10
[4]
Alysson Bessani, João Sousa, and Eduardo E. P. Alchieri. 2014. State Machine Replication for the Masses with BFT-SMaRt. In Proceedings of the IEEE/IFIP International Conference on Dependable Systems and Networks (DSN ’14). IEEE Computer Society, Washington, DC, USA. 355–362. https://doi.org/10.1109/DSN.2014.43
[5]
Manuel Bravo, Gregory V. Chockler, and Alexey Gotsman. 2022. Liveness and Latency of Byzantine State-Machine Replication. In 36th International Symposium on Distributed Computing, DISC 2022, October 25-27, 2022, Augusta, Georgia, USA, Christian Scheideler (Ed.) (LIPIcs, Vol. 246). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 12:1–12:19. https://doi.org/10.4230/LIPIcs.DISC.2022.12
[6]
Vitalik Buterin, Diego Hernandez, Thor Kamphefner, Khiem Pham, Zhi Qiao, Danny Ryan, Juhyeok Sin, Ying Wang, and Yan X Zhang. 2020. Combining GHOST and Casper. arxiv:2003.03052.
[7]
Harold Carr, Christa Jenkins, Mark Moir, Victor Cacciari Miraldo, and Lisandra Silva. 2022. Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda. In NASA Formal Methods, Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing, Cham. 616–635. isbn:978-3-031-06773-0 https://doi.org/10.1007/978-3-031-06773-0_33
[8]
Miguel Castro. 2001. Practical Byzantine Fault Tolerance. Ph. D. Dissertation. Massachusetts Institute of Technology. https://www.microsoft.com/en-us/research/wp-content/uploads/2017/01/thesis-mcastro.pdf
[9]
Berk Cirisci, Constantin Enea, and Suha Orhun Mutluergil. 2023. Quorum Tree Abstractions of Consensus Protocols. In Programming Languages and Systems, Thomas Wies (Ed.). Springer Nature Switzerland, Cham. 337–362. isbn:978-3-031-30044-8 https://doi.org/10.1007/978-3-031-30044-8_13
[10]
Pierre Civit, Muhammad Ayaz Dzulfikar, Seth Gilbert, Vincent Gramoli, Rachid Guerraoui, Jovan Komatovic, and Manuel Vidigueira. 2022. Byzantine Consensus Is Θ (n^2): The Dolev-Reischuk Bound Is Tight Even in Partial Synchrony!. In 36th International Symposium on Distributed Computing (DISC 2022), Christian Scheideler (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 246). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 14:1–14:21. isbn:978-3-95977-255-6 issn:1868-8969 https://doi.org/10.4230/LIPIcs.DISC.2022.14
[11]
Francesco D’Amato, Joachim Neu, Ertem Nusret Tas, and David Tse. 2023. Goldfish: No More Attacks on Ethereum?!. arxiv:2209.03255.
[12]
D. Dolev and A. Yao. 1983. On the security of public key protocols. IEEE Transactions on Information Theory, 29, 2 (1983), 198–208. https://doi.org/10.1109/TIT.1983.1056650
[13]
Cezara Drăgoi, Thomas A. Henzinger, and Damien Zufferey. 2016. PSync: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). Association for Computing Machinery, New York, NY, USA. 400–415. isbn:9781450335492 https://doi.org/10.1145/2837614.2837650
[14]
Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. 1988. Consensus in the Presence of Partial Synchrony. Journal of the ACM, 35, 2 (1988), April, 288–323. https://doi.org/10.1145/42282.42283
[15]
Rati Gelashvili, Lefteris Kokoris-Kogias, Alberto Sonnino, Alexander Spiegelman, and Zhuolun Xiang. 2022. Jolteon and Ditto: Network-Adaptive Efficient Consensus with Asynchronous Fallback. In Financial Cryptography and Data Security, Ittay Eyal and Juan Garay (Eds.). Springer International Publishing, Cham. 296–315. isbn:978-3-031-18283-9 https://doi.org/10.1007/978-3-031-18283-9_14
[16]
Neil Giridharan, Florian Suri-Payer, Matthew Ding, Heidi Howard, Ittai Abraham, and Natacha Crooks. 2023. BeeGees: Stayin’ Alive in Chained BFT. In Proceedings of the 2023 ACM Symposium on Principles of Distributed Computing (PODC ’23). Association for Computing Machinery, New York, NY, USA. 233–243. isbn:9798400701214 https://doi.org/10.1145/3583668.3594572
[17]
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: Proving Practical Distributed Systems Correct. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP ’15). Association for Computing Machinery, New York, NY, USA. 1–17. isbn:9781450338349 https://doi.org/10.1145/2815400.2815428
[18]
Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst., 12, 3 (1990), jul, 463–492. issn:0164-0925 https://doi.org/10.1145/78969.78972
[19]
Wolf Honoré, Jieung Kim, Ji-Yong Shin, and Zhong Shao. 2021. Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems. Proc. ACM Program. Lang., 5, OOPSLA (2021), Article 97, oct, 31 pages. https://doi.org/10.1145/3485474
[20]
Wolf Honoré, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, and Zhong Shao. 2024. AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. Proc. ACM Program. Lang., 8, OOPSLA1 (2024), Article 109, apr, 30 pages. https://doi.org/10.1145/3649826
[21]
Wolf Honoré, Ji-Yong Shin, Jieung Kim, and Zhong Shao. 2022. Adore: Atomic Distributed Objects with Certified Reconfiguration. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022). Association for Computing Machinery, New York, NY, USA. 379–394. isbn:9781450392655 https://doi.org/10.1145/3519939.3523444
[22]
Mahimna Kelkar, Fan Zhang, Steven Goldfeder, and Ari Juels. 2020. Order-Fairness for Byzantine Consensus. In Advances in Cryptology – CRYPTO 2020, Daniele Micciancio and Thomas Ristenpart (Eds.). Springer International Publishing, Cham. 451–480. isbn:978-3-030-56877-1 https://doi.org/10.1007/978-3-030-56877-1_16
[23]
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal. 2020. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. In Programming Languages and Systems, Peter Müller (Ed.). Springer International Publishing, Cham. 336–365. isbn:978-3-030-44914-8 https://doi.org/10.1007/978-3-030-44914-8_13
[24]
Klaus Kursawe. 2020. Wendy, the Good Little Fairness Widget: Achieving Order Fairness for Blockchains. In Proceedings of the 2nd ACM Conference on Advances in Financial Technologies (AFT ’20). Association for Computing Machinery, New York, NY, USA. 25–36. isbn:9781450381390 https://doi.org/10.1145/3419614.3423263
[25]
Leslie Lamport. 1998. The Part-Time Parliament. ACM Trans. Comput. Syst., 16, 2 (1998), may, 133–169. issn:0734-2071 https://doi.org/10.1145/279227.279229
[26]
Leslie Lamport. 2005. Real Time is Really Simple. 72. https://www.microsoft.com/en-us/research/publication/real-time-is-really-simple/
[27]
Andrew Lewis-Pye. 2022. Quadratic worst-case message complexity for State Machine Replication in the partial synchrony model. CoRR, abs/2201.01107 (2022), arXiv:2201.01107.
[28]
Giuliano Losa and Mike Dodds. 2020. On the Formal Verification of the Stellar Consensus Protocol. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020), Bruno Bernardo and Diego Marmsoler (Eds.) (OpenAccess Series in Informatics (OASIcs), Vol. 84). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 9:1–9:9. isbn:978-3-95977-169-6 issn:2190-6807 https://doi.org/10.4230/OASIcs.FMBC.2020.9
[29]
Dahlia Malkhi and Kartik Nayak. 2023. Extended Abstract: HotStuff-2: Optimal Two-Phase Responsive BFT. Cryptology ePrint Archive, Paper 2023/397. https://eprint.iacr.org/2023/397
[30]
Oded Naor, Mathieu Baudet, Dahlia Malkhi, and Alexander Spiegelman. 2021. Cogsworth: Byzantine View Synchronization. Cryptoeconomic Systems, 1, 2 (2021), oct 22, https://doi.org/10.21428/58320208.08912a03
[31]
Oded Naor and Idit Keidar. 2020. Expected Linear Round Synchronization: The Missing Link for Linear Byzantine SMR. In 34th International Symposium on Distributed Computing (DISC 2020), Hagit Attiya (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 179). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 26:1–26:17. isbn:978-3-95977-168-9 issn:1868-8969 https://doi.org/10.4230/LIPIcs.DISC.2020.26
[32]
Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning. Theoretical Computer Science, 375, 1 (2007), 271–307. issn:0304-3975 https://doi.org/10.1016/j.tcs.2006.12.035 Festschrift for John C. Reynolds’s 70th birthday
[33]
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. 2017. Reducing Liveness to Safety in First-Order Logic. Proc. ACM Program. Lang., 2, POPL (2017), Article 26, dec, 33 pages. https://doi.org/10.1145/3158114
[34]
Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honoré, and Zhong Shao. 2024. Artifact for PLDI 2024 paper # 290: LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. https://doi.org/10.5281/zenodo.10909272
[35]
Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honoré, and Zhong Shao. 2024. LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. Yale Univ. https://flint.cs.yale.edu/publications/lido.html
[36]
Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Esteves-Verissimo. 2018. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham. 619–650. isbn:978-3-319-89884-1 https://doi.org/10.1007/978-3-319-89884-1_22
[37]
Fred B. Schneider. 1990. Implementing Fault-Tolerant Services Using the State Machine Approach: A Tutorial. ACM Comput. Surv., 22, 4 (1990), dec, 299–319. issn:0360-0300 https://doi.org/10.1145/98163.98167
[38]
Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2017. Programming and Proving with Distributed Protocols. Proc. ACM Program. Lang., 2, POPL (2017), Article 28, dec, 30 pages. https://doi.org/10.1145/3158116
[39]
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, Frans Kaashoek, and Nickolai Zeldovich. 2023. Grove: A Separation-Logic Library for Verifying Distributed Systems. In Proceedings of the 29th Symposium on Operating Systems Principles (SOSP ’23). Association for Computing Machinery, New York, NY, USA. 113–129. isbn:9798400702297 https://doi.org/10.1145/3600006.3613172
[40]
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for Decidability of Deductive Verification with Applications to Distributed Systems. SIGPLAN Not., 53, 4 (2018), jun, 662–677. issn:0362-1340 https://doi.org/10.1145/3296979.3192414
[41]
Søren Eller Thomsen and Bas Spitters. 2021. Formalizing Nakamoto-Style Proof of Stake. In 2021 IEEE 34th Computer Security Foundations Symposium (CSF). 1–15. https://doi.org/10.1109/CSF51468.2021.00042
[42]
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. 2015. Verdi: A Framework for Implementing and Formally Verifying Distributed Systems. SIGPLAN Not., 50, 6 (2015), jun, 357–368. issn:0362-1340 https://doi.org/10.1145/2813885.2737958
[43]
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson. 2016. Planning for Change in a Formal Verification of the Raft Consensus Protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016). Association for Computing Machinery, New York, NY, USA. 154–165. isbn:9781450341271 https://doi.org/10.1145/2854065.2854081
[44]
Maofan Yin, Dahlia Malkhi, Michael K. Reiter, Guy Golan Gueta, and Ittai Abraham. 2019. HotStuff: BFT Consensus with Linearity and Responsiveness. In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing (PODC ’19). Association for Computing Machinery, New York, NY, USA. 347–356. isbn:9781450362177 https://doi.org/10.1145/3293611.3331591

Cited By

View all
  • (2024)Compositional Verification of Composite Byzantine ProtocolsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690355(34-48)Online publication date: 2-Dec-2024

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages  Volume 8, Issue PLDI
June 2024
2198 pages
EISSN:2475-1421
DOI:10.1145/3554317
Issue’s Table of Contents
This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 June 2024
Published in PACMPL Volume 8, Issue PLDI

Permissions

Request permissions for this article.

Check for updates

Badges

Author Tags

  1. byzantine fault-tolerance
  2. consensus protocols
  3. distributed systems
  4. formal verification
  5. liveness
  6. proof assistants
  7. refinement
  8. safety

Qualifiers

  • Research-article

Funding Sources

  • National Science Foundation
  • Defense Advanced Research Projects Agency

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)305
  • Downloads (Last 6 weeks)45
Reflects downloads up to 01 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Compositional Verification of Composite Byzantine ProtocolsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690355(34-48)Online publication date: 2-Dec-2024

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media