Certora技术白皮书

Certora 工具套件

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

工具套件的核心是 Certora Prover，一个验证工具，它接收低级合约字节码（例如，EVM 字节码程序、一个 Solana eBPF 对象 或 Stellar WASM 对象），以及用 CVL (Certora Verification Language) 或 CVLR (Certora Verification Language for Rust) 编写的规范。该证明工具将代码和规范一起分析，以识别代码与规范偏离的情形。该技术自动定位即使是最优秀的审计员也可能错过的关键漏洞，并通过证明某些关键属性得到满足来增强代码安全性的信心。

开发者和安全研究人员均可通过使用 Certora Prover 获益。对于开发者而言，Prover 提供的保证优于测试或模糊测试，并且其设置所需的样板代码和附加构造更少。研究人员也可以利用 Prover 绘制攻击路径并选择重点努力的方向。

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

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

• Gambit，用于通过变异和虚无检测确保规范的质量
• Safeguard，用于监控以太坊节点中的不变式
• Quorum, 用于捕捉治理提案有效负载中的错误。

验证与审计

由于智能合约中的漏洞可能使合约创建者和其用户面临巨大的损失，合约开发者渴望在其合约部署之前消除漏洞。许多安全公司提供基于手动审计的服务，既有通过自身专家执行审计，也有通过漏洞赏金计划外包邮件进行审计。

手动审计虽然重要，但存在严重限制。Certora 的工具套件在许多方面补充了这些限制：

(1) 自动重新检查。每次代码更改时，都会需要新的审计，这需要雇佣相同的外部审计团队。提前安排定期审计可能是一项重大的操作挑战；因此，同一项目的不同版本可能会最终有不同的审计员，这样项目代码库/问题的历史背景可能会丢失。相比之下，Certora 的方法使开发者能够在开发过程中早期指定关键属性，这些属性可以在代码更改时自动重新检查—— 一次指定，频繁验证！

(2) 协作编码。审计通常由外部安全人员执行，他们具有丰富的一般经验，但可能缺乏对特定合约的深入了解。Certora 的基于属性的方法使开发者和审计员能够 一起 制定编码合约安全相关方面的属性，从而允许检测到更特定于应用程序和更深层的逻辑缺陷。

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

(4) 随时可用性。最佳审计员通常要预定数月。由于陡峭的学习曲线、结构化上手资源/项目缺乏、以及对审计员的高期望，以太坊在可预见的未来可能继续面临代码安全专业人员的严重短缺。由于 Certora 的方法利用自动验证技术来减少所需的重复劳动，因此其服务更容易获得，开发者/专家可以在其代码上指定属性。

(5) 向左转移。不幸的是，Web3 中的安全软件开发生命周期被简化为 3 步“构建-审计-发布”的线性时间表，在审计阶段面临巨大的不切实际的期望，这是一种不可持续的发展趋势。通过开发者/专家使用 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 值。

有关更多详情，请参阅 验证报告 和 规范。

转账操控攻击

这些漏洞出现在系统容易受到捐赠攻击时，例如首次存款者攻击。在这种情况下，系统错误地计算外部转移的资产，或假设捐赠存款会很小。这可能会被利用，导致协议意外的资产损失。

为防止此类攻击的一些关键属性是：

• 微小金额利好资金方 – 用户不应该能够通过一次操作（例如，在单个事务中存款和提取）获利。
• 用户资产保护 – 当另一个用户在没有授权的情况下执行操作时，用户的总资产不应该发生变化。

通过执行这些属性，Certora Prover 确保协议对金融操控和意外资产重新分配保持抵抗力。

在 SushiSwap Trident 中，Certora Prover 发现了一个关键漏洞，该漏洞可用于通过转移基础代币来消耗协议资金。有关更多细节，请查看我们的 博客。

质押奖励错误计算

基于权益证明的系统定期分配奖励，通过 block.timestamp - lastTimestamp 计算奖励。如果 lastTimestamp 在合约创建时或在奖励分配开始时未正确初始化为 block.timestamp，则此计算将导致 block.timestamp - 0，导致过大的时间差。结果，系统可能会分配出远超预期的奖励。

