事后分析：Notional Finance 漏洞及正确形式化规范的重要性

介绍

不变量是程序状态的属性，描述程序的完整性，从而防止意外情况的发生。自计算机科学诞生之初，不变量对于程序安全性的作用就已得到广泛认可。不变量在 DeFi 安全中扮演着重要角色，因为“代码即法律”，每个人都可以执行代码而无法撤销交易。因此，当不变量被违反时，一切都变得不确定，因为违反状态可能会导致不良行为。不变量可以通过运行时检查进行动态强制执行，也可以在代码部署之前通过形式化验证工具（如 Certora Prover）进行静态证明。

Notional Finance 团队编写并在其代码中检查的不变量不幸地没有描述开发者所设想的属性。由于逻辑错误，该不变量是空洞的，即没有办法违反它。因此，它在 Certora Prover 的输出中显示为“已验证”。

一位白帽黑客后来报告说，该代码存在漏洞，可以通过达到预期不可行的程序状态来利用。收到 Notional Finance 团队的报告后，我们立即研究了原始不变量，并对其进行了修正，以描述开发者的最初意图。我们确认，正确的不变量本可以提前标记出该问题。

在这篇文章中，我们将描述错误和正确的不变量，以及从中吸取的教训。特别是，我们将讨论我们即将对工具进行的改进，以防止将来出现此类情况。

Notional Finance 系统的状态

存入 Notional 账户的资产（或货币）可以属于两种类型之一：“位图（bitmap）”，必须使用 enableBitmapCurrency 方法显式启用；以及“活跃（active）”，这是自动分配资产的组。如果用户调用 enableBitmapCurrency，系统应确保该资产不再被标记为“活跃”货币。

资产使用 14 位表示。每个资产最多可以设置两个标志，因此它在存储中占用最多 16 位（或 2 字节）。每个账户都与一个类型为 uint16 的 bitmapCurrencyId 字段和一个类型为 bytes18（即 144 位）的 activeCurrencies 字段相关联，最多可容纳 9 个资产。

为了使状态正确， bitmapCurrencyId 中表示资产的非零 14 位值不得出现在 activeCurrencies 的任何插槽中。

空洞不变量

最初编写的用于描述不相交资产概念的不变量如下：

// 错误的不变量
invariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(
    address account,
    uint144 i
)
    0 <= i && i < 9 && getBitmapCurrency(account) != 0 &&
        (
            // 启用位图后，它只能在 active currencies 字节中具有货币掩码
            // in the active currencies bytes
            (hasCurrencyMask(account, i) && getActiveUnmasked(account, i) == 0) ||
                getActiveMasked(account, i) == 0
        ) => getActiveUnmasked(account, i) != getBitmapCurrency(account)

该不变量接受一个账户和一个 activeCurrencies 中的索引，并且预期检查 ith 索引中的货币是否不等于位图货币（蕴含式的右侧，或结论）：getActiveUnmasked(account, i) != getBitmapCurrency(account)。蕴含式的左侧（前提）预期设置一些自然要求，例如，索引应在 0 到 9 之间。该不变量使用两个辅助定义来查看存储在插槽 i 中的货币，一个仅包含货币的 14 位（getActiveUnmasked），另一个包含标志（getActiveMasked）。

然而，更仔细地检查该不变量表明，结论可以从前提中轻易得出。在前提中，我们首先注意到位图货币必须是非零的。然后我们分别分析每个析取项（“或”表达式的元素）：

• hasCurrencyMask(account, i) && getActiveUnmasked(account, i) == 0：这告诉我们感兴趣的货币 ID（插槽 i 中的活跃未掩码货币 ID）为零。结合位图货币非零的信息，得出我们检查的货币 ID 不是位图货币。因此，结论立即成立。
• getActiveMasked(account, i) == 0：我们注意到，在规范中，getActiveMasked 定义返回比 getActiveUnmasked 更多的位（16 位而不是 14 位）。因此，如果 getActiveMasked(account, i) == 0，则 getActiveUnmasked(account, i) 也必须为零。结论可以通过与前一种情况类似的论证轻松得出。

因此，如果前提为真，则结论永远不可能是假的。当 Certora Prover 检查此不变量时，它会尝试找到一个具体的输入和状态，使得：

• 在执行代码中的某个公共方法之前，结论可以从前提中得出。
• 在执行代码中的某个公共方法之后，前提为真，但结论为假。

然而，这样的输入状态是不可能存在的，因为结论在所有输入上，无论执行什么方法，都可以从前提中得出。

我们意识到该不变量是空洞的，无法用于发现代码中存在的漏洞。

少即是多

我们提出了一个所需属性的正确形式化，形式很简单：

invariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(
    address account,
    uint144 i
)
  0 <= i && i < 9
         && getActiveUnmasked(account, i) != 0
         && hasCurrencyMask(account, i)
              => getActiveUnmasked(account, i) != getBitmapCurrency(account)

