当不变量不成立时：DAI的Certora惊喜

作者：Kurt Barry（MakerDAO）， Uri Kirstein（Certora）

引言

"你不知道的事情不会让你陷入麻烦。让你陷入麻烦的，是你确知的那些事情，它们其实并不正确。" - 马克·吐温

Multi-Collateral DAI 是由 MakerDAO 管理的稳定币，是最大的加密货币之一。它于 2019 年 11 月推出，截至 2022 年 5 月，市值大约为 65 亿美元，背后大约有 100 亿美元的抵押品。按加密货币标准来看，它已经算是古老的，如果其智能合约中存在任何bug，早就应该被发现。令人惊讶的是，发现了一个自 2018 年以来被认为是恒定关系的系统量之间的依赖关系，甚至被认为是可以在数学上证明的，并不存在。这一异常是使用 Certora Prover 发现的。幸运的是，无资金受到风险。这个发现重要地提醒我们，必须非常小心地区分一些可能是真的东西和那些实际上是被证明的东西（同时也要记住，证明中也可能存在错误！）。

Certora Prover

为了保持 DAI 及其背靠的抵押品安全，MakerDAO 协议工程核心单位（PECU）采用了多种流程和技术。代码更改经过广泛的内部审核，必须通过单元测试和集成测试。通过红队测试、模糊测试和外部审计来寻找错误。 MakerDAO 还有一个 Immunefi 漏洞赏金计划。

PECU 安全基础设施的另一个重要组成部分是形式验证。形式验证试图证明程序行为符合某些规范（通常单独定义）。系统的代码被转化为逻辑公式，随后使用数学方法尝试证明规范中描述的性质。形式验证的巨大优势在于其全面性 - 所有执行路径被检查，因此我们会遇到极少的边际案例。

Certora 提供了一种自动形式验证工具，称为 Certora Prover。MakerDAO PECU 团队自 2021 年 6 月以来一直在撰写规范并使用 Prover 进行验证。

Maker 协议

Maker 协议由创建和维持 DAI 稳定币的智能合约组成。在为在其他链（包括像 rollups 这样的第二层解决方案）上部署而准备期间，对合约进行了一些更改和更新。Certora prover 被用于对修改后的合约进行形式验证。除了与 K Framework 进行的原始验证相似的功能级证明外，充分利用了 Certora Prover 表达合约级属性的能力（即适用于合约的所有功能的属性）。最重要的这样的属性是一个称为“DAI 基本方程”的不变性。

DAI 基本方程

DAI 是由债务支持的。债务要么被分配给一个 Vault，意味着它与某种抵押资产相关，要么是“无担保的”（也称：“坏的”），意味着这要由协议（即 MKR 持有者）负责。这两个债务来源相加，应该等于所有 DAI 余额的总和。在数学上，我们可以写成：

$$ \sum udaiu=\sum{i,u} tab_{i,u}+vice $$

为了使上述方程有意义，我们需要一些定义：

• $dai_u$ 指的是用户 $u$ 的 DAI余额。
• $tab_{i,u}$ 指的是属于用户 $u$ 具有抵押类型 $i$ 的 Vault 的债务。
• $vice$ 是无担保债务。可以假设总和遍历所有有效值，约定 $daiu$ 和 $tab{i,u}$ 的值在未修改之前默认值为零。在以太坊的上下文中，“用户”的概念与“以太坊地址”一致，可能是一个智能合约或一个由外部拥有的账户。

DAI 会计的真实来源在于一个称为 Vat 的合约。DAI 基本方程 (FEoD) 因此可以用 Vat 的存储变量来表示。由于在收集借贷费用时遍历所有 Vault 是不可行的，Vat 不精确地存储所有能最自然地表达基本方程的值。以 Vat 存储变量的形式表达 FEoD 的最简单方法是：

$$ Vat.debt=Vat.vice+\sum_i Vat.ilks[i].Art \cdot Vat.ilks[i].rate $$

