LiDO：具有基于细化的活跃性证明的线性化拜占庭分布式对象
Authors:
Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honoré, Zhong ShaoAuthors Info & Claims
Key words:
distributed systems, consensus protocols, byzantine fault-tolerance, safety, liveness, formal verification, refinement, proof assistants
分布式系统、共识协议、拜占庭容错、安全性、活性、形式化验证、细化、证明助手
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.
拜占庭式容错状态机复制(SMR)协议，如PBFT、HotStuff和Jolteon，对于现代区块链技术至关重要。然而，正确实现它们是具有挑战性的，因为它们必须处理来自拜占庭对等体的任何意外消息，并始终确保安全性和活动性。已经开发了许多正式的框架来验证SMR实现的安全性，但是在验证其有效性方面仍然存在差距。现有的动态证明要么局限于网络级别，要么不涵盖流行的部分同步协议。
我们介绍了LiDO，这是一个共识模型，可以通过改进来验证实现的安全性和活动性。我们观察到，目前的共识模型不能处理活跃性，因为它们不包括起搏器状态。我们表明，通过在LiDO模型中添加起搏器状态，我们可以将SMR协议的活性属性表示为几个可以通过改进证明轻松验证的安全属性。基于我们的LiDO模型，我们为Coq的未管道和管道Jolteon提供了机械化安全性和活动性证明。这是首个对拜占庭共识协议进行非平凡优化(如流水线)的机械化活性证明。
论文详情：https://dl.acm.org/doi/10.1145/3656423
PDF：https://dl.acm.org/doi/pdf/10.1145/3656423
