More Web Proxy on the site http://driver.im/

research-article

Open access

AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects

Authors:

Zhong ShaoAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 8, Issue OOPSLA1

Article No.: 109, Pages 419 - 448

https://doi.org/10.1145/3649826

Published: 29 April 2024 Publication History

Abstract

Achieving consensus is a challenging and ubiquitous problem in distributed systems that is only made harder by the introduction of malicious byzantine servers. While significant effort has been devoted to the benign and byzantine failure models individually, no prior work has considered the mechanized verification of both in a generic way. We claim this is due to the lack of an appropriate abstraction that is capable of representing both benign and byzantine consensus without either losing too much detail or becoming impractically complex. We build on recent work on the atomic distributed object model to fill this void with a novel abstraction called AdoB. In addition to revealing important insights into the essence of consensus, this abstraction has practical benefits for easing distributed system verification. As a case study, we proved safety and liveness properties for AdoB in Coq, which are the first such mechanized proofs to handle benign and byzantine consensus in a unified manner. We also demonstrate that AdoB faithfully models real consensus protocols by proving it is refined by standard network-level specifications of Fast Paxos and a variant of Jolteon.

References

[1]

Ittai Abraham, Heidi Howard, and Kartik Nayak. 2021. Benign HotStuff. https://decentralizedthoughts.github.io/2021-04-02-benign-hotstuff/

[2]

Agda Development Team. 2005–2022. What is Agda? https://agda.readthedocs.io/en/latest/getting-started/what-is-agda.html

[3]

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.) (CAV ’19). Springer International Publishing, Cham. 245–266. https://doi.org/10.1007/978-3-030-25543-5_15

[4]

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-39597-7-2-5-5-6 issn:1868-8969 https://doi.org/10.4230/LIPIcs.DISC.2022.10

[5]

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

Digital Library

[6]

Manuel Bravo, Gregory Chockler, and Alexey Gotsman. 2020. Making Byzantine Consensus Live. In Proc. of the 34th International Symposium on Distributed Computing (DISC ’20). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany. https://doi.org/10.4230/LIPIcs.DISC.2020.23

[7]

Ethan Buchman. 2016. Tendermint: Byzantine Fault Tolerance in the Age of Blockchains. Ph. D. Dissertation. University of Guelph.

[8]

Ethan Buchman, Jae Kwon, and Zarko Milosevic. 2019. The Latest Gossip on BFT Consensus. arxiv:1807.04938.

[9]

Mike Burrows. 2006. The Chubby Lock Service for Loosely-Coupled Distributed Systems. In Proc. of the 7th Symposium on Operating Systems Design and Implementation (OSDI ’06). USENIX Association, Berkeley, CA, USA. 335–350. https://dl.acm.org/doi/10.5555/1298455.1298487

Digital Library

[10]

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.) (NFM ’22). Springer-Verlag, Berlin, Heidelberg. 616–635. https://doi.org/10.1007/978-3-031-06773-0_33

Digital Library

[11]

Miguel Castro and Barbara Liskov. 1999. Practical Byzantine Fault Tolerance. In Proc. of the 3rd Symposium on Operating Systems Design and Implementation (OSDI ’99). USENIX Association, Berkeley, CA, USA. 173–186. http://dl.acm.org/citation.cfm?id=296806.296824

[12]

Fay Chang, Jeffrey Dean, Sanjay Ghemawat, Wilson C. Hsieh, Deborah A. Wallach, Mike Burrows, Tushar Chandra, Andrew Fikes, and Robert E. Gruber. 2006. Bigtable: A Distributed Storage System for Structured Data. In Proc. of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI ’06). ACM, New York, NY, USA. 205–218. https://doi.org/10.1145/1365815.1365816

Digital Library

[13]

Kaustuv C Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. 2008. A TLA+ Proof System. In Workshop on Knowledge Exchange: Automated Provers and Proof Assistants, Renate Schmidt Stephan Schulz, Piotr Rudnicki, Geoff Sutcliffe, Boris Konev (Ed.) (KEAPPA ’08, Vol. 418). CEUR-WS.org, online. 17–37. http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-418/paper2.pdf

[14]

Berk Cirisci, Constantin Enea, and Suha Orhun Mutluergil. 2023. Quorum Tree Abstractions of Consensus Protocols. In Proc. of the 32nd European Symposium on Programming, Thomas Wies (Ed.) (ESOP ’23). Springer Nature Switzerland, Cham. 337–362. https://doi.org/10.1007/978-3-031-30044-8_13

Digital Library

[15]

Coq Development Team. 1999–2022. The Coq Proof Assistant. http://coq.inria.fr

[16]