其中总和遍历所有有效债务类型。

$Vat.debt$ 是一个 累计 值，存储所有 DAI 余额的总和。

$Vat.vice$ 就是总的坏债务（从技术上讲它也是一个累计，因为坏债务总是“分配”给某个地址）。

$Vat.ilks[i].Art$ 是另一个累计值，是针对某种抵押类型（“ilk”）的“标准化”债务的总和。标准化的债务是一个数值，当与适当的 rate 相乘后，给出当前的 DAI 债务。

$Vat.ilks[i].rate$ 是另一种累计值，率 累计器。它跟踪自创立以来某种抵押类型的总复利费用。例如，如果一种抵押品的稳定费用年利率为 5%，并且存在了两年，那么它在 Vat 中的 rate 将是 $1.05^2=1.1025$。如果在那个时候，有人从那种抵押类型的 Vault 中提取 110.25 DAI，关联的 $Art$ 增加将是：

$$ \frac{110.25}{1.1025}=100 $$

关于费用计算在 Maker 协议中如何工作的更多信息可以在文档中找到。

请注意，要真正证明 FEoD，应建立所有累计器的正确性（即，它们确实等于它们应该等的和或乘积）。然而，基于简洁的考虑，这里我们将重点关注累计器之间的关系。现在我们拥有了理解使用 Certora 技术证明 FEoD 尝试所需的协议特定背景。

编写规范

注意： 强调 bug 的简明规范可以在一个自包含的库中公开获取，其中包含在发现时进行测试的代码。它包含了如何自己尝试的说明。

Certora Prover 的规范是用 Certora 验证语言（CVL）编写的。在 CVL 中，有一个名为 不变性 的构造，代表系统在经历任何更改后始终应该拥有的属性。通过归纳法来证明不变性。首先，在构造函数调用之后证明不变性成立；这就是归纳基础。然后，对于合约中的每个函数，假设不变性在其调用之前成立，并证明在调用之后也成立。验证每个函数是归纳步骤。不变性出现在Vat.spec 文件的结尾的简化示例中：

invariant fundamental_equation_of_dai()
   debt() == vice() + sumOfVaultDebtGhost()
   filtered { f -> !f.isFallback }

第一行像函数一样声明了不变性 - 它有一个名称和参数（在这种情况下没有）。第二行是重要部分 - 描述 FEoD 的逻辑公式，依据前面讨论。debt() 和 vice() 表达式调用 Vat 函数，读取相应的存储槽。请注意，这些在文件顶部声明为 envfree（意味着它们不依赖于调用上下文，如 msg.sender）：

methods {
    debt() returns (uint256) envfree
    vice() returns (uint256) envfree
}

不变性第三行告诉验证器不要考虑 Vat 的回退函数，因为它总是回退，因此没有相关性（如果不这样做，验证器会发出“规则有效性”警告）。

不变性第二行中的 sumOfVaultDebtGhost() 是合约中不存在的函数。它作为 ghost 计算。Ghosts 模型化那些不能通过函数调用直接获取的合约状态。没有合约函数返回所有 Vault 债务的总和，因此我们必须使用 ghost。关于 ghost 的更详细信息可以在Certora 文档中找到。

尽管不变性中仅明确使用了一个 ghost，但定义了三个 ghost：

ghost sumOfVaultDebtGhost() returns uint256 {
    init_state axiom sumOfVaultDebtGhost() == 0;
}

ghost mapping(bytes32 => uint256) rateGhost {
    init_state axiom forall bytes32 ilk. rateGhost[ilk] == 0;
}

ghost mapping(bytes32 => uint256) ArtGhost {
    init_state axiom forall bytes32 ilk. ArtGhost[ilk] == 0;
}

