NEO 的 dBFT 协议的形式化安全性分析

NEO 是全球顶尖的公链之一。我们关注其骨干共识协议，称为委托拜占庭容错（dBFT）。dBFT 协议已被 ONT 等多种区块链系统采用。dBFT 声称在不超过 $f = \lfloor \frac{n}{3} \rfloor$ 个节点为拜占庭节点时可保证安全性，其中 $n$ 为共识参与者的总数。然而，我们发现了破坏其所声称安全性的攻击。本文通过对 dBFT 协议进行安全性分析给出我们的结果。首先，我们评估 NEO 的源代码，并通过状态机复制（SMR）模型形式化地给出 dBFT 的流程。接着，我们给出带有两例攻击的理论分析。这些攻击在不超过 $f$ 个节点的情况下破坏了 dBFT 的安全性。然后，我们就如何修复系统以抵御所发现的攻击提出建议。所建议的修复已被 NEO 官方团队采纳。最后，我们进一步讨论了导致此类问题的原因、与当前许可链区块链系统的关系，以及潜在影响的范围。