形式化验证流水线Moonshot共识协议的安全性
Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol
AI总结：
本文使用IVy对Supra的Pipelined Moonshot共识协议进行形式化建模与验证，证明在拜占庭验证者少于三分之一时协议无分叉且能防止双花攻击。
摘要：
去中心化金融已成为传统中心化金融系统的当代竞争者及互补者。截至2024年1月23日，根据Defillama的数据，所有区块链上的DeFi应用锁定的总价值约为550亿美元。拜占庭容错状态机复制（SMR）协议（通常被称为共识协议）是区块链的核心组件。如果共识协议中可能出现分叉，它们可能会被滥用于实施双花攻击，鉴于区块链上交易的高金融量，这将是灾难性的。对共识协议的安全性进行形式化验证是保证不可能出现分叉的黄金标准。然而，这被认为是复杂且具有挑战性的。除了Tendermint和QBFT之外，没有多少复杂的共识协议经过形式化验证，这一事实反映了这一点。我们关注Supra的Pipelined Moonshot共识协议。与Tendermint的形式化验证类似，我们也使用IVy对Pipelined Moonshot进行建模，并形式化证明对于所有网络规模，只要拜占庭验证者的数量少于三分之一，该协议就不允许分叉，从而证明Pipelined Moonshot是安全的，并且无法利用分叉进行双花。该IVy模型和安全性证明可在Github上获取。
英文摘要：
Decentralized Finance (DeFi) has emerged as a contemporary competitive as well as complementary to traditional centralized finance systems. As of 23rd January 2024, per Defillama approximately USD 55 billion is the total value locked on the DeFi applications on all blockchains put together. A Byzantine Fault Tolerant (BFT) State Machine Replication (SMR) protocol, popularly known as the consensus protocol, is the central component of a blockchain. If forks are possible in a consensus protocol, they can be misused to carry out double spending attacks and can be catastrophic given high volumes of finance that are transacted on blockchains. Formal verification of the safety of consensus protocols is the golden standard for guaranteeing that forks are not possible. However, it is considered complex and challenging to do. This is reflected by the fact that not many complex consensus protocols are formally verified except for Tendermint and QBFT. We focus on Supra's Pipelined Moonshot consensus protocol. Similar to Tendermint's formal verification, we too model Pipelined Moonshot using IVy and formally prove that for all network sizes, as long as the number of Byzantine validators is less than one thirds, the protocol does not allow forks, thus proving that Pipelined Moonshot is safe and double spending cannot be done using forks. The IVy model and proof of safety is available on Github.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