另外两个（rateGhost 和 ArtGhost）是构建债务总和 ghost 所需的。它们分别表示给定抵押类型的复利和总的“标准化债务”。请注意，它们是从抵押品标识符到其相应数量的 映射，即每个 ghost 跟踪每种抵押类型的不同值。init_state axiom ... 表达式定义了 ghost 在调用构造函数后应具有的初始值，设置为零以匹配以太坊的行为。请回忆一下，rate 和 Art 的乘积对于某个 ilk 给出由贷款担保的总 DAI 债务。

Ghosts 使用 Hook 更新，Hook根据特定程序行为修改 ghost 变量。在文档中，对于好奇者还有更详细的信息。Vat.spec 使用了两种类型的Hook - Sload 和 Sstore。首先考虑两个 Sload Hook：

hook Sload uint256 v currentContract.ilks[KEY bytes32 ilk].(offset 0) STORAGE {
    require ArtGhost[ilk] == v;
}

hook Sload uint256 v currentContract.ilks[KEY bytes32 ilk].(offset 32) STORAGE {
    require rateGhost[ilk] == v;
}

语法可能看起来复杂，但从概念上讲，这些Hook非常简单：每当从合约存储中读取 rate 或 Art 值时，对应的 ghost 必须与读取的值相等。这确保了每当使用它们时，ghost 值与存储中的值一致。

Sstore Hook在 rate 或 Art 写入存储时生效，而不是读取。在Hook主体中可以使用旧的和新的存储值。这些值像 Sload Hook一样更新 ArtGhost[ilk] 或 rateGhost[ilk] 的值，并根据先前定义的 rate、Art 和某个 ilk 的 DAI 债务之间的关系，更新 sumOfVaultDebtGhost 值。

hook Sstore currentContract.ilks[KEY bytes32 ilk].(offset 0) uint256 newArt (uint256 oldArt) STORAGE {
    havoc sumOfVaultDebtGhost assuming sumOfVaultDebtGhost@new() == sumOfVaultDebtGhost@old() + (newArt * rateGhost[ilk]) - (oldArt * rateGhost[ilk]);
    ArtGhost[ilk] = newArt;
}

hook Sstore currentContract.ilks[KEY bytes32 ilk].(offset 32) uint256 newRate (uint256 oldRate) STORAGE {
    havoc sumOfVaultDebtGhost assuming sumOfVaultDebtGhost@new() == sumOfVaultDebtGhost@old() + (ArtGhost[ilk] * newRate) - (ArtGhost[ilk] * oldRate);
    rateGhost[ilk] = newRate;
}

这些 Sstore Hook使 ArtGhost 和 rateGhost 成为必需。由于在呈现程序执行期间Hook被应用，因此在Hook内无法调用合约函数。因为函数可能不能按预期工作，存储可能处于不意外的状态。

如前所述，这项规范并不 足够 完全建立 FEoD。完整的证明还需要建立 debt 和 Art 累计器的正确性等其他条件。然而，这个不变性 在任何违反该不变性的情况下 是足够的，这说明 FEoD 不成立。换句话说，如果 Vat 合约和我们预期的相符，这个不变性应该成立。

让我们看看在尝试证明 FEoD 时会发生什么！

不成立!?

我们第一次注意到运行验证器时，在命令行输出的最后部分：

我们可以立即看到存在不变性的违反，并且它涉及到 Vat.init 函数。但是，现在下结论认为 FEoD 不成立为时尚早。Certora Prover 在证明技术中使用了 过度近似，这意味着它有时可能报告错误的违例。然而，除非 Prover 本身有 bug，否则不应发生假阴性。因此，我们可以对成功证明充满信心，但必须始终检查违规情况。幸运的是，对于它发现的任何违规，Prover 总是生成 concrete counterexample - 一组输入、存储和调用上下文的组合，说明违反了该属性。这使得快速检查违反是否合理变得简单。

我们可以通过在网页浏览器中加载“验证报告”链接来检查 counterexample。我们获得类似以下的视图：

下一步是在“结果”下深入查看“fundamental_equation_of_dai”项。继续点击“init(bytes32)”会显示如下内容：

