Certora技术白皮书

作者: Daniel Jackson , Chandrakana Nandi , Mooly Sagiv 编辑: Sameer Arora , Uri Kirstein

Certora 是消除智能合约中的漏洞的技术和服务的领先提供商。本文档概述了使 Certora 独特的技术，解释了其优势和当前的局限性。

Certora 工具套件

Certora 提供了一套用于审计智能合约的工具，包括漏洞检测和生成确保基本属性始终有效的证明。本文假设读者已熟悉智能合约的基本概念。本文档中提到的示例的更多细节可以在我们 网站 的 演示 部分找到。

工具套件的核心是 Certora Prover，这是一个验证工具，接受低级 EVM 字节码程序 和用 CVL (Certora 验证语言) 编写的规范。Prover 通过共同分析代码和规范来识别代码偏离规范的场景。该技术自动找出即使是最优秀的审计员也可能遗漏的关键漏洞，并通过证明某些关键属性得到满足来增强代码安全性。

从高层来看，Certora Prover 本质上是一个复杂的编译器，将智能合约字节码和指定的属性翻译成一个数学公式，该公式简洁地定义了程序可能违反属性中指定的预期行为的确切条件。这个公式被输入到最先进的开源求解器中，这些求解器检查可能执行的无限空间并找到任何违反场景，然后由编译器转换回智能合约的领域。

此外，Certora 还拥有用于分析合约复杂性、使用突变检测进行规范检查、以及轻量级验证的模糊器工具。

验证与审计

由于智能合约中的漏洞可能使合约创作者及其用户面临巨大的损失，合约开发者急于在其合约部署前消除漏洞。许多安全公司提供基于人工审计的服务，或者通过漏洞奖励计划进行外包审计。

人工审计虽然至关重要，但存在严重的局限性。Certora 的工具套件在许多方面互补它们：

(1) 自动重新检查。每次代码更改时，都需要新的审计，这需要雇佣相同的外部审计团队。提前安排周期性的审计可能是一个重大的运营挑战；相同项目的不同版本可能最终会遭遇不同的审计员，因此丢失了项目代码库/关注事项的历史上下文。相比之下，Certora 的方法让开发者在开发过程早期就可以指定重要属性，这些属性在每次代码更改时都可以自动重新检查——指定一次，经常验证！

(2) 协作规范化。审计通常由具有广泛一般经验的外部安全人员进行，但可能缺乏对特定合约的深入，先前的理解。Certora 的基于属性的方法让开发者和审计员能够共同制定属性，这些属性记录了合约的安全相关方面，允许检测到更特定于应用的、更深层次的逻辑缺陷。

(3) 更强的保证。审计员的任何小错误或忽视都可能导致丢失关键漏洞。Certora 工具套件即使在经过大量审计后也发现了重大漏洞。这并不令人惊讶，因为人工审计中几乎不可避免地会出现错误。另一方面，使用 Certora 工具的用户则专注于属性本身的指定。由于属性的检查是完全自动化的，成功的检查在数学上 保证该属性成立：与人工审计员不同，Prover 从不产生推理错误。检查失败的情况下有助于开发者定位失败的场景。

(4) 随时可用性。最优秀的审计员通常提前 18 个月就会被预约。由于陡峭的学习曲线、缺乏结构化的入职资源/措施以及对审计员高期望，以太坊可能在可预见的未来继续经历代码安全专业人才的严重短缺。由于 Certora 的方法利用自动验证技术来减少需要的重复工作量，其服务对于能够指定代码属性的开发者/专家而言更加容易获得。

(5) 向左转。Web3 中的安全软件开发生命周期不幸地被缩减为 3 步“构建-审计-发布”的线性时间线，其中审计阶段的期望巨大且不切实际，这是不可持续的。开发者/专家使用 Certora 的工具来指定和检查安全属性将催化“向左转”的努力，在应用程序生命周期的早期更好地解决安全问题并显著提高安全性。

