Certora技术白皮书

Certora 工具套件

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

该工具套件的核心是 Certora Prover，一个验证工具，接受低级合约字节码（例如，EVM 字节码程序、Solana eBPF 对象 或 Stellar WASM 对象），以及用 CVL（Certora 验证语言） 或 CVLR（Certora 验证语言 Rust 版） 编写的规范。Prover 将代码和规范结合起来进行分析，以识别代码偏离规范的场景。该技术能够自动定位即使是最佳审计员也可能遗漏的关键漏洞，并通过证明某些关键属性得以满足，从而增强代码安全性的信心。

开发人员和安全研究人员都可以通过使用 Certora Prover 获益。对于开发人员来说，Prover 提供的保证超出了测试或模糊测试，其设置所需的样板代码和工具也更少。研究人员也可以使用 Prover 映射攻击向量，并选择重点关注的领域。

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

此外，Certora 还开发了更多工具：

• Gambit，用于确保使用突变和无效检测提高规范质量
• Safeguard，用于监控以太坊节点中的不变量
• Quorum，用于捕捉治理提案有效载荷中的错误。

验证与审计

由于智能合约中的漏洞可能会使合同的创建者和其用户面临巨大的损失，因此合约开发人员急于在合同部署之前消除漏洞。许多安全公司基于人工审计提供服务，或者是通过漏洞赏金计划进行外部审计。

人工审计虽不可或缺，但具有严重的局限性。Certora 的工具套件在许多方面补充了这些局限：

(1) 自动重检。每当代码发生变化时，都需要进行新的审计，这需要聘请同一团队的外部审计员。提前安排定期审计在预定周期内可能是一项重大运营挑战；因此，同一项目的不同版本可能会聘请不同的审计员，导致项目代码库/关注事项的历史上下文丢失。相反，Certora 的方法允许开发人员在开发过程的早期指定关键属性，从而在代码每次更改时自动进行重新检查 — 指定一次，验证多次！

(2) 协作编码。审计通常由外部安全人员进行，他们通常拥有广泛的一般经验，但可能缺乏对特定合约的深入理解。Certora 的基于属性的方法使开发人员和审计员能够共同制定规范，编码与合约安全相关的方面，从而允许检测到更具体和更深层次的逻辑缺陷。

(3) 更强的保证。审计人员的任何小失误或疏忽都可能导致关键漏洞的遗漏。Certora 工具套件即使在经过广泛的审计之后也能发现重大漏洞。这并不令人惊讶，因为人工审计中的错误几乎是不可避免的。另一方面，使用 Certora 工具的用户将所有注意力集中在指定属性本身上。由于属性检查是完全自动化的，成功的检查在数学上保证了属性的成立：Prover 与人类审计员不同，从不犯推理错误。失败的检查帮助开发人员确定失败场景。

(4) 随时可用。最好的审计员通常提前几个月被预定。由于陡峭的学习曲线、缺乏结构化的入职资源/倡议以及审计员的高期望，以太坊在可预见的未来可能将继续遭受代码安全专业人员的显著短缺。由于 Certora 的方法利用自动验证技术来减少所需的重复工作量，其服务更易于开发人员/专家使用，他们可以在代码上指定属性。

(5) 向左移动。遗憾的是，Web3 中的安全软件开发生命周期被简化为“构建-审计-发布”的三步线性时间轴，审计阶段面临着巨大的不切实际期望，这种期望是不可持续的。开发人员/专家通过使用 Certora 的工具指定和检查安全属性，将催化“向左移动”的努力，从而更好地解决安全问题，并在应用程序生命周期的早期阶段显著改善安全性。

初步经验表明，审计和形式验证可以很好地协同工作。人工审计可以帮助指定或识别形式验证中缺失的规则，而形式验证可以识别人工审计遗漏的边界情况，特别是在代码随着时间不断修改的情况下。

验证与测试

与任何软件一样，智能合约也需要进行测试。但由于一些限制，测试可能不足以揭示安全缺陷。

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

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

(3) 测试套件成本。全面的测试套件非常冗长且难以编写、维护和理解。期望的属性，作为 Certora 技术的基础，通常更为紧凑，因为一个属性可以概括大量测试用例。

验证与模糊测试