在 Aave 的 StakeToken 中，我们证明了奖励申领的完整性。你可以在我们的 博客中阅读有关开止奖励的重大错误及该规则防止这种错误的内容。

主要特性

1. 完全自动化验证

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

2. 例子生成场景

仅仅知道智能合约未满足某个属性对于用户理解合约可能存在的漏洞是远远不够的。因此，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 规范的机制。我们建议读者查阅 参考手册，该手册包含完整细节。

归纳不变式

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

归纳不变式是被任意执行保持的 invariants。一个归纳不变式必须在转移系统的所有初始状态下保持成立。此外，当在满足不变式的任意状态 s 中执行转移并给出步骤至状态 s' 时，必须在 s' 上保证不变式成立。归纳不变式可以保证程序是正确的，而不顾执行的指令数量。对归纳的反例是一个从满足不变式的状态转移到违反不变式的错误状态。

与上面描述的常规反例不同，归纳的反例 并不 一定表明程序存在漏洞，因为它可能反映出该程序到达的状态是不可能的；它只可能表明该规范不是归纳式的。通过 强化 使其成为归纳式的。这模仿了归纳证明。要了解更多关于归纳不变式的信息，我们向读者推荐 这个视频。关于 CVL 中不变式的更多信息，可以参阅 文档。

规则

CVL 中的 规则 描述了系统可能转移的属性。在智能合约中，这种状态转移可通过调用函数来实现。因此，规则可以被视为从被验证的智能合约中调用函数的“包装器”。该调用由必须在函数调用之前和之后成立的谓词“包装”。规则必须描述：（1）转移之前的状态；（2）转移；（3）转移之后的状态。描述状态意味着对可能状态的集合设定要求。描述转移意味着指定调用的函数及输入满足的条件。

通过约束求解进行验证

Certora Prover 比较字节码的行为和规范以查找漏洞并形式证明其缺失。直观上，这一想法是将 EVM 的语义和规范建模为一种称为 SMT（Satisfiability Modulo Theories）的逻辑公式。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 行的 send 命令中唯一调用的方法是 foo。这需要证明第 l2 和 l3 行的内存写入未更改 mem[index] 的内容。这通常是一个不可判定的问题，处理这个问题的方法称为 指针分析。Certora Prover 实现了指针分析，在许多情况下强制执行编译器生成的内存访问模式上的不变式，以解决该问题。

模块化

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

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

通过摘要，用户可以在一次通过中验证整个程序，而是将问题分解为两种类型的子问题。第一，在程序的整体验证条件中，使用的是方法的摘要，而不是方法的定义。其次，我们检查该方法的摘要是否是实际方法定义的正确近似。在实践中，有时省略第二次检查，以给规则创建者提供最大的灵活性。

Certora Prover 架构

Certora Prover 实现了一条复杂的工具链，用于验证低级代码。它目前支持 EVM 字节码、eBPF 和 Web Assembly。

图 3 显示了 Certora Prover 的架构。反汇编器将区块链特定字节码映射到称为 “寄存器” 的标量变量指令中。这种表示称为 TAC。类似的方法已经在流行的 Soot 静态分析框架中实现。静态分析算法随后推断出关于代码的合理不变式，从而大幅简化验证任务。然后，VC（验证条件）生成器输出一组数学约束，这些约束描述程序可能违反规则的条件。最后，Certora Prover 调用现成的 SMT 求解器，自动搜索表示规则违反的数学约束的解决方案。如前所述，这是一个不可判定的问题，这些求解器在某些情况下可能会因为超时而失败，导致无法得出结论。Certora 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 支持推理关于 所有 执行以太坊字节码程序。该证明器以字节码程序以及用 CVL 编写的规范作为输入。证明器的目标是检查字节码的所有执行是否满足规范。证明器通过分析字节码并将其与规范一起转换为约束体系来实现这一点。这些约束随后由一套底层 SMT 求解器解决。这些求解器要么报告所有执行均正确，否 则返回一个特定输入，该输入导致违反规范的执行。在这两种情况下，信息都被翻译成高层格式并展示给用户。

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

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