初步经验表明，审计和形式验证的结合效果良好。人工审计可以帮助指定或识别形式验证中的缺失规则，而形式验证可以识别人工审计遗漏的边缘案例，尤其是当代码随着时间不断修改时。

验证与测试

和任何软件一样，智能合约也需要测试。但由于一些局限性，测试可能不足以揭露安全缺陷。

(1) 路径爆炸。函数中的每个 if 语句都可能使执行可以采取的路径数量加倍。因此，路径通常随着代码的大小指数增长。测试很少能够覆盖即使是路径的高比例，更不用说所有路径了，因此遗漏了一些路径，这在分析中留下了危险的空白。基于验证的工具，例如 Certora Prover，考虑_每个_路径。

(2) 状态爆炸。合约的状态数量同样随着状态组件的数量指数增长。测试人员一般会尝试选择一些具有代表性的状态进行测试，以及一些异常值和一些被怀疑是棘手情况的状态。但这些只能覆盖实际中可能出现的状态的一小部分。基于验证的工具，例如 Certora Prover，考虑_每个_状态。

(3) 测试套件成本。一个全面的测试套件非常繁琐且难以编写、维护和理解。预期属性，即 Certora 技术的基础，通常要紧凑得多，因为单个属性可以泛化到大量测试用例中。

迄今为止的经验

Certora 为各种客户分析了数百个智能合约，发现了严重漏洞，如果未被检测，可能会导致重大损失。以下是 Certora Prover 检测到的一些有趣漏洞的小选集：

• 与转账相关。当发送者的地址与接收者的地址相同 (to) 时，合约可能会允许一笔交易，其中发送者将资产转移到他们自己的账户。与人们的预期相反，典型的转账代码在这种情况下会产生错误的结果，允许发送者凭空创建资产：

function transfer(address to, uint amount) public {
    uint srcBalance = balances[msg.sender];
    uint dstBalance = balances[to];
    balances[msg.sender] = srcBalance - amount;
    balances[to] = dstBalance + amount;
}

• 与偿付能力相关。Certora Prover 在多个合约中成功检测到的常见漏洞是一名用户在没有支付任何费用的情况下获得资产。我们在一些 ERC20 合约中发现了这个问题。以下部分描述的 KashiPair 案例研究就是一个此类漏洞的例子。

• 与质押相关。基于权益证明的系统根据时间段分配奖励。他们使用经过的时间计算要发送的当前奖励：block.timestamp - lastTimestamp。但如果 lastTimestamp 未在创建合约时或在开始分配奖励时初始化为 block.timestamp，那么这种时间的度量将等于 block.timestamp - 0，这是一个巨大的数字，分配的奖励数量将远超预期。

• 与边缘案例相关。CVL 的表现力特别适合编写有关智能合约中出现的数学公式的属性。一个例子是以下部分描述的著名 Maker DAO 案例研究。相关的，Certora Prover 也因计算中的溢出/下溢而发现了漏洞。

案例研究

为了展示 Certora 在实践中的影响，本节呈现三个案例研究，展示 Certora Prover 如何能够在真实和复杂的智能合约中发现漏洞。

常量乘积池

Trident 是 SushiSwap 的一个平台，用于启动和运行流动性池以及管理与用户的互动；预计将处理价值数十亿美元的 SUSHI 代币。Certora Prover 在 Trident 协议中发现了一个池 draining 攻击，该漏洞随后被 SushiSwap 修复。

此攻击与常量乘积池（CPP）的自动化做市商合约有关。在 CPP 中，流动性提供者 (LPs) 存入两种基础代币（Token0 和 Token1）以换取 LP 代币。他们可以随后“销毁”（或交换） LP 代币以回收 Token0 和 Token1 的成比例数额。Trident 用户可以通过将某种类型的代币转账到池中并收到一定数量的其他代币来将一种基础代币交换为另一种。为了确定汇率，池返回足够的代币以确保

(reserves0 ⋅ reserves1)_pre = (reserves0 ⋅ reserves1)_post

其中 reserves0 和 reserves1 分别是 Token0 和 Token1 的储备。

