反编译Vyper程序以进行形式验证

Vyper 编程语言提供了一个干净的内存和控制抽象。与 Solidity 相比，它被认为对 DeFi 编程非常有吸引力。不幸的是，Vyper 程序仍然包含关键的逻辑错误。上个月，一个 Vyper 编译器错误导致了 7000 万美元的损失。

我们描述了 Certora 验证工具包，以防止 Vyper 程序中的数十亿美元逻辑错误，这些错误本可以防止上个月的攻击。通过使用该工具包，用户可以表达高层的期望属性以描述 Vyper 智能合约。计算机随后分析合约的可执行版本，以寻找会违反这些属性的输入行为，甚至数学上证明其不存在。其主要思想是自动从字节码中恢复低级内存结构，然后将反汇编代码的精确语义编码为数学约束系统。然后，我们利用现有的求解器构造一个解决方案，以解决指示代码中的错误或证明约束不可行的数学约束。这意味着该程序可以保证满足要求。

我们展示了该工具在识别错误和证明现实代码方面的应用。

Certora 验证管道回顾

Certora 验证管道在 我们的白皮书 中已被讨论。对于这篇博客，我们为 Vyper 用户提供了一个总结。下图展示了 Certora Prover 中涉及的阶段。

1. 源程序使用 Vyper 编译器编译成 EVM (以太坊虚拟机) 可执行文件。
2. 用户在 CVL (Certora 验证语言) 规范中描述期望的属性。
3. EVM 被反编译成一种称为 TAC (三地址码) 的中间语言。
4. TAC 程序被编译成 SMT2 逻辑公式。
5. 要么 SMT 求解器在代码中找到错误，要么保证规则成立。

理解 Vyper 字节码的挑战

尽管 Vyper 和 Solidity 编译器都生成 EVM 字节码，但其输出可能非常不同。特别是，Vyper 编译器会在内存中广泛地复制值。最终，当 Certora Prover 将 EVM 字节码程序转化为逻辑公式时，内存使用了一个称为 “数组理论” 的技术建模，这在包括时 notoriously 昂贵。在这种情况下，Vyper 对内存的广泛使用对 Vyper 智能合约的形式验证带来了显著的可扩展性挑战。

为了应对这些可扩展性问题，Certora 的研发团队扩展了现有的专有 内存分析，以处理由 Vyper 编译器生成的用例。该分析可以恢复一些关于 EVM 字节码程序内存布局的高层细节，并证明用于优化我们应用数组理论的 不变式，从而提高我们的自动化验证的可扩展性。

一个真实世界的例子

我们希望验证用 Vyper 编写的 sort 函数的有效性。此代码取自 curve-crypto-contract 仓库 的 CurveFi。

首先，我们添加一个外部函数以便访问该代码进行验证。这是必要的，因为 Certora Prover 通过模拟来自未知发送方的任意消息与智能合约进行交互。添加此函数是至关重要的，因为内部函数不属于合约的公共 ABI，它们不能直接被我们的 prover 访问。

以下 CVL 规则检查 sort 函数是否按降序返回元素。

然而，这仅仅是我们关心的许多属性之一。我们还想知道 sort 函数是否返回与提供给该函数的相同元素。为了避免推理关于排列，下方规则使用一个自由变量并声明这两个多项式相等，这意味着 a0, a1, a2 和 b0, b1, b2 是彼此的排列。

注意

最后的等式使用全无界整数算术，因为所有数字都转换为 mathint。

状态和当前限制

当前 Vyper 语言的支持处于预 Alpha 级别。语言的大部分特性都得到了支持。许多非平凡的程序属性可以得到证明，包括：

• 包含所有基本语言语法的属性
• 确保内存和存储中复杂数据结构的属性
• 需要推理多个合约交互的属性

当前的进行工作包括但不限于（无特定顺序）：

• 目前仅支持 Vyper 0.3.7 和 0.3.9
• 对存储中动态数组的第一类支持
• 某些 CVL 的高级特性（特别是，ghost 状态和 hooks）尚不支持
• 多种待处理的内部分析改进正在进行中
• 继续优化我们 Vyper 分析的性能

相关工具

形式验证是计算机科学的一个成熟领域，拥有出色的技术和开源软件。 Viper 验证结构 也支持 Vyper 合约的形式验证。Certora Prover 通过以下方式实现更可扩展的验证：

1. 对字节码进行静态程序分析，减少约束求解的固有复杂性。
2. 使模块化规范可选，减少验证代码时所需的人工劳动量。
3. 我们部署、划分和征服多个 SMT 求解器，以扩大形式验证到更大程序的规模。

此外，Certora Prover 也能够保护免受编译器错误的影响。

acknowledgments（致谢）

我们要感谢 Benjamin Greenwald，他为在 Certora prover 中增加对 Vyper 的支持而努力。

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