基于HotStuff的拜占庭容错共识在Agda中的形式化验证：扩展版
分布式、并行与集群计算
2022-03-30 v2 计算机科学中的逻辑
摘要
LibraBFT是一种基于HotStuff的拜占庭容错（BFT）共识协议。我们给出了HotStuff/LibraBFT底层协议的抽象模型，以及其核心正确性（安全性）属性和一项扩展条件（使非参与方能够验证已提交结果）的机器可检查的形式化证明。（活性性质将针对具体实现进行证明，而非针对本文所提出的抽象模型。）一项关键贡献是以抽象方式精确定义关于诚实节点行为的假设，且独立于任何特定实现。因此，我们的工作是在不必重复证明底层协议正确性的艰苦工作的情况下，证明整类具体实现之正确性的重要一步。这些抽象证明针对单一配置（epoch）；将这些证明扩展到跨配置变更是未来的工作。我们的模型和证明用Agda表达，并以开源形式提供。
引用
@article{arxiv.2203.14711,
title = {Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version},
author = {Harold Carr and Christopher Jenkins and Mark Moir and Victor Cacciari Miraldo and Lisandra Silva},
journal= {arXiv preprint arXiv:2203.14711},
year = {2022}
}
备注
23 pages, 1 figure, extended version of version to be published in 14th NASA Formal Methods Symposium (NFM 2022)