可以将 LP 代币转换为基础代币的能力建议了一个重要的不变量：如果存在任何 LP 代币（totalSupply > 0），则 reserves0 和 reserves1 都不应为零（否则池无法产生基础代币）。更正式地，我们编写的 CVL 属性是：

(totalSupply = 0 <=> reserves0 = 0) &&
(totalSupply = 0 <=> reserves1 = 0)

我们在 Trident 协议上运行了 Certora Prover 以验证这一不变量，并发现一种称为 burn-single 的操作违反了它。burn-single 操作结合了 burn 和 swap：它首先销毁 LP 代币以产生两种基础代币，然后将一种类型的代币交换为另一种类型（仅产生单一种基础代币）。尽管 swap() 和 burn() 操作维持了不变量，但组合操作存在一个 flaw，使恶意用户能够 draining 池中的流动资金。有关此问题的更多详细信息，请参见我们的 博客文章。

Kashi Pair

我们使用 Certora Prover 验证了 KashiPair 合约，该合约允许用户将资产作为 抵押 存入，并根据系统的利用率借入其他资产，采用灵活的预言机和利率。Certora Prover 在 KashiPair 中发现了多种漏洞。这里我们讨论了 KashiPair 违反的一种属性，称为 清算的反单调性。考虑以下显示的 liquidate 方法。该方法作为 batchCalls 方法的一部分被调用，该方法会触发多笔交易。

/*
* 清算处于无偿还状态的用户。
*  user - 要清算的地址
*  to   - 收取抵押品的地址
*/
function liquidate(address user, address to) public {
  require(!_isSolvent(user), "用户是有偿还能力的");
  uint256 borrow = userBorrowAmount[user];
  uint256 collateral = userCollateralAmount[user];
  userBorrowAmount[user] = 0;
  userCollateralAmount[user] = 0;  // msg.sender 将 borrowToken 转账给系统，而 `this` 合约
  // 将 collateralToken 转账给 'to'
  borrowToken.transferFrom(msg.sender, address(this), borrow);
  collateralToken.transfer(to, collateral);
}
/*
* 允许以批处理模式调用几个函数
* 和与其他合约互动。
*/
function batchCalls (address[] calldata callee, bytes[] calldata datas) external {
  ...
  callee[i].call(datas[i]);
}

liquidate 的一个重要属性是 borrow 和 collateral 必须成反比，即，

// 在调用 liquidate 之前
{
  b = borrowToken.balanceOf(system) &&
  c = collateralToken.balanceOf(system)
} liquidate(x, y) // 在调用 liquidate 之后
{
  borrowToken.balanceOf(system) > b <=> 
  collateralToken.balanceOf(system) < c
}

这个属性是在 CVL 中编写的（有关如何编写这些属性的更多详细信息，请参见后面的“规则”部分），由 Certora 团队与 SushiSwap 团队共同编写，并发现了一个违规情况。结果发现，在此版本的 liquidate 中，可以使用 batchCalls 调用 liquidate，其中 msg.sender 设置为当前合约的地址，这允许系统将抵押品转移到当前合约而不需要支付任何金额。随后，SushiSwap 团队通过在 liquidate 方法顶部添加未允许 msg.sender与当前合约地址相同的额外要求，修复了此漏洞。

require(msg.sender != address(this));

更多细节可以在我们的 验证报告 中找到。

Maker DAO

Maker 协议 由创建和维持 DAI 稳定币的智能合约组成。DAI 由 债务 支持。债务要么分配给 Vault，意味着与某个抵押资产有关联，要么是“无担保的”，意味着它由协议（即 MKR 持有者）的责任。这两个债务来源相加后，应等于所有 DAI 余额的总和。这个关键不变量被称为 DAI 的“基本等式”（Fundamental Equation of DAI，FEoD）：

dai == vice + sumOfVaultDebt

其中 dai 是所有 DAI 余额的总和，vice 是总的无担保债务。FEoD 是最著名的多抵押 DAI “不变量”，自 2018 年以来人们就已经知道，直到最近，人们认为这是数学上可证明的。Maker 团队与 Certora 一起将该不变量记录在 CVL 中，并使用 Certora Prover 来证明这一点。

