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

我们最近推出了新服务「不变式开发即服务」。经常有人问我们：「为什么选择模糊测试而不是形式化验证？」答案是：「这很复杂。」

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

本文将探讨支持形式化验证的两个主要主张为何常常站不住脚：证明无缺陷通常无法实现，且模糊测试能发现形式化验证所揭示的相同缺陷。

证明无缺陷

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

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

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

具体来说，我们首先严格形式化了增量Merkle树算法。然后，我们提取了存款合约中采用的算法的伪代码实现，并正式证明了伪代码实现的正确性。
复杂代码可能需要自定义功能摘要进行分析：在这种情况下，验证依赖于自定义摘要的正确性，这将正确性的责任转移到了该摘要上。构建此类摘要可能需要使用额外的自定义语言（如CVL），从而增加了复杂性。
循环和递归可能需要添加手动约束（例如，仅展开循环给定次数）以帮助证明器。例如，Certora证明器可能会将某些循环展开固定次数的迭代，并将任何额外的迭代报告为违规，迫使用户进一步参与。
求解器可能超时：如果工具依赖求解器求解方程，可能无法在合理时间内找到解决方案。特别是，证明具有大量非线性算术操作或存储/内存更新的代码具有挑战性。如果求解器超时，则无法提供保证。

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

发现缺陷

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

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

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

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

DAI的基本不变式

MakerDAO在四年后在其实时代码中发现了一个缺陷。您可以在《当不变式不是：DAI的Certora惊喜》中阅读更多关于该缺陷的信息。使用Certora证明器，MakerDAO发现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：Solidity中DAI不变式的基本方程

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

Compound V3 Comet中抵押账户的清算

Certora团队使用他们的Certora证明器在Compound V3 Comet智能合约中发现了一个有趣的问题，该问题允许完全抵押的账户被清算。此问题的根本原因是對16位向量使用了8位掩码。掩码对于向量中的高位保持为零，这在计算总抵押时跳过资产，并导致抵押账户的清算。关于此问题的更多信息可在《Compound V3（Comet）形式化验证报告》中找到。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23


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.创始人的推文 「形式化验证：需要PhD。模糊测试：需要耐心。」

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

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

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

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

编写良好的不变式是关键

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

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

如果您喜欢这篇文章，请分享： Twitter | LinkedIn | GitHub | Mastodon | Hacker News

页面内容

证明无缺陷
发现缺陷
DAI的基本不变式
Compound V3 Comet中抵押账户的清算
形式化验证注定失败吗？
编写良好的不变式是关键

最近文章

使用Deptective调查您的依赖项
系好安全带，Buttercup，AIxCC的评分回合正在进行中！
使您的智能合约超越私钥风险
Go解析器中意想不到的安全隐患
我们从审查首批DKLs中学到了什么
Silence Laboratories的23个库

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

本文探讨了在智能合约审计中模糊测试相比形式化验证的优势。通过实际案例证明模糊测试能更高效地发现相同漏洞，同时分析了形式化验证在实际应用中的局限性，包括代码改写需求、求解器超时等问题。