AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects

Last modified: Sat Apr 6 04:17:56 2024 GMT.

Authors

Wolf Honore
Longfei Qiu
Yoonseung Kim
Ji-Yong Shin
Jieung Kim
Zhong Shao

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.

Published

In Proc. 2024 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'24), Pasadena, CA, October 2024. Published as Proceedings of the ACM on Programming Languages (PACMPL), Volume 8, Number OOPSLA1, Article 109 (April 2024), 30 pages.

Conference Paper [PDF]

Extended Technical Report [PDF]

Artifact [URL]

colophon