论文标题
具有拜占庭式容错的正式验证的日志复制协议
A Formally Verified Protocol for Log Replication with Byzantine Fault Tolerance
论文作者
论文摘要
拜占庭式容错方案可以在存在崩溃，故障或积极恶意过程的情况下实现状态复制。但是，在没有验证工具的无助的情况下设计此类协议非常容易出错。在对抗环境中，性能和灵活性是以复杂性为代价的，这使得对现有协议的验证极为困难。我们采用不同的方法，并提出了一个针对特定用例的正式验证共识协议：安全记录。我们的协议允许每个节点在并行子例程中提出条目，并确保正确的节点在没有领导者选举的情况下就所有提出的条目的集合一致。它很简单却实用，因为它可以容纳诸如证书透明度之类的记录系统的工作量。我们证明，就所需的回合和可容忍的故障而言，它是最佳的。使用Isabelle/Hol，我们根据听觉模型提供了完全机器检查的安全性证明，我们将扩展到支持签名。我们还提出并评估了原型实现。
Byzantine fault tolerant protocols enable state replication in the presence of crashed, malfunctioning, or actively malicious processes. Designing such protocols without the assistance of verification tools, however, is remarkably error-prone. In an adversarial environment, performance and flexibility come at the cost of complexity, making the verification of existing protocols extremely difficult. We take a different approach and propose a formally verified consensus protocol designed for a specific use case: secure logging. Our protocol allows each node to propose entries in a parallel subroutine, and guarantees that correct nodes agree on the set of all proposed entries, without leader election. It is simple yet practical, as it can accommodate the workload of a logging system such as Certificate Transparency. We show that it is optimal in terms of both required rounds and tolerable faults. Using Isabelle/HOL, we provide a fully machine-checked security proof based upon the Heard-Of model, which we extend to support signatures. We also present and evaluate a prototype implementation.
