利用形式化验证查找编译器 Bug

编译器最重要的属性——也是你每次编译代码时所依赖的属性——就是“语义保留”。这是一种花哨的说法，意思是编译器会保留程序的含义。从编译器输出的已编译程序（在底层字节码或机器代码中）应该完全按照输入程序的方式执行。

当考虑编译器在编译期间可能执行的各种优化时，也存在类似的属性。编译器可以自由地重新排序赋值、更改循环结构等，只要程序的整体行为不改变（并且理想情况下程序最终运行得更快）。

编译器错误尤其有害，因为它们会悄悄地破坏这个重要的属性。从编译器输出的程序可能 几乎 是正确的，但行为已经以微妙的方式改变了。我们已经记录了 web3 生态系统中的编译器出现错误的许多方式 编译器。我们最近发现的一个 bug 是在一个优化pass中：在试图保存一些位操作时，LLVM 优化器（不那么巧妙地）改变了输入程序。

如果我们想降低优化器 bug 的影响，一个简单的方法就是简单地禁用所有优化。然而，随着 web3 生态系统变得越来越复杂和成熟，这种方法变得越来越不可行。以 gas 形式存在的计量执行为高效代码提供了真正的经济激励，而且 EVM 上的代码大小限制正成为许多开发者的约束。我们显然希望获得优化的好处，同时降低可能潜入的不可避免的 bug 的影响。

虽然形式化验证的编译器 确实存在，但 web3 生态系统目前还没有这样的编译器，构建和验证这样的编译器将需要多年的努力。然而，我们仍然可以使用形式化验证来确保优化不会改变我们的程序。

等价性检查

一开始，我们说过编译器必须保留原始程序的含义。在考虑优化时也是如此：启用优化后编译器生成的程序应该与禁用优化时的行为完全相同。

如果我们有一个比较两个程序并指示它们是否 等价 的工具，那么我们就可以 验证 编译器优化。如果优化前后的程序具有相同的行为，那么根据定义，优化不会改变程序行为。

我们一直在研究这样一个等价性检查器。给定两个程序，我们的检查器使用现有的 Certora Prover 基础设施来证明程序在所有输入上都是等价的，这意味着程序产生相同的结果，同时具有相同的可观察的副作用。

这个等价性检查器有许多潜在的应用，但我们特别兴奋的一个是编译器优化验证。虽然我们的解决方案仍然处于开发阶段，还没有超过原型阶段，但我们已经用它来发现 Vyper 编译器中的一个优化 bug。

Bug

在继续之前，我们要强调以下几点：

1. 我们发现的 bug 在实验性的 Venom 优化管道中。
2. 触发此优化问题的代码在部署到链上时 没有 使用此优化设置。
3. 该 bug 已经由 Vyper 开发者修复。

让我们首先看看有问题的代码，它取自 Vyper 编译器的测试用例，并且来自 Curve Finance 代码库：

虽然我们省略了许多底层的数学细节，但这个函数使用牛顿逼近法计算一个方程的近似解。在循环的每次迭代中，y 的近似值使用导数进行细化，然后计算近似值的绝对变化 (diff)。如果近似值的变化足够小，函数将返回近似值 y。

当我们把等价性检查器应用到这个函数时，它标记了一个输入，在这个输入中，这个函数的非优化版本会遍历循环体，然后跳回到循环的顶部，而优化版本会在同一个输入上返回 y。等价性检查器如何找到这个输入的细节超出了本文的范围。为了给出一个粗略的分解：等价性检查器在有和没有优化的情况下编译这段代码，检测生成的字节码以记录循环是否退出/后跳/恢复，用相同的输入调用每个版本的代码，然后最终断言循环执行了相同的操作（后跳、退出等）。

重申一下，这个推理是在现有的 Certora Prover 中完成的，因此完全是符号化的：当考虑函数和循环行为时，我们正在推理函数 newton_y 的所有可能的输入和循环的所有可能的行为。

在等价性检查器标记了不同的行为之后，我们手动检查了这段代码的优化和非优化版本。Venom 优化管道执行的一个主要更改是将局部变量从 EVM 内存中的位置移动到 EVM 堆栈。为了说明这个变化，让我们首先看看 if y > y_prev 检查的未优化版本：

R942 = tacM[0x1a0]

R943 = tacM[0x120]

B944 = R943 > R942

if B944 goto 13008_1019_0_0_0_0 else goto 12978_1019_0_0_0_0

这段代码以 Certora Prover 使用的 TAC 中间表示形式呈现。以 R 和 B 开头的变量表示堆栈上的值。 tacM[0x1a0] 表示我们从偏移量为 0x1a0 的 EVM 内存中读取，0x120 同理。然后，这段代码比较这两个值，根据结果跳转到代码中的两个不同位置。内存中的位置 0x1a0 对应于局部变量 y_prev，0x120 保存 y。现在让我们看看如果条件为真，即 y > y_prev，我们跳转到的代码：

R952 = tacM[0x120]

R953 = tacM[0x1a0]

R954 = R952 - R953

tacM[0x300:0x300+32] = R954

在这里我们可以看到 y_prev（也就是 0x1a0 中的值）从 y（0x120 中的值）中减去，然后存储到 0x300 的槽中，你可能已经正确地猜到它对应于变量 diff。else 分支（当 y_prev >= y 时）是相似的。

现在让我们看看优化版本中相同代码的反编译，其中局部变量已经从内存中的位置移动到堆栈变量。这是 应该 对应于 y > y_prev 的相同的条件检查。

B879 = R874 > R874

if B879 goto 11178_1009_0_0_0_0 else goto 11032_1009_0_0_0_0

这里有两件事要注意：首先，我们不再看到任何内存访问，因为局部变量确实已经移动到堆栈中。然而，我们正在将相同的堆栈变量与自身进行比较！我们在这里计算的条件必然是假的，所以让我们看看条件的 else 分支，以更清楚地了解发生了什么：

R893 = R874 - R874

R893 意味着保存 diff 的值，diff 应该等于 y_prev - y，但我们反而从自身中减去了相同的值。换句话说，diff 总是 0。然而，如果 diff 总是 0，那么检查 diff < max(convergence_limit, y // 10**14) 总是真的，因此循环将 总是 在第一次迭代中 返回。正是这种不同的行为——一个版本的循环返回，而另一个版本的循环继续——是等价性检查器检测到的。

Venom 优化器中潜在的 bug 与局部变量如何映射到堆栈位置有关。在这里，y 和 y_prev 已经被混淆为存在于相同的堆栈位置，给出了不正确的结果。当我们联系 Vyper 开发者并告知我们的发现时，他们确认了这个 bug 的有效性，并且它已经在 Vyper 0.4.2 中修复。

结论

虽然这个优化 bug 已经被修复，但我们的发现证明了我们的等价性检查器在验证编译器优化方面的效用。正如我们之前提到的，它仍然处于积极的开发中，但我们将分享更新，因为它变得更加健壮并准备好用于黄金时段。

与此同时，我们不想阻止任何人使用编译器优化，但与软件开发堆栈的每个部分一样，值得不要想当然，并进行严格的测试，以验证你的编译器没有对你的代码引入细微的更改。

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