LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness ProofsLast modified: Sat Apr 6 04:21:30 2024 GMT.
AuthorsLongfei QiuYoonseung Kim Ji-Yong Shin Jieung Kim Wolf Honore Zhong Shao AbstractByzantine 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. PublishedIn Proc. 2024 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'24), Copenhagen, Denmark, June 2024. Published as Proceedings of the ACM on Programming Languages (PACMPL), Volume 8, Number PLDI, Article 193 (June 2024), 25 pages. |
Copyright © 1996-2024 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science |
colophon |