区块链共识的整体验证

区块链近来引起业界关注，部分原因在于其自动化资产转移的能力。它要求分布式参与方在存在恶意（又称拜占庭）参与方的情况下就一个区块达成共识。恶意参与方经常利用这些区块链共识算法的弱点，有时造成灾难性后果。事实上，这些弱点相当常见，现有区块链共识协议手写证明中的缺陷便是明证 [63]。矛盾的是，迄今为止，尚无任何区块链共识通过模型检测得到整体验证。在本文中，我们通过对工业界所用区块链共识的首次模型检测，弥补了这一矛盾。我们提出一种整体方法来验证 Red Belly Blockchain [20] 的共识算法，适用于任意数量 $n$ 的进程以及任意数量 $f<n/3$ 的拜占庭进程。我们直接将算法伪代码分解为两部分——内部广播算法和外部决策算法——各自建模为阈值自动机 [36]，并以线性时序逻辑形式化其预期属性。随后，我们在精心识别的公平性假设下自动检测内部广播算法。对于外部算法的验证，我们依据已检测的内部算法属性简化了内部算法的模型。由此，我们不仅在约 70 秒内正式验证了 Red Belly Blockchain 共识的安全性属性，还验证了它的活性。