Jeff Dean. 2009. Designs, Lessons and Advice from Building Large Distributed Systems. https://research.cs.cornell.edu/ladis2009/talks/dean-keynote-ladis2009.pdf Keynote from ACM SIGOPS International Workshop on Large Scale Distributed Systems and Middleware

[17]

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

Digital Library

[18]

etcd Authors. 2013–2022. etcd. https://etcd.io/

[19]

Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. 1985. Impossibility of Distributed Consensus with One Faulty Process. Journal of the ACM, 32, 2 (1985), April, 374–382. https://doi.org/10.1145/3149.214121

Digital Library

[20]

Rati Gelashvili, Lefteris Kokoris-Kogias, Alberto Sonnino, Alexander Spiegelman, and Zhuolun Xiang. 2022. Jolteon and Ditto: Network-Adaptive Efficient Consensus with Asynchronous Fallback. In Proc. of the 26th International Conference on Financial Cryptography and Data Security (FC ’22). Springer-Verlag, Berlin, Heidelberg. https://fc22.ifca.ai/preproceedings/35.pdf

Digital Library

[21]

Sanjay Ghemawat, Howard Gobioff, and Shun-Tak Leung. 2003. The Google File System. In Proc. of the 19th ACM Symposium on Operating Systems Principles (SOSP ’03). ACM, New York, NY, USA. 29–43. https://doi.org/10.1145/945445.945450

Digital Library

[22]

Yossi Gilad, Rotem Hemo, Silvio Micali, Georgios Vlachos, and Nickolai Zeldovich. 2017. Algorand: Scaling Byzantine Agreements for Cryptocurrencies. In Proceedings of the Symposium on Operating Systems Principles (SOSP ’17). ACM, New York, NY, USA. 51–68. https://doi.org/10.1145/3132747.3132757

Digital Library

[23]

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 Proc. of the 25th Symposium on Operating Systems Principles (SOSP ’15). ACM, New York, NY, USA. 1–17. https://doi.org/10.1145/2815400.2815428

Digital Library

[24]

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), Oct., https://doi.org/10.1145/3485474

Digital Library

[25]

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. Yale Univ. https://flint.cs.yale.edu/publications/adob.html

[26]

Wolf Honoré, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, and Zhong Shao. 2024. Artifact For "AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects". https://doi.org/10.5281/zenodo.10727570

[27]

Wolf Honoré, Ji-Yong Shin, Jieung Kim, and Zhong Shao. 2022. Adore: Atomic Distributed Objects with Certified Reconfiguration. In Proc. of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’22). ACM, New York, NY, USA. 379–394. https://doi.org/10.1145/3519939.3523444

Digital Library

[28]

Patrick Hunt, Mahadev Konar, Flavio Paiva Junqueira, and Benjamin Reed. 2010. ZooKeeper: Wait-Free Coordination for Internet-Scale Systems. In Proc. of the 2010 USENIX Conference on USENIX Annual Technical Conference (USENIXATC ’10). USENIX Association, Berkeley, CA, USA. 11. https://doi.org/10.5555/1855840.1855851

Digital Library

[29]

Isabelle Development Team. 1986–2022. What is Isabelle? https://isabelle.in.tum.de/overview.html

[30]

Leslie Lamport. 1994. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16, 3 (1994), May, 872–923. https://doi.org/10.1145/177492.177726

Digital Library

[31]

Leslie Lamport. 1998. The Part-Time Parliament. ACM Trans. Comput. Syst., 16, 2 (1998), 133–169. https://doi.org/10.1145/279227.279229

Digital Library

[32]

Leslie Lamport. 2006. Fast Paxos. Distributed Computing, 19, 2 (2006), 79–103. https://doi.org/10.1007/s00446-006-0005-x

Digital Library

[33]

Leslie Lamport. 2011. Byzantizing Paxos by Refinement. In Proc. of the 25th International Conference on Distributed Computing (DISC ’11). Springer-Verlag, Berlin, Heidelberg. 211–224. https://doi.org/10.5555/2075029.2075058

Digital Library

[34]

Leslie Lamport, Robert Shostak, and Marshall Pease. 1982. The Byzantine Generals Problem. ACM Transactions on Programming Languages and Systems, July, 382–401. https://doi.org/10.1145/357172.357176

Digital Library

[35]

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Proc. of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M. Clarke and Andrei Voronkov (Eds.) (LPAR ’10). Springer-Verlag, Berlin, Heidelberg. 348–370. https://doi.org/10.1007/978-3-642-17511-4_20

[36]

Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguiça, and Rodrigo Rodrigues. 2012. Making Geo-Replicated Systems Fast as Possible, Consistent when Necessary. In 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI ’12). USENIX Association, Hollywood, CA. 265–278. https://www.usenix.org/conference/osdi12/technical-sessions/presentation/li