令人惊讶的是，Prover 发现了这一不变量的违规，并生成了一个具体的反例，显示在所谓的 init() 函数执行后该属性不成立。重要的是，反例显示该属性在“前状态”（即 init()被调用之前）为真，但在“后状态”（即 init() 执行后）不再成立。这种反例被称为归纳反例，即它显示系统从一个属性为真的状态过渡到一个违反该属性的状态（有关不变量的更多详细信息，请参见 后面部分）。反例可能不是一个“真实”反例，即“坏”转变的起始状态可能实际上无法达到。这在不变量的定义未能涵盖一些系统属性时会发生。然而，在这里并不是这种情况。Maker 团队实际上确定了一系列函数调用 序列，这可能在实践中导致这些违规情况。

协议的下一个版本将进行修复，以确保该不变量得到满足。有关在编写规范中使用的 CVL 功能的更多详细信息，请参见最近的 博客文章。

关键特性

1. 完全自动化的验证

Certora Prover 提供一键式验证。用户编写规范并将智能合约和规范作为参数传递给 Certora Prover。从那时起，用户不需要干预验证过程。最终，Certora Prover 生成一份用户友好的报告，其中列出了满足的属性和未满足的属性。

2. 生成反例场景

仅仅知道智能合约未满足某个属性不足以让用户理解合约可能存在的漏洞。因此，Certora Prover 更易于通过为用户提供一个反例来解释验证结果。反例表示智能合约的一个具体状态，这有助于用户缩小规范违反的根本原因。

3. 丰富的规范语言

与传统的单元测试不同，传统的单元测试描述特定输入的输出，Certora Prover 要考虑整个（可能是无限）的可能输入空间。与其编写大量测试用例，不如编写更紧凑和更通用的 CVL 规范。CVL 支持不变量、参数函数、未解释函数、可以对合约状态进行建模的“幽灵”函数和关系属性。这允许推理关于无限行为，也允许程序之间的等价性检查（例如，进行代码重构不会引入新的行为）。

4. 强大的互动支持

由于形式验证是一个不可判定的问题，因此始终会有一些属性对某些程序无法进行自动验证。Certora Prover 提供了一套丰富的功能来近似难以验证的代码，给予用户细粒度的工具以在健全性和完整性之间做出权衡。这些工具包括： (1) 限制执行的循环迭代次数或提供检查的循环不变式；(2) 将大型代码分解为若干部分，以便于模块验证。

5. 规范检查。形式验证中最困难的挑战之一是提出正确的规范。规范中的错误可能会导致用户错误地得出自己合约正确实现的结论。因此，Certora 实施了一些技术，用于防止某些糟糕规范模式。例如，形如 x = 5 ==> x > 0 的重言不变式将被系统标记为潜在的错误规范。Certora 还提供了一种突变验证工具，该工具自动生成和验证通过变异代码生成的原合约的变体。通过验证的突变可能表明规范存在可以修复的漏洞。

设计原则

Certora 的方法是基于几个设计原则：

1. 验证你所执行的内容。

该工具套件是在 EVM 字节码上构建，而不是 Solidity 代码上。这一决定显著提高了安全性，因为我们验证的是实际执行的代码。特别是，它不信任生成 EVM 字节码的编译器（例如，Solidity 编译器）。这一决定确实增加了验证问题的复杂性，因为编译器通常生成复杂的优化代码。在转换过程中某些信息会丢失，这增加了验证的复杂性，并在验证失败时还增加了诊断难度。然而，Certora Prover 能够执行静态程序分析，以在可能的情况下重建这些信息，以帮助用户诊断反例。

2. 信任但验证

EVM 提供了一个丰富的接口。此外，生成 EVM 字节码的编译器利用动态加载，使得通用验证几乎不可能。因此，我们对分析的 EVM 字节码施加了一些限制，以使验证可扩展。我们的静态分析算法强制实施这些限制。当静态分析算法失败时，我们会分析失败情况。在 一些 情况下，这反映出 Solidity 编译器中的漏洞，并将报告给 Solidity 团队。我们还在不断努力改进和概括静态分析，以支持更多智能合约。