它要求，给定一个账户和 activeCurrencies 中 0 到 9 之间的索引，如果未掩码货币非零，并且为其设置了“活跃”标志，则它必须不同于位图货币。

我们在暴露漏洞的方法 enableBitmapForAccount 上运行了修改后的不变量，并收到了 规则的预期违反。

在执行该方法之前的 pre-state 中，我们注意到位图货币为 0，0x3ffe 是插槽 8（activeCurrencies 中的最后一个）中的活跃货币。我们还看到，由于 activeCurrencies 中的最后 2 个字节是 0xfffe，因此设置了“活跃”标志。在 post-state 中，0x3ffe 现在设置为位图货币，但活跃货币保持不变，这意味着 0x3ffe 也是活跃货币。从这种状态来看，可能会出现双重支出，从而允许利用。

在向 Notional 代码发布建议的热修复程序后，我们运行了修改后的不变量，并且它成功地证明了代码是正确的。可以在 此处 和 此处 找到包含该工具输出的相关验证报告。完整修订后的规范也可用。

检查空洞性

有时确实很难正确地形式化规则。然而，在编写规则时，我们可以检查自己，并确保我们没有遗漏预期含义。

在我们的例子中，我们可以采用不正确的不变量并将其断言为规则。如果此规则已验证，则意味着系统中没有任何状态违反该不变量，这意味着没有什么可检查的：

rule verifiedIfInvariantIsVacuous(address account, uint144 i) {
    assert 0 <= i && i < 9 && getBitmapCurrency(account) != 0 &&
        (
            // 启用位图后，它只能在 active currencies 字节中具有货币掩码
            // in the active currencies bytes
            (hasCurrencyMask(account, i) && getActiveUnmasked(account, i) == 0) ||
                getActiveMasked(account, i) == 0![]        ) => getActiveUnmasked(account, i) != getBitmapCurrency(account);
}

一个好的不变量有助于区分好状态和坏状态。一个坏的不变量包含所有状态。

空洞性问题在形式化验证领域由来已久，不仅存在于软件验证中，实际上可以追溯到硬件验证。已经开发了几种用于 自动空洞性检查 [1] 的技术**。如果空洞性检查失败，则会向程序员显示警告。我们计划在不久的将来集成此类方法。

任何人今天都可以使用的另一种有用的技术是手动向代码中添加错误，目的是破坏我们编写的规则。如果我们没有收到因向代码添加此类错误而违反我们规则的报告，则可能规则的形式化不正确。

更好的规范带来更好的安全性

Notional Finance 代码中发现的漏洞已经通过了一些最好的审计师和 Notional Finance 的才华横溢的团队。Notional 采取了广泛的预防措施，使用不同的层来保护其代码：审计、形式化验证和漏洞赏金。在安全性方面没有万能的解决方案，我们一直在学习如何改进。

多层安全保障是好的，但不能保证 100% 的保护。在此事件中未检查 Certora 规则，但可以轻松地对其进行测试和审计，以避免安全漏洞。

形式化规范在代码安全方面的效用已得到充分理解。然而，正确地编写规范可能与正确地编写代码一样棘手。我们建议采取以下措施来提高规范和代码的安全性：

1. 审计规范。好的规范易于阅读和审查。我们注意到更正后的规范更具可读性。Certora 计划与外部审计师合作审查这些规则。这在图中有所描述。
2. 开设 漏洞赏金 以发现规范问题，而不仅仅是代码问题。
3. 开发 用于检查规范的技术。我们已经实施了健全性检查，以确保规则中的每个断言都是可访问的（不包含 require(false) 或逻辑上等效的语句）。我们现在正在实现对不变量的检查，如上所述。
4. 集成 规范的测试工具，特别是突变测试。

应该像代码一样仔细检查规则。然后，Certora Prover 可以提供非常高的漏洞覆盖率。

总结

我们从此事件中得出的结论是：

1. 没有规范的代码就像没有计划的房子。
2. 编写形式化规范很困难，需要仔细的思考和工具。

D. Knuth 的一句名言是

有些任务最好由机器完成，

有些任务最好由人类的洞察力完成;

一个设计合理的系统将找到正确的平衡。

我们正在努力寻找正确的平衡，以简化使用 Certora Prover 进行验证的任务。我们现在正在添加对人编写的不变量的检查。将来，计算机将为常见的金融交易提出有用的不变量。

致谢

感谢 Notional Finance 团队及时通知我们有关该问题，以及他们的诚实和透明。

1. Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh:

Efficient Detection of Vacuity in Temporal Model Checking. Formal Methods Syst. Des. 18(2): 141–163 (2001)

• 原文链接： certora.com/blog/post-mo...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～