论文标题
拜占庭状态机器复制的效率和潜伏期（扩展版本）
Liveness and Latency of Byzantine State-Machine Replication (Extended Version)
论文作者
论文摘要
拜占庭国家机器复制（SMR）确保在存在恶意复制品的情况下，复制状态的一致性是现代区块链技术的核心。拜占庭SMR协议通常只能在同步下保证在所有情况下的安全性和livese。但是，即使在这个假设下也要保证livesice是不平凡的。到目前为止，我们还缺乏将Livices机制纳入拜占庭SMR方案的系统方法，这通常会导致细微的错误。为了缩小这一差距，我们引入了一个模块化框架，以促进可证明的实用和高效拜占庭SMR协议的设计。我们的框架依赖于特殊SMR同步器原始的视图抽象来推动命令订购协议。我们提出了SMR同步器及其在部分同步下的有限空间实现的简单形式规范。我们还应用规范来证明可笑并通过统一方法分析三个拜占庭SMR方案的潜伏期。特别是，这些结果之一产生了我们认为是开创性PBFT方案算法核心的第一个严格的可月经证明。
Byzantine state-machine replication (SMR) ensures the consistency of replicated state in the presence of malicious replicas and lies at the heart of the modern blockchain technology. Byzantine SMR protocols often guarantee safety under all circumstances and liveness only under synchrony. However, guaranteeing liveness even under this assumption is nontrivial. So far we have lacked systematic ways of incorporating liveness mechanisms into Byzantine SMR protocols, which often led to subtle bugs. To close this gap, we introduce a modular framework to facilitate the design of provably live and efficient Byzantine SMR protocols. Our framework relies on a view abstraction generated by a special SMR synchronizer primitive to drive the agreement on command ordering. We present a simple formal specification of an SMR synchronizer and its bounded-space implementation under partial synchrony. We also apply our specification to prove liveness and analyze the latency of three Byzantine SMR protocols via a uniform methodology. In particular, one of these results yields what we believe is the first rigorous liveness proof for the algorithmic core of the seminal PBFT protocol.