3. 将规范与代码分开

CVL 规范是在单独的文件中编写的，使其能够跨不同版本的相同合约使用。此外，Certora 还策划了一个通用正确性属性数据库，可以轻松适应不同的合约。使用独立的规范语言也使得在不同智能合约语言（如 Vyper）及其他区块链（如 Solana）之间使用属性变得更加容易。

技术细节

本节提供有关如何使用 Certora 工具套件指定和检查属性的更多详细信息。

形式规范

软件开发中最大的挑战之一是指定程序的预期行为。开发人员通常使用单元测试来指定给定输入的预期输出，但单元测试只能枚举有限数量的输入场景进行测试。与单元测试相比，CVL 中的规范描述了_每个_可能的输入的预期输出。由于本文只描述了 CVL 规范中使用的一些机制，因此我们将读者参考完整的 参考手册。

归纳不变量

程序是状态转换系统的描述。程序的规范是应该在状态转换系统的所有可达状态上保持的谓词。如果它实际上在所有可达状态上都符合，它就是一个不变量。如果不在所有可达状态保持，则程序存在漏洞。导致程序进入一个不满足规范的状态的输入是一个反例。它表明该规范对程序_不是_不变量。例如，在一个保持银行账户余额的合约中，不变量可能要求总余额等于所有余额的总和。

归纳不变量是通过任意执行保持的 invariant 。归纳不变量必须在转换系统的所有初始状态下成立。此外，当在满足不变量的某个任意状态 s 中执行一个转换，并把 s 转移到状态 s'，则不变量必须在 s' 中成立。归纳不变量可以保证，无论执行的指令数量如何，程序都是正确的。归纳反例是从一个满足不变量的状态转换到一个违反不变量的“坏”状态。

与前面描述的常规反例不同，归纳反例_并不_一定表明程序存在漏洞，因为它可能反映出程序可能无法达到的状态；它只能表明规范不是归纳性的。这些规范可以通过_加强_变得归纳。 这模仿了归纳法的证明。要了解更多关于归纳不变量的信息，我们推荐读者观看 这个视频。你还可以在 文档 中了解有关 CVL 中不变量的更多信息。

规则

CVL 中的 规则 描述了系统可能过渡的属性。在智能合约中，这种过渡可以通过调用函数来完成。因此，可以将规则视为围绕被验证的智能合约中调用的函数的一个“包装器”。调用被谓词“包裹”，在函数调用前后必须保持。规则必须描述：（1）转换前的状态，（2）转换，（3）转换后的状态。描述状态意味着对可能状态集设置要求。描述转换意味着指定哪个函数被调用以及输入满足的条件。使用 霍尔三元组 符号，规则可以写为：

{ state before };f(function inputs);{ state after };

例如，我们可能希望在用户 Bob 向池合约执行存款调用时跟踪用户 Alice 的余额变化。以上三元组可以表示为：

{ uint256 x = BalanceOf(Alice) };deposit(Bob, amount);{ BalanceOf(Alice) == x };

通过约束求解进行验证

Certora Prover 比较字节码的行为与规范，以查找漏洞并正式证明其不存在。直观地说，想法是将 EVM 的语义和规范建模为一种称为 SMT （满足性模理论简称）的逻辑公式。SMT 公式是关于符号变量的约束。符号变量与程序变量非常不同——它们的值可以是任意的。例如，公式 x * x > 4 是可满足的，比如 x = 3。然而，公式 x * x + 1 < 0 是不可满足的。 SMT 的求解器能够生成一个正式证明，表明此公式对任何 x 都不可满足，同时也能够为前一个公式生成一个满足的模型。接下来的小节中我们将以简单的步骤解释验证过程。

布尔满足性