[37]

Giuliano Losa and Mike Dodds. 2020. On the Formal Verification of the Stellar Consensus Protocol. In Proc. of the 2nd Workshop on Formal Methods for Blockchains, Bruno Bernardo and Diego Marmsoler (Eds.) (FMBC ’20, Vol. 84). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 1–9. https://doi.org/10.4230/OASIcs.FMBC.2020.9

[38]

David Mazieres. 2015. The Stellar Consensus Protocol: A Federated Model for Internet-Level Consensus. https://www.stellar.org/papers/stellar-consensus-protocol

[39]

Satoshi Nakamoto. 2008. Bitcoin: A Peer-to-Peer Electronic Cash System. Decentralized Business Review.

[40]

Diego Ongaro and John K. Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In USENIX Annual Technical Conference. USENIX Association, Berkeley, CA, USA. 305–319. https://dl.acm.org/doi/10.5555/2643634.2643666

[41]

Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. 2018. Reducing Liveness to Safety in First-Order Logic. Proc. ACM Program. Lang., 2, POPL (2018), Jan., https://doi.org/10.1145/3158114

Digital Library

[42]

Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: Safety Verification by Interactive Generalization. In Proc. of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, Chandra Krintz and Emery Berger (Eds.) (PLDI ’16). ACM, New York, NY, USA. 614–630. https://doi.org/10.1145/2908080.2908118

Digital Library

[43]

Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Esteves-Verissimo. 2018. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Proc. of the 27th European Symposium on Programming, Amal Ahmed (Ed.) (ESOP ’18). Springer-Verlag, Berlin, Heidelberg. 619–650. https://doi.org/10.1007/978-3-319-89884-1_22

[44]

Olivier Rütti, Zarko Milosevic, and André Schiper. 2010. Generic Construction of Consensus Algorithms for Benign and Byzantine Faults. In Proc. of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks (DSN ’14). IEEE Computer Society, Washington, DC, USA. 343–352. https://doi.org/10.1109/DSN.2010.5544299

[45]

Fahad Saleh. 2021. Blockchain without Waste: Proof-of-Stake. The Review of Financial Studies, 34, 3 (2021), 1156–1190.

[46]

Fred B. Schneider. 1990. Implementing Fault-Tolerant Services Using the State Machine Approach: A Tutorial. ACM Computing Surveys (CSUR), 22, 4 (1990), 299–319. https://doi.org/10.1145/98163.98167

Digital Library

[47]

Victor Shoup. 2000. Practical Threshold Signatures. In Advances in Cryptology, Bart Preneel (Ed.) (EUROCRYPT ’00). Springer-Verlag, Berlin, Heidelberg. 207–220. https://doi.org/10.1007/3-540-45539-6_15

[48]

Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems. In Proc. of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’18). ACM, New York, NY, USA. 662–677. https://doi.org/10.1145/3192366.3192414

Digital Library

[49]

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. In Proc. of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM, New York, NY, USA. 357–368. https://doi.org/10.1145/2737924.2737958

Digital Library

[50]

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 Proc. of the 5th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’16). ACM, New York, NY, USA. 154–165. https://doi.org/10.1145/2854065.2854081

Digital Library

[51]

Maofan Yin, Dahlia Malkhi, Michael K. Reiter, Guy Golan Gueta, and Ittai Abraham. 2019. HotStuff: BFT Consensus with Linearity and Responsiveness. In Proc. of the 2019 ACM Symposium on Principles of Distributed Computing (PODC ’19). ACM, New York, NY, USA. 347–356. https://doi.org/10.1145/3293611.3331591

Digital Library

Cited By

Qiu LKim YShin JKim JHonoré WShao Z(2024)LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness ProofsProceedings of the ACM on Programming Languages10.1145/36564238:PLDI(1140-1164)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656423

Recommendations

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

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 ...
Verdi: a framework for implementing and formally verifying distributed systems
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex ...
Verdi: a framework for implementing and formally verifying distributed systems
PLDI '15

Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex ...

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 OOPSLA1

April 2024

1492 pages

EISSN:2475-1421

DOI:10.1145/3554316

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2024 Owner/Author.

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: 29 April 2024

Published in PACMPL Volume 8, Issue OOPSLA1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

NSF (National Science Foundation)
DARPA (Defense Advanced Research Projects Agency)

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
247
Total Downloads

Downloads (Last 12 months)247
Downloads (Last 6 weeks)37

Reflects downloads up to 16 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Qiu LKim YShin JKim JHonoré WShao Z(2024)LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness ProofsProceedings of the ACM on Programming Languages10.1145/36564238:PLDI(1140-1164)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656423

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents