基于 DAG 的共识协议的可复用形式化验证
Reusable Formal Verification of DAG-based Consensus Protocols
AI总结：
本文提出可复用、可组合的 TLA+/TLAPS 形式化验证框架，通过组合 DAG 构建与排序规范完成五种协议的安全性证明，并将证明工作量减少近一半。
摘要：
区块链使用共识协议来达成一致，例如就交易排序达成一致。基于 DAG 的共识协议正越来越多地被区块链公司采用，以降低能耗并增强安全性。这些协议协作构建区块的偏序（DAG 构建），并生成区块的线性序列（DAG 排序）。鉴于区块链的战略重要性，对共识协议等关键组件正确性的形式化证明至关重要。本文给出了五种基于 DAG 的共识协议的安全性经过验证的规范。其中四种协议——DAG-Rider、Cordial Miners、Hashgraph 和 Eventual Synchronous BullShark——在文献中已得到充分确立。第五种协议是 Aleph 的一个微小变体，Aleph 是另一种已得到充分确立的协议。我们的框架支持证明复用，将证明工作量减少了近一半。它通过提供多种独立的、经过形式化验证的 DAG 构建与排序变体规范来实现这一点，这些规范可以组合起来表达全部五种协议。我们采用 TLA+ 来规范协议并编写其证明，并使用 TLAPS 证明系统自动检查这些证明。每个 TLA+ 规范都相对紧凑，TLAPS 能在数分钟内高效验证数百到数千个义务。我们工作的意义有两方面：第一，它通过提供可靠的安全性保证来支持基于 DAG 的系统的采用；第二，它表明基于 DAG 的共识协议适用于实用、可复用且可组合的形式化方法。
英文摘要：
Blockchains use consensus protocols to reach agreement, e.g., on the ordering of transactions. DAG-based consensus protocols are increasingly adopted by blockchain companies to reduce energy consumption and enhance security. These protocols collaboratively construct a partial order of blocks (DAG construction) and produce a linear sequence of blocks (DAG ordering). Given the strategic significance of blockchains, formal proofs of the correctness of key components such as consensus protocols are essential. This paper presents safety-verified specifications for five DAG-based consensus protocols. Four of these protocols -- DAG-Rider, Cordial Miners, Hashgraph, and Eventual Synchronous BullShark -- are well-established in the literature. The fifth protocol is a minor variation of Aleph, another well-established protocol. Our framework enables proof reuse, reducing proof efforts by almost half. It achieves this by providing various independent, formally verified, specifications of DAG construction and ordering variations, which can be combined to express all five protocols. We employ TLA+ for specifying the protocols and writing their proofs, and the TLAPS proof system to automatically check the proofs. Each TLA+ specification is relatively compact, and TLAPS efficiently verifies hundreds to thousands of obligations within minutes. The significance of our work is two-fold: first, it supports the adoption of DAG-based systems by providing robust safety assurances; second, it illustrates that DAG-based consensus protocols are amenable to practical, reusable, and compositional formal methods.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
