模糊测试 vs. 形式化验证：为何选择前者？

原创

qife122

发布于 2025-08-25 09:49:14

1670

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

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

我们在大多数审计中使用模糊测试，但过去也使用过形式化验证方法。特别是在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通过生成随机交易序列来存入抵押并检查不变式，在几分钟内打破了不变式。