Authors
Longfei Qiu
Yoonseung Kim
Ji-Yong Shin
Jieung Kim
Wolf Honore
Zhong Shao
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.
Published
In
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.