计算机科学中的经典问题是布尔满足性：给出对逻辑变量 v1, v2, ..., vk 的布尔公式（0, 1），是否存在一种值使该公式为真。例如，a && !a 对于 a = true 和 a = false 都是 false，因此不可满足。对于 n 个变量的满足性问题可以通过枚举所有的 2^n 组合来解决。随着 n 增长，这变得迅速不可行。更糟糕的是，一个著名的计算机科学理论结果表明这个问题本质上是不可解决的：没有算法能够比暴力枚举更有效地解决每一个实例。然而，在实践中，人们发现实际上出现的大多数问题instances 是可以有效解决的，因此开发了一个名为 SAT 求解器的广泛工具生态系统。现代 SAT 求解器往往能够在几秒钟内找到数千行变量的公式。

通过减少到满足性进行形式验证

给定一个无限循环解除的程序和有关它的一个断言，可以使用布尔满足性进行验证。例如，图1展示了一个小程序的控制流。为了确定程序末尾的断言是否有效，我们检查 SAT 查询：

((a ∧  x) ∨ (¬a ∧ ¬x)) ∧
((b ∧  y) ∨ (¬b ∧ ¬y)) ∧
((x ∧ ¬y) ∨ (¬x ∧  y))

注意，这个公式紧凑地定义了程序的四条路径。SAT 求解器确定对于 a = 0 和 b = 1，x 和 y 的值分别为 0 和 1，这表明断言存在违反。

图 1：带有断言 X == Y 的程序控制流，对于所有情况均不为真。

现代 SAT 求解器也可以在没有枚举所有值的情况下确定公式是不满足的。他们使得能够正式验证程序在所有路径上的正确性。例如，图 2 显示了一个有效断言的代码片段。

图 2：一个有有效断言的示例。

在这种情况下，SAT 查询：

((a ∧ x ∧ b) ∨ (¬a ∧ ¬x ∧ ¬b)) ∧
((b ∧ y)     ∨ (¬b ∧ ¬y))      ∧
((x ∧ ¬y)    ∨ (¬x ∧ y))

对所有的 a、b、x 和 y 的值是不可满足的。因此，断言是有效的。

超越布尔：SMT

布尔公式仅适合表示有限状态空间。对于智能合约来说，状态空间通常由结构（如数组）构成，这些状态是无界的，因此需要更丰富的满足性概念。

SMT（满足性模理论）正是为这个目的而开发的，扩展了以往应用于 SAT 的约束求解到更一般的公式。

人们已经存在许多求解 SMT 约束的开源软件，包括 Z3、CVC5、Yices 和 Vampire。Certora 验证器利用了所有这些求解器。这些求解器能够生成反例并在许多有趣的情况下提供正式证明。

使用静态分析加速约束求解

智能合约通常使用复杂的数学公式，其中涉及非线性算术。SMT 求解器解决这些查询存在困难。此外，Solidity 编译器生成了以不平凡的方式操作内存的非平凡指令，通常使用动态加载来隐藏程序的控制流。这些策略使得使用 SMT 求解器进行有关程序正确性的形式推理变得更加困难，需要求解器推断有关程序的复杂事实。

为此，Certora 开发了复杂的静态分析算法（也称为抽象解释），以在预处理阶段从字节码中自动推断非平凡不变量。

对于许多常见程序，Certora 的静态分析算法可以减少 SMT 求解的复杂性，同时又不会牺牲覆盖率。例如，考虑以下 EVM 代码片段：

l1: mem[index] = “foo()”;
l2: mem[index + 4] = x;
l3: mem[otherIndex] = 44;
l4: send(contract, mem[index .. index + 36])

求解器需要确保在第 l4 行 send 命令中唯一调用的方法是 foo。这需要证明第 l2 和 l3 行对内存的写入不会改变 mem[index] 的内容。这通常是不判定的问题，推理这种情况的技术称为指针分析。Certora Prover 实现了指针分析，通过执行对编译器生成的内存访问模式的限制，以便在许多情况下解决这个问题。

模块化

自动验证合约是否满足某个规范在理论上是一个不可判定的问题，并且在实践中可能具有高复杂性。为了减少完成证明所需的资源，Certora Prover 的用户可以采用几种方法来简化问题。一个重要的技术类是基于模块化，即将验证问题分解成多个独立的子问题。

