为什么优先选择模糊测试而非形式化验证？

我们最近推出了我们的新产品，作为一种服务的 Invariant 开发。我们经常被问到的一个问题是：“为什么使用模糊测试而不是形式化验证？” 答案是：“这很复杂。”

我们的大部分审计都使用模糊测试，但过去也使用过形式化验证方法。 特别是，我们发现符号执行在诸如 Sai、Computable 和 Balancer 等审计中很有用。 然而，我们通过经验意识到，模糊测试工具产生类似的结果，但需要的技能和时间却显著减少。

在这篇博文中，我们将研究为什么支持形式化验证的两个主要论断通常会失败：证明不存在漏洞通常是无法实现的，并且模糊测试可以识别出形式化验证发现的相同漏洞。

证明不存在漏洞

形式化验证优于模糊测试的关键卖点之一是它能够证明不存在漏洞。 为此，形式化验证工具使用数学表示来检查给定的 不变式 对于系统的所有输入值和状态是否成立。

虽然这种说法在简单的代码库上是可以实现的，但在实践中并不总是能够实现，尤其是在复杂的代码库中，原因如下：

• 可能需要重写代码，使其能够进行形式化验证。 这导致验证的是目标的伪副本，而不是目标本身。 例如，Runtime Verification 团队验证了 ETH2.0 升级的存款合约的伪代码，正如他们 博客文章 中的这段摘录所提到的：

> **具体来说，我们首先严格地形式化了增量Merkle树算法。 然后，我们提取了存款合约中使用的算法的伪代码实现，并正式证明了伪代码实现的正确性。**

• 复杂的代码可能需要对某些功能进行自定义摘要 才能进行分析。 在这些情况下，验证依赖于自定义摘要的正确性，这会将正确性的责任转移到该摘要上。 为了构建这样的摘要，用户可能需要使用一种额外的自定义语言，例如 CVL，这会增加复杂性。
• 循环和递归可能需要添加手动约束（例如，仅在给定的时间内展开循环）以帮助证明者。 例如，Certora 证明者可能会将某些 循环 展开固定次数的迭代，并将任何额外的迭代报告为违规，从而迫使用户进一步参与。
• 求解器可能会超时。 如果该工具依赖于求解器来求解方程，则可能无法在合理的时间内找到解。 特别是，证明具有大量非线性算术运算或对存储或内存进行更新的代码具有挑战性。 如果求解器超时，则无法提供保证。

因此，虽然证明不存在漏洞在理论上是形式化验证方法的一个好处，但在实践中可能并非如此。

发现漏洞

当无法形式化验证代码时，仍然可以将形式化验证工具用作漏洞查找工具。 然而，问题仍然存在，“形式化验证能否找到模糊器无法找到的真正漏洞？” 在这一点上，使用模糊器不是更容易吗？

为了回答这个问题，我们研究了在 MakerDAO 和 Compound 中使用形式化验证发现的两个漏洞，然后尝试仅使用模糊器找到这些相同的漏洞。 剧透警告：我们成功了。

我们选择这两个漏洞是因为它们被广泛宣传为通过形式化验证发现的，并且它们影响了两个流行的协议。 令我们惊讶的是，与模糊测试发现的许多漏洞（请参阅我们的 安全审查）相比，很难找到仅通过形式化验证发现的公共问题。

我们的模糊器在几分钟内在典型的开发笔记本电脑上运行就发现了这两个漏洞。 我们评估的漏洞，以及我们用来发现它们的形式化验证和模糊测试 harness，可在我们的 GitHub 页面 上找到，该页面是关于对形式化验证的合约进行模糊测试以重现流行的安全问题。

DAI 的基本 不变式

MakerDAO 在四年后在其线上代码中发现了一个漏洞。 你可以在 当 不变式 不存在时：DAI 的 Certora 惊喜 中了解更多关于该漏洞的信息。 使用 Certora 证明器，MakerDAO 发现 DAI 的基本 不变式，即所有抵押品支持的债务和无抵押债务的总和应等于所有 DAI 余额的总和，在特定情况下可能会被违反。 核心问题是，当 vault 的 Rate 状态变量为零且其 Art 状态变量为非零时调用 init 函数会改变 vault 的总债务，这违反了检查总债务和总 DAI 供应量的 不变式。 MakerDAO 团队得出结论，在调用 fold 函数后调用 init 函数是打破 不变式 的一种方式。