“调用跟踪”子窗口包含了提取 counterexample 所需的信息。展开“假设不变性在前状态中”表明我们以 debt()、vice() 和 sumOfVaultDebtGhost() 的零值开始：

查看后状态显示，在 init 执行后，不知何故 sumOfVaultDebtGhost() 变为非零值，这当然是一个违反。请注意，counterexample 中的确切数值在你自己运行工具时可能不同。

但是为什么？我们可以看到在函数执行过程中应用了 Sstore Hook：

所有所需的信息都在此，尽管需要一些工作来弄清楚发生了什么。首先，我们需要理解 init 的工作原理：对于新的抵押类型，init 将其 rate 设置为一个的固定点等价物（在此情况下为 10^27），以便未来的复利计算能得以有效工作。

    function init(bytes32 ilk) external auth {
        require(ilks[ilk].rate == 0, "Vat/ilk-already-init");
        ilks[ilk].rate = 10 ** 27;
        emit Init(ilk);
    }

这个 rate 的更新触发了相应的 Sstore Hook。检查Hook末尾的平等关系，我们可以推断 sumOfVaultDebtGhost() 变为非零是因为 ArtGhost[ilk] * newRate 是非零的。因此 ArtGhost[ilk]，因此 ilk 的 Art 存储值，必须是非零的。总之，如果在 Vat.ils[ilk].Rate 为零，但 Vat.ilks[ilk].Art 不为零时，调用函数 Vat.init(ilk) 将导致 FEoD 不成立。

现在 counterexample 非常清晰，我们仍然需要回答“这在实践中是可能的吗？”的问题。Certora Prover 仅假设初始存储状态遵循所讨论的不变性 - 这些状态不一定是通过执行智能合约功能 可达到 的。可以尝试用 Certora Prover 证明状态不可达（该尝试将失败）。但是，我们将采取一种捷径，通过描述实现 counterexample 前置条件的方法，这在 PECU 发现时迅速进行了识别。Vat.fold 函数可以在相关 Art 变为非零后将 rate 重置为零，从而允许在已经激活的 ilk 上调用 init。可以在发现此 counterexample 后提交的bug中找到示例测试用例。请注意，fold 本身遵循 FEoD，因此仅第二个 init 调用会导致违反。我们非常有信心，这就是违反 FEoD 的唯一方法，因为 (1) init 要求 rate 为零，(2) 债务只能在 rate 为非零时产生，以及 (3) 唯一可以减少 rate 的 Vat 函数是 fold。

这是一个令人惊讶的结果。FEoD 是众所周知的 Multi-Collateral DAI “不变性”，至少自 2018 年以来就得到了认可，甚至被认为在数学上是可以证明的。幸运的是，这个边缘情况不会对系统构成威胁，因为 fold 和 init 函数被限制在治理和受信任的合约范围内。如果违反序列得以执行，将会使 Vault 债务总额超过未偿 DAI，这可能会让 DAI 的价格高于其Hook，难以使 Vault 还清其债务。治理已经可以以其他方式造成更严重的损害，因此其行为是受到限制的，允许用户在恶意行为开始生效前退出系统。诚实少数的 MKR 持有者甚至可以触发关闭程序，安全优雅地解散系统。未来在其他链上的部署将包含修复，使 FEoD 成为真正的不变性。

结论

这个发现支持我们在智能合约安全的整体方法中使用形式验证。发现一个长期以来的假设是错误的，强调了在开发智能合约系统时保持谦逊和开放的心态的重要性。关于安全性或正确性的信念应该仅以证据的权重为依据，而不是绝对存在。错误和缺陷可能会长时间隐藏在显而易见之处。有效的工具是极大的帮助，但前提是必须正确和一致地应用！

如果你有任何问题，请与 MakerDAO 协议工程核心单位联系（在 MakerDAO Discord 的 protocol-engineering-public 频道找到我们）或 Certora 团队（Discord 或 Twitter）。

• 原文链接： hackmd.io/@SaferMaker/DA...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～