在模块化验证中，用户从智能合约中选择一些方法进行总结。总结近似方法的行为。通过用其总结替换该方法，用户简化了 Certora Prover 的整体验证问题。许多不同类型的总结都是可能的。例如，可以将方法的主体总结为返回任意值、常量、某种幽灵状态或其他简化的描述。

通过总结，不必一次性验证整个程序，问题被分解成两类子问题。第一，在程序的整个验证条件中，我们使用其总结，而不是使用该方法的定义。第二，我们检查该方法的总结是实际方法定义的一个正确近似。在实践中，有时可以省略第二个检查，以给予规则编写者最大的灵活性。

Certora Prover 架构

Certora Prover 实现了一个复杂的工具链，以验证低级代码。它目前支持 EVM 字节码，但其工具链是通用的，可以适应其他字节码，例如 eBPF 和 Web Assembly。

图 1 描述了 Certora Prover 的架构。它对 EVM 字节码进行操作，这是一种基于栈的语言。反编译器将每个栈位置映射到一个称为寄存器的符号值，然后将字节码指令转换为寄存器上的指令。这种表示方式称为 TAC。流行的 Soot 静态分析框架中实现了类似的技术。静态分析算法然后推断关于代码的可靠不变量，从而大大简化验证任务。接下来，VC（验证条件）生成器输出一组数学约束，描述程序能够违反规则的情况。最后，Certora Prover 调用现成的 SMT 求解器，这些求解器自动搜索数学约束的解决方案，这些解决方案代表违反规则的情况。如前所述，这是一个不可判定的问题，这些求解器在某些情况下“确实”可以通过超时失败。Certora Prover 从求解器获得结果，处理它以生成详细报告，并将报告呈现给客户/Prover 用户。

图 3： Certora Prover 架构

相关工具和其他方法

智能合约的正确性在工业界和学术界均得到了相当大的关注。以下是一些使用与 Certora 相似或正交的方法的相关工具。

单元测试和模糊测试

使用 Foundry、MythX、Manticore 和 Echidna 等工具对智能合约进行测试和模糊测试非常有效。Certora Prover 通过使用强大的 CVL 规范和利用 SMT 求解器来识别可能罕见的路径显示出覆盖率的优势。

传统静态分析

可以使用直接在源代码上工作的轻量级静态分析工具，如 Slither，来识别智能合约中可能存在的漏洞。相比之下，Certora Prover 在字节码级别运作，提供更强的保证。它提供规则违反的证据和被验证规则的正式正确性保证，而这些都是不考虑控制流的简单静态分析所无法做到的。然而，这使得 Certora Prover 的计算开销更大，并且在大型合约上运行速度更慢。

证明助手

诸如 K、Coq 和 Isabelle/HOL 的证明助手实现了完全不同的方法来获取可证明正确的代码。程序员编写有关模型的数学证明，并且额外的工具从证明中提取代码。相比之下，使用 Certora Prover 可能更像是单元测试和模糊测试。在 Certora Prover 中，字节码被验证的基础真相是高层 CVL 规范。

结论

Certora Prover 支持推理_所有_以太坊字节码程序的执行。Prover 作为输入字节码程序以及用 CVL 编写的规范。Prover 的目标是检查字节码的所有执行是否符合规范。它通过分析字节码并将其转换为与规范一起形成的一系列约束来实现这一点。这些约束随后由一套基础的 SMT 求解器进行求解。求解器要么报告所有执行是正确的，要么返回导致执行违反规范的特定输入。在这两种情况下，信息被转换为高级格式并展示给用户。

使用任何形式验证技术的主要挑战是复杂性。对于实际合约和规范，Prover 生成的约束可能会给求解器带来很大的挑战。在这些情况下，用户可以通过总结复杂的代码片段来细分证明。通过良好的总结，每个证明的部分均可由求解器处理，这些部分组合起来证明原始规范。

• 原文链接： medium.com/certora/certo...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～