Notional Finance漏洞的事后分析——一个恒真的不变式

Notional Finance 漏洞的事后分析 — 一种同义反复的不变量

引言

2022 年 1 月 7 日，Notional Finance报告了一个关键漏洞，该漏洞阻止了其智能合约。该漏洞是由于潜在的资产重复计算引起的 —— 同一个 token 可能同时显示为“位图货币”和“活动货币”。这个 bug 逃过了 DeFi 领域最好的审计师的法眼。在开发过程中，Notional 团队采用了形式化验证，通过使用 Certora Prover 来检查系统的一个不变量：任何资产都不应同时标记为“位图”和“活动”。

不变量是程序状态的属性，描述了程序的完整性，从而防止了令人不快的意外。自计算机科学诞生以来，不变量对程序安全性的效用已得到广泛认可。不变量在 DeFi 安全中起着重要作用，因为“代码即法律”，每个人都可以执行代码，而无法撤销交易。因此，当违反不变量时，一切都完了，因为从违反状态开始，可能会出现不良行为。不变量可以通过运行时检查以动态方式强制执行，也可以在通过 Certora Prover 等形式化验证工具部署代码之前以静态方式证明。

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

此后，一位白帽黑客报告说，该代码很容易受到攻击，因为它达到了预期不可行的程序状态。收到 Notional Finance 团队的报告后，我们立即研究了原始不变量，并对其进行了更正，以描述开发人员的最初意图。我们确认正确的加粗不变量可以提前标记出问题。

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

Notional Finance 系统的状态

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

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

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

空洞的不变量

编写的用于描述非交叉资产概念的原始不变量如下：

// WRONG INVARIANT
invariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(
    address account,
    uint144 i
)
    0 <= i && i < 9 && getBitmapCurrency(account) != 0 &&
        (
            // When a bitmap is enabled it can only have currency masks
            // in the active currencies bytes
            (hasCurrencyMask(account, i) && getActiveUnmasked(account, i) == 0) ||
                getActiveMasked(account, i) == 0
        ) => getActiveUnmasked(account, i) != getBitmapCurrency(account)

该不变量采用一个账户和 activeCurrencies 中的一个索引，并且期望检查 i 索引中的货币是否不等于位图货币（蕴含式的右侧，或加粗结论加粗）：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 上运行了修改后的不变量，并收到了该规则的预期违规。

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

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

检查空虚性

有时确实很难正确地形式化规则。但是，我们可以在编写规则时检查自己，并确保我们没有遗漏我们想要表达的含义。

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

rule verifiedIfInvariantIsVacuous(address account, uint144 i) {
    assert 0 <= i && i < 9 && getBitmapCurrency(account) != 0 &&
        (
            // When a bitmap is enabled it can only have currency masks
            // 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 规则，但可以轻松地对其进行测试和审核，以避免出现安全漏洞。

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

形式化规范对于代码安全性的效用已得到充分理解。但是，获得正确的规范可能与获得正确的代码一样棘手。我们建议采取以下措施来提高规范和代码的安全性：

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

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

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

总结

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

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

D. Knuth 的一句名言是

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

加粗而另一些任务最好由人类的洞察力完成；加粗

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

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

致谢

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

1. Ilan Beer、Shoham Ben-David、Cindy Eisner、Yoav Rodeh：

   时间模型检查中空洞性的高效检测。形式化方法系统设计 18(2): 141–163 (2001) ↩︎

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