一句话：LiDO 模型引入 pacemaker 状态，将 SMR 活性归约为安全性质，并在 Coq 中机器化验证 Jolteon（含流水线）的安全与活性。
拜占庭容错状态机复制协议（如 PBFT、HotStuff、Jolteon）是区块链等技术的基础，但其实现必须处理拜占庭节点的任意消息并始终保证安全性与活性，正确实现和验证困难。已有形式化框架多验证安全性，活性验证仍有缺口：现有活性证明要么局限于网络层，要么不覆盖常用的部分同步协议。本文提出 LiDO 共识模型，观察到共识模型缺少 pacemaker 状态导致难以处理活性；通过向 LiDO 加入 pacemaker 状态，可将 SMR 协议的活性性质表达为若干可由精化证明验证的安全性质。作者在 Coq 中为无流水线和流水线版 Jolteon 给出了机器化的安全性与活性证明。这是首个针对具有流水线等非平凡优化的拜占庭共识协议的机器化活性证明。
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.
@article{QiuKSKHS24,
title = {LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs},
author = {Longfei Qiu and Yoonseung Kim and Ji-Yong Shin and Jieung Kim and Wolf Honoré and Zhong Shao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656423}
}