区块链拜占庭容错的的形式化验证
分布式、并行与集群计算
2019-10-16 v2
摘要
为实现区块链，现在的趋势是集成非平凡的拜占庭容错共识算法，而非等待接收区块以决定最长分支的初创思路。在存在十年之后，区块链如今交易大量有价值资产，一次简单的分歧就可能导致灾难性损失。遗憾的是，区块链中使用的拜占庭共识方案至多靠“手工”证明正确，因为我们未获悉任何一个经过形式化验证。本文提出两项贡献：（i）我们通过列出区块链共识的六个漏洞（包括两个新反例）来说明问题的严重性；（ii）随后我们使用 ByMC 模型检查器形式化验证 Red Belly Blockchain 的两个拜占庭容错组件。首先，我们用 116 行代码指定一个简单的广播原语，在双核 Intel 机器上 40 秒验证完毕。接着，我们用 276 行代码指定一个区块链共识算法，在 64 核 AMD 机器上使用 MPI 于 17 分钟内验证完毕。最后我们认为，形式化验证区块链共识协议的正确性现已变得相对简单且至关重要。
引用
@article{arxiv.1909.07453,
title = {Formal Verification of Blockchain Byzantine Fault Tolerance},
author = {Pierre Tholoniat and Vincent Gramoli},
journal= {arXiv preprint arXiv:1909.07453},
year = {2019}
}