模糊测试通过自动生成大量输入来增强测试。如果使用得当，它在检测错误方面可能非常有效，但仍受路径和状态爆炸的制约。一个罕见的边缘案例可能需要生成数百万个随机输入，在找到之前可能需要数周的执行时间。

模糊测试始于一个具体的程序状态。因此，如果达到有问题的状态需要特别的函数调用链及相关的参数值，模糊测试器可能需要极其长的时间才能找到它。如果 Certora Prover 则使用数学约束求解，能够非常快速地找到这种相关性。例如， Maker 的 DAI 基本方程的问题需要用相关参数调用两个特定的函数，模糊测试花费了 13 小时和 1.25 亿次迭代才找到。相比之下，Certora Prover 仅用了 23 秒。

识别的漏洞及证明的属性

Certora 已分析了数百个智能合约，以满足各种客户的需求，发现了严重漏洞。如果不被发现，这些漏洞可能导致重大经济损失。以下是 Certora Prover 识别的一些关键漏洞及其检测到这些漏洞的属性的描述。

数据一致性

智能合约常常使用关键协议变量的多种表示。如果这些表示由于缺失或错误的更新而变得不一致，可能会出现意外行为或财务不准确。

在 Uniswap v4 中，我们通过不变量验证池的价格和 tick 之间的一致性：

tickAtSqrtRatio(pool.sqrtPrice) == pool.tick

这一不变量最初被违反，发现了一个中等严重性的错误，随后进行了修复和验证。详见 博客文章 和 规范。

在 Compound v3 中，我们证明了用户抵押物两个不同表示之间的关键关系：

userCollateral[user][asset].balance > 0 ⇔
isInAssetsIn(userBasic[user].assetsIn, getAssetOffset(asset))

这一不变量揭示并帮助解决了协议中的问题。详见 验证报告、规范 和 博客文章。

委托投票的正确总和

在 AAVE Token v3 中，我们证明了委托投票余额和未委托余额的总和等于总供应量。这个证明确保了投票权不会被重复计算或丢失。详见 验证报告 和 规范。

协议的偿付能力

协议的偿付能力意味着它持有足够的资产来覆盖所有义务。缺少偿付能力检查或对清算操作的拒绝服务 (DoS) 攻击可能导致协议无法挽回的资产损失。

在 Lido 的双重治理 中，Certora Prover 验证了负责愤怒退出资产的托管合约是保持偿付能力的，确保：

1. 托管合约持有正确数量的 stETH 和 ETH。
2. 最后提取的用户按与早期提取相同的比例接收股份。
3. UnstETH 锁定者在最终化时提取其确切的 NFT 值。

关于更多细节，请见 验证报告 和 规范。

转帐Manipulation 攻击

当一个系统容易遭受捐赠攻击，如首位存款者攻击时，这些漏洞就会出现。在这种情况下，系统不当地计算外部转移的资产或假设捐赠存款会很小。这有时会被利用，导致协议意外的资产损失。

一些关键属性可防止此类攻击：

• 灰尘有利于房屋 - 用户不应能够在一项操作中获利（例如，在单个交易中存入和提取）。
• 用户资产保护 - 当另一个用户在没有授权的情况下执行操作时，用户的总资产应保持不变。

通过加强这些属性，Certora Prover 确保协议保持对财务操纵和意外资产再分配的抵抗。

在 SushiSwap Trident 中，Certora Prover 发现了一个严重的漏洞，可以通过转移基础代币来耗尽协议。如需了解更多细节，请查看我们的 博客。

质押奖励计算错误

基于权益证明的系统周期性地分配奖励，计算奖励的方式为 block.timestamp - lastTimestamp。如果在合约创建时或开始分配奖励时，lastTimestamp 没有正确初始化为 block.timestamp，这一计算将导致 block.timestamp - 0，进而产生过大的时间差。因此，系统可能会分配比预期多得多的奖励。

在 Aave 的 StakeToken 上，我们证明了奖励申请的完整性。你可以在我们的 博客中阅读 about 一个相同规则防止的严重错误。

主要特性

1. 完全自动化验证

Certora Prover 提供一键式验证。用户编写规范，并用待验证的智能合约和规范作为参数调用 Certora Prover。从那里开始，用户不需要干预验证过程。最终，Certora Prover 会生成一个用户友好的报告，列出被满足的属性和未满足的属性。

2. 生成反 example 场景