function sumOfDebt() public view returns (uint256) {
    uint256 length = ilkIds.length;
    uint256 sum = 0;
    for (uint256 i=0; i < length; ++i){
        sum = sum + ilks[ilkIds[i]].Art * ilks[ilkIds[i]].rate;
    }
    return sum;
}

function echidna_fund_eq() public view returns (bool) {
    return debt == vice + sumOfDebt();
}

图 1：Solidity 中 DAI 不变式 的基本方程

我们用 Solidity 实现了相同的 不变式，如图 1 所示，并使用 Echidna 进行了检查。 令我们惊讶的是，Echidna 违反了 不变式，并找到了一条触发违规的独特路径。 我们的实现可以在存储库的 Testvat.sol 文件中找到。 实现 不变式 很容易，因为被测试的源代码很小，只需要计算所有债务总和的逻辑。 Echidna 在一台 i5 12-GB RAM Linux 机器上花费不到一分钟就违反了 不变式。

Compound V3 Comet 中抵押账户的清算

Certora 团队使用他们的 Certora Prover 识别出 Compound V3 Comet 智能合约中一个有趣的问题，该问题允许清算一个完全抵押的账户。 此问题的根本原因是为 16 位向量使用 8 位掩码。 对于向量中的较高位，掩码保持为零，这会在计算总抵押品时跳过资产，并导致清算抵押账户。 有关此问题的更多信息，请参见 Compound V3 (Comet) 的形式化验证报告。

function echidna_used_collateral() public view returns (bool) {
    for (uint8 i = 0; i < assets.length; ++i) {
        address asset = assets[i].asset;
        uint256 userColl = sumUserCollateral(asset, true);
        uint256 totalColl = comet.getTotalCollateral(asset);
        if (userColl != totalColl) {
            return false;
        }
    }
    return true;
}

function echidna_total_collateral_per_asset() public view returns (bool) {
    for (uint8 i = 0; i < assets.length; ++i) {
        address asset = assets[i].asset;
        uint256 userColl = sumUserCollateral(asset, false);
        uint256 totalColl = comet.getTotalCollateral(asset);
        if (userColl != totalColl) {
            return false;
        }
    }
    return true;
}

图 2：Solidity 中 Compound V3 Comet 的 不变式

Echidna 发现了 Solidity 中 不变式 实现的问题，如图 2 所示。 此实现可以在存储库中的 TestComet.sol 文件中找到。 实现 不变式 很容易； 它需要限制与测试合约交互的用户数量，并添加一种计算所有用户抵押品总和的方法。 Echidna 在几分钟内通过生成随机交易序列来存入抵押品并检查 不变式 来打破了 不变式。

形式化验证是否注定要失败？

形式化验证工具需要大量的领域特定知识才能有效地使用，并且需要大量的工程工作才能应用。 Runtime Verification 的首席执行官 Grigore Rosu 总结如下：

图 3：Runtime Verification Inc. 创始人的一条 推文

虽然形式化验证工具在不断改进，从而减少了工程工作量，但现有的工具都没有达到现有模糊器的易用性。 例如，Certora Prover 使形式化验证比以往任何时候都更容易访问，但对于复杂的代码库而言，它仍然远不如模糊器用户友好。 随着这些工具的快速发展，我们希望在未来形式化验证工具能够像其他动态分析工具一样易于访问。

那么这是否意味着我们永远不应该使用形式化验证？ 绝对不是。 在某些情况下，形式化验证合约可以提供额外的信心，但这些情况很少见且特定于上下文。

仅当以下情况属实时，才考虑对你的代码进行形式化验证：

• 你正在遵循 不变式 驱动的开发方法。
• 你已经使用模糊测试测试了许多 不变式。
• 你对哪些剩余 不变式 和组件将受益于形式化方法有很好的理解。
• 你已经解决了所有其他会降低你的 代码成熟度 的问题。

编写好的 不变式 是关键

多年来，我们观察到 不变式 的质量至关重要。 编写好的不变式是 80% 的工作量； 用于检查/验证它们的工具固然重要，但却是次要的。 因此，我们建议从最简单、最有效的技术（模糊测试）开始，并且仅在适当的时候依赖形式化验证方法。

如果你渴望改进你处理 不变式 的方法并将它们集成到你的 开发过程 中，请联系我们 以利用我们的专业知识。

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