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

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

我们在大多数审计中使用模糊测试，但过去也使用过形式化验证方法。特别是在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智能合约中的一个有趣问题，该问题允许完全抵押的账户被清算。此问题的根本原因是使用8位掩码处理16位向量。掩码在向量的高位保持为零，这在计算总抵押时跳过资产，导致抵押账户被清算。关于此问题的更多信息可在《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.创始人的推文 虽然形式化验证工具不断改进，减少了工程努力，但现有工具都没有达到现有模糊测试器的易用性。例如，Certora证明器使形式化验证比以往更容易访问，但对于复杂的代码库，它仍然远不如模糊测试器用户友好。随着这些工具的快速发展，我们希望未来形式化验证工具能像其他动态分析工具一样易于访问。

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

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

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

编写良好的不变式是关键

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

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

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