为何选择模糊测试而非形式化验证？

我们近期推出了新服务“不变式开发即服务”。一个常被问到的问题是：“为什么选择模糊测试而不是形式化验证？”答案是：“这很复杂。”

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

在这篇博客文章中，我们将探讨支持形式化验证的两个主要主张为何往往站不住脚：证明无漏洞通常不可实现，且模糊测试能识别形式化验证发现的相同漏洞。

证明无漏洞

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

虽然这种主张在简单代码库上可能实现，但在实践中并不总是可行，尤其是对于复杂代码库，原因如下：

• 代码可能需要重写以适应形式化验证。这导致验证的是目标的伪副本而非目标本身。例如，Runtime Verification 团队验证了 ETH2.0 升级存款合约的伪代码，如他们博客文章摘录所述：

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

• 复杂代码可能需要某些功能的自定义摘要进行分析。在这些情况下，验证依赖于自定义摘要的正确性，这将正确性责任转移到了该摘要上。构建此类摘要可能需要使用额外的自定义语言（如 CVL），从而增加了复杂性。

• 循环和递归可能需要添加手动约束（例如，仅展开循环给定次数）以帮助证明器。例如，Certora 证明器可能将某些循环展开固定次数的迭代，并将任何额外迭代报告为违规，迫使用户进一步参与。

• 求解器可能超时。如果工具依赖求解器解方程，在合理时间内找到解决方案可能不可行。特别是，证明具有大量非线性算术操作或存储/内存更新的代码具有挑战性。如果求解器超时，则无法提供保证。

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

发现漏洞

当无法正式验证代码时，形式化验证工具仍可用作漏洞发现工具。然而，问题仍然是：“形式化验证能否找到模糊测试器无法找到的真正漏洞？”此时，使用模糊测试器不是更简单吗？

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

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

我们的模糊测试器在典型开发笔记本电脑上运行几分钟内就找到了这两个漏洞。我们评估的漏洞以及用于发现它们的形式化验证和模糊测试工具可在我们的 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 证明器在 Compound V3 Comet 智能合约中发现了一个有趣的问题，该问题允许完全抵押的账户被清算。此问题的根本原因是使用 8 位掩码处理 16 位向量。掩码在向量的高位保持为零，这在计算总抵押时跳过资产，导致抵押账户被清算。更多关于此问题的信息可在《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 的 CEO Grigore Rosu 总结如下：

图 3：Runtime Verification Inc.创始人的推文“形式化验证：需要付出努力。但一旦完成，您就获得了保证。模糊测试：易于设置。但您永远不知道什么时候完成。”

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

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

仅当以下情况成立时才考虑对代码进行形式化验证：

• 您遵循不变式驱动开发方法。

• 您已经使用模糊测试测试了许多不变式。

• 您清楚了解哪些剩余不变式和组件会从形式化方法中受益。

• 您已经解决了所有其他会降低代码成熟度的问题。

编写良好的不变式是关键

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

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

如果您喜欢这篇文章，请分享：TwitterLinkedInGitHubMastodonHacker News

页面内容证明无漏洞发现漏洞 DAI 的基本不变式 Compound V3 Comet 中抵押账户的清算形式化验证注定失败吗？编写良好的不变式是关键近期文章使用 Deptective 调查您的依赖项系好安全带，Buttercup，AIxCC 的评分回合正在进行中！使您的智能合约超越私钥风险成熟 Go 解析器中意外的安全陷阱我们从审查首批 DKLs 中学到的东西 Silence Laboratories 的 23 个库© 2025 Trail of Bits。使用 Hugo 和 Mainroad 主题生成。更多精彩内容 请关注我的个人公众号 公众号（办公 AI 智能小助手）公众号二维码

办公AI智能小助手