仅仅知道某个属性未被智能合约满足，用户可能无法理解合约可能存在的漏洞。因此，Certora Prover 通过向用户呈现反例，使解释验证结果变得更容易。反例表示智能合约的具体状态，帮助用户缩小规范违反的根本原因。

3. 丰富的规范语言 与传统的单元测试不同，后者描述特定输入的输出，而 Certora Prover 考虑所有（潜在无限的）可能输入的空间。用户不必编写大量测试用例，而是使用 CVL 或 CVLR 编写更紧凑和通用的规范。

CVLR 和 CVL 允许编写符号变量，显著扩大测试覆盖率。CVL 还支持不变式、参数化函数、未解释函数、可以模拟合约状态（在合约存储中未明确存在）的“幽灵”函数和关系属性。这使得可以对无限行为进行推理，并且还允许在程序之间进行等价性检查（例如，确保代码重构不引入新行为）。

4. 强大的交互支持

由于形式验证是一个不可判定的问题，因此总会有一些属性对某些程序无法自动验证。Certora Prover 提供了一组丰富的功能，用于近似难以验证的代码，为用户提供精细化工具以权衡可靠性与完整性。这些包括：(1) 限制执行的循环迭代次数或提供检查的循环不变式 (2) 将大代码分解为几个部分，以便于模块化验证。

5. 规范检查

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

设计原则

Certora 的方法遵循多个设计原则：

1. 验证你执行的内容。 工具套件基于合约字节码（EVM 字节码、Stellar WASM 等），而不是原始源语言（如 Solidity、Vyper、Rust 等）。这一决策显著提高了安全性，因为我们验证的是实际执行的代码。特别地，它不信任生成字节码的编译器（例如，Solidity 编译器）。这一决策确实使验证问题变得复杂，因为编译器通常生成复杂的优化代码。在转换过程中会丢失某些信息，这增加了验证的复杂性，并在验证失败时使其诊断能力变得复杂。但是，Certora Prover 能够执行静态程序分析，在可能的情况下降低这一信息的丢失，帮助用户诊断反例。

2. 信任但验证 Prover 所支持的区块链使用的低级字节码允许极为复杂的行为（任意指针算术、动态控制流等），这使得通用验证几乎不可能。因此，我们对分析的字节码施加某些限制，以使验证可扩展（例如，只有有限形式的指针算术）。我们的静态分析算法强制执行这些限制。当静态分析算法失败时，我们会分析失败。在 某些情况下，这反映了源语言编译器的漏洞，我们已向相关团队报告了该问题。我们不断努力改进和概括静态分析，以处理更多智能合约。

技术细节

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

形式规范

软件开发中的最大挑战之一是明确程序的预期行为。开发人员通常使用单元测试来指定特定输入的预期输出，但单元测试只能枚举有限数量的输入场景进行测试。与单元测试不同，CVL 或 CVLR 中的规范描述对每个可能输入的预期输出。本文仅描述了 CVL 或 CVLR 规范中使用的一些机制。我们推荐读者参考包含完整细节的 参考手册。

归纳不变式

程序是状态转移系统的描述。程序的规范是一个应该在状态转移系统的所有可达状态上保持的谓词。如果它确实在所有可达状态上保持，那么它就是一个不变式。如果它并未在所有可达状态上保持，则表明程序存在漏洞。导致程序达到不满足规范的状态的输入是一个反例。它显示了规范对程序不是不变式。例如，在一个保持银行账户余额的合约中，一个不变式可能要求总余额等于所有余额的总和。

归纳不变式是通过任意执行保持的不变式。归纳不变式必须在状态转移系统的所有初始状态下保持。此外，当在满足不变式的任意状态 s 中执行转换，并且 s 步到状态 s' 时，不变式必须在 s' 时保持。归纳不变式可以保证程序是正确的，不论执行的指令数量如何。归纳反例是一种从满足不变式的状态转换到违反不变式的坏状态。

与前面描述的常规反例不同，用于归纳的反例并不一定表明程序存在漏洞，因为它可能反映了程序无法达到的状态；它可能仅表明规范并非归纳的。这类规范可以通过增强使其归纳。这模拟了归纳证明。要了解更多关于归纳不变式的信息，我们推荐读者观看 该视频。你也可以在 文档 中了解更多关于不变式的信息。

