AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects

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 mechaniz...

Full description

Saved in:
Bibliographic Details
Published in:Proceedings of ACM on programming languages 2024-04, Vol.8 (OOPSLA1), p.419-448, Article 109
Main Authors: Honoré, Wolf, Qiu, Longfei, Kim, Yoonseung, Shin, Ji-Yong, Kim, Jieung, Shao, Zhong
Format: Article
Language:English
Subjects:
Abstraction
Distributed computing models
Distributed programming languages
Formal software verification
Software and its engineering
Software reliability
Software safety
Software verification
Theory of computation
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2475-1421
2475-1421
DOI:10.1145/3649826