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

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

尽管我们在多数审计中使用模糊测试，但过去也曾采用形式化验证方法。尤其在Sai、Computable和Balancer等审计中，符号执行被证明有效。然而经验表明，模糊测试工具能产生类似结果，且所需技能和时间显著更少。

本文将剖析支持形式化验证的两个主要论断为何往往不成立：证明无缺陷通常无法实现，且模糊测试能发现形式化验证所揭示的相同漏洞。

证明无缺陷的局限性

形式化验证的核心优势是能证明无缺陷。其通过数学表示检查给定不变式是否对系统所有输入值和状态成立。但该目标仅在简单代码库中可行，复杂代码库中常因以下原因无法实现：

代码需重构以适应验证：导致验证的是目标伪副本而非目标本身。例如Runtime Verification团队验证ETH2.0升级存款合约的伪代码时，需先形式化增量Merkle树算法，再证明伪代码实现的正确性。
需自定义功能摘要：复杂代码要求为部分功能创建自定义摘要，验证的正确性依赖于这些摘要，且可能需使用CVL等额外自定义语言增加复杂度。
循环与递归需手动约束：例如Certora验证器可能固定次数展开循环，并将额外迭代报为违规，需用户进一步干预。
求解器超时：涉及大量非线性算术操作或存储更新的代码难以在合理时间内求解，超时则无法提供保证。

因此，证明无缺陷在理论上虽是形式化验证的优点，实践中却常难以实现。

漏洞发现能力对比

当形式化验证不可行时，其工具仍可用于发现漏洞。但问题在于：「形式化验证能否找到模糊测试无法发现的真实漏洞？」此时，直接使用模糊测试是否更简便？

为回答该问题，我们研究了MakerDAO和Compound中通过形式化验证发现的两个漏洞，并尝试仅用模糊测试复现。结果：我们成功了。

选择这两个漏洞因其被广泛宣传为形式化验证发现，且影响流行协议。值得注意的是，纯形式化验证发现的公开问题较少，而模糊测试发现大量漏洞（参见我们的安全评审）。

DAI的基本不变式漏洞

MakerDAO在运行四年后的代码中发现漏洞（详见《当不变式失效：DAI的Certora意外》）。使用Certora验证器发现，DAI的基本不变式（所有抵押债务与无抵押债务之和应等于DAI总余额）在特定情况下可被违反。核心问题是：当金库Rate状态变量为零且Art非零时调用init函数，会改变金库总债务，违反债务总和与DAI供应量不变的检查。MakerDAO团队总结称，在调用fold后调用init函数会破坏不变式。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12


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：DAI基本不变式的Solidity实现

我们在Solidity中实现相同不变式（图1），并用Echidna检查。Echidna在不到一分钟内违反该不变式并找到触发路径。代码详见仓库Testvat.sol文件。因被测代码较小且仅需计算债务总和逻辑，实现过程简单。

Compound V3 Comet抵押账户清算漏洞

Certora团队使用其验证器发现Compound V3 Comet智能合约中允许完全抵押账户被清算的异常问题。根本原因为对16位向量使用8位掩码，导致高位资产在计算总抵押时被跳过。详情参见《Compound V3形式化验证报告》。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


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;
}

图2：Compound V3 Comet不变式的Solidity实现

Echidna通过实现图2所示不变式发现该问题。代码详见TestComet.sol文件。实现需限制与测试合约交互的用户数，并添加计算用户抵押总和的方法。Echidna在几分钟内通过随机交易序列破坏不变式。

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

形式化验证工具需大量领域知识且工程投入显著。Runtime Verification CEO Grigore Rosu总结如下：

「形式化验证工具虽持续改进以降低工程成本，但尚无工具能达到模糊测试的易用性。」（图3：Runtime Verification创始人的推文）

例如Certora验证器虽提升了形式化验证的可访问性，但对复杂代码库仍远不如模糊测试友好。随着工具快速发展，我们期待形式化验证能像动态分析工具一样易用。

这是否意味着应完全弃用形式化验证？绝非如此。在某些场景下，形式化验证能提供额外信心，但这些情况罕见且依赖具体上下文。

仅当满足以下条件时考虑形式化验证：

采用不变式驱动开发方法
已用模糊测试验证大量不变式
清楚哪些剩余不变式和组件适合形式化方法
已解决所有降低代码成熟度的问题

关键在于编写优质不变式

多年来我们观察到不变式质量至关重要。编写优质不变式占80%的工作，验证工具虽重要但属次要。因此建议从最简易高效的模糊测试入手，仅在适当时机采用形式化验证。

若您希望优化不变式策略并集成至开发流程，欢迎联系我们的专家团队。

（原文结束）

模糊测试为何优于形式化验证？关键发现与实战案例

本文通过对比模糊测试与形式化验证在智能合约审计中的实际效果，结合MakerDAO和Compound的真实漏洞案例，揭示模糊测试在效率与可访问性上的显著优势，并探讨形式化验证的适用边界与技术挑战。