规则

CVL 中的规则描述了系统可能转移的属性。在智能合约中，可以通过调用函数来实现这些转移。因此，规则可以被视为围绕从被验证的智能合约调用的函数的“包装器”。该调用被“包装”在必须在函数调用前后保持的谓词中。规则必须描述：(1) 转换前的状态，(2) 转换，(3) 转换后的状态。描述状态意味着对可能状态集设置要求。描述转换意味着指定调用哪个函数以及输入满足哪些条件。

通过约束求解进行验证

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

布尔满足性

计算机科学中的一个经典问题是布尔满足性：给定一个关于逻辑变量的布尔（0，1）公式：v1, v2, ..., vk，是否存在使得该公式为真的逻辑变量值。例如，a && !a 在 a = true 和 a = false 时均为 false，因此它不可满足。n 变量上的满足性问题可以通过列举所有的 2^n 值组合来解决。随着 n 的增长，这变得迅速难以处理。更糟糕的是，计算机科学的一个著名理论结果表明，这一问题本质上是难以处理的：没有算法能比暴力枚举更有效地解决每一个实例。但实际上，绝大多数实际产生的问题实例是可以高效解决的，并且开发了一套广泛的工具生态系统——称为 SAT 求解器。现代最先进的 SAT 求解器通常能够在几秒钟内找到带有数千个变量的公式的解。

通过简化达到形式验证满足性

给定一个无循环程序及其关于的声明，可以利用布尔满足性（ SAT）验证该声明。例如，图 1 显示了一个小程序的控制流。为了确保程序结尾的声明成立，我们检查 SAT 查询：

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

请注意，该公式紧凑地定义了程序的 4 种路径。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 行的发送命令中，唯一调用的方法是 foo。这需要证明第 l2 和 l3 行对内存的写操作没有改变 mem[index] 的内容。这一般是一个不可判定的问题，一种推理这种情况的技术被称为指针分析。Certora Prover 实现指针分析，以强制执行编译器生成的内存访问模式上的不变式，以便在许多情况下解决该问题。

模块化

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

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

使用总结后，用户不仅在一个步骤中验证整个程序，而是将问题分解为两种子问题。首先，在程序的整个验证条件中，使用方法的总结，而不是使用方法的定义。其次，我们检查该方法的总结是否是实际方法定义的正确近似。在实践中，有时省略第二个检查，以便为规则编写者提供最大灵活性。

Certora Prover 架构

Certora Prover 实现了一个复杂的工具链，用于验证低级代码。当前支持 EVM 字节码、eBPF 和 WebAssembly。

图 3 描绘了 Certora Prover 的架构。去编译器将区块链特定字节码映射为关于称为“寄存器”的标量变量的指令。该表示被称为 TAC。类似的技术已在流行的 Soot 静态分析框架中实现。一个静态分析算法随后会推导出关于代码的可信不变式，从而极大简化验证任务。然后，VC（验证条件）生成器输出一组数学约束，描述程序可能违反的规则。最后，Certora Prover 调用现成的 SMT 求解器，自动搜索表示规则违反的数学约束的解。如前所述，这是一个不可判定的问题，这些求解器在某些情况下可以失败，超时并得到不明确的答案。Certora Prover 接收求解器的结果，将其处理生成详细的报告，并向 Prover 的客户/用户展示。

图 3：Certora Prover 架构。

相关工具和其他方法

智能合约的正确性受到了业界和学术界的广泛关注。以下是一些与 Certora 类似或正交的方法所使用的相关工具。

单元测试和模糊测试

智能合约的测试和模糊测试可以在如 Foundry、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 的目标是检查字节码的所有执行是否满足规范。Prover 通过分析字节码并将其与规范结合转化为一系列约束来实现这一目标。这些约束随后由一组底层 SMT 求解器解决。这些求解器要么报告所有执行是正确的，或者返回导致执行违反规范的特定输入。在这两种情况下，信息都会转换为高层格式并反馈给用户。

使用任何形式验证技术的主要挑战是复杂性。对于实际合约和规范，Prover 生成的约束对求解器来说可能非常具有挑战性。在这些情况下，用户可以通过对复杂代码段进行总结来降低证明的复杂性。通过良好的总结，每个证明部分都可以由求解器处理，而这些部分相加即构成原始规范的证明。

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