EIP-615: EVM 的子程序和静态跳转

简述

在 21 世纪，在一个流通着数十亿 ETH 的区块链上，形式化规范和验证是防止损失的重要工具。然而，EVM 的设计使得这变得不必要地困难。此外，EVM 的设计使得近线性时间编译到机器代码变得困难。我们建议推进解决这些问题的提案，以加强 EVM 的安全保障并减少性能障碍。

摘要

EVM 代码目前难以进行静态分析，这阻碍了用于防止我们的区块链所经历的许多代价高昂的错误的关键工具。此外，以太坊虚拟机的所有当前实现（包括编译器）的性能都不足以减少对预编译的需求，也无法满足网络的长期需求。本提案将动态跳转确定为造成这些问题的主要原因，并提出了对 EVM 规范的更改以解决该问题，从而使进一步努力实现更安全、更高性能的 EVM 成为可能。

我们还建议在将 EVM 合约放置到区块链上之前，以接近线性的时间验证 EVM 合约是否正确使用子程序，避免滥用堆栈，并满足其他安全条件。经过验证的代码可以避免大多数运行时异常以及对其进行测试的需要。良好控制的控制流和堆栈使用使解释器、编译器、形式分析和其他工具的工作更加轻松。

动机

目前，EVM 仅支持动态跳转，即跳转到的地址是堆栈上的参数。更糟糕的是，EVM 未能提供 Wasm 和大多数 CPU 提供的普通替代控制流工具，例如子程序和开关。因此，无法避免动态跳转，但它们模糊了代码的结构，从而在很大程度上抑制了控制流和数据流分析。这从根本上使优化编译的质量和速度相互矛盾。此外，由于许多跳转可能跳转到代码中的任何跳转目标，因此代码中可能路径的数量可能会随着跳转数量乘以目标数量的乘积而增加，静态分析的时间复杂度也会增加。许多这些情况在部署时是不可判定的，从而进一步抑制了静态和形式分析。

然而，鉴于以太坊的安全要求，接近线性的 n log n 时间复杂度至关重要。否则，可以精心设计或发现具有二次复杂度的合约，用作针对验证和优化的拒绝服务攻击向量。

但是，如果没有动态跳转，则可以在线性时间内静态分析代码。这允许_线性时间验证_。它还可以进行代码生成和此类优化，这些优化可以在 log n 时间内完成，从而构成 n log n时间编译器。

并且，如果没有动态跳转，并且有适当的子程序，EVM 成为从其他语言生成代码的更好目标，包括

• Solidity
• Vyper
• LLVM IR
  • 前端包括 C、C++、Common Lisp、D、Fortran、Haskell、Java、Javascript、Kotlin、Lua、Objective-C、Pony、Pure、Python、Ruby、Rust、Scala、Scheme 和 Swift

结果是，所有以下验证和优化都可以在部署时以接近线性的 (n log n) 时间复杂度完成。

• 可以验证是否存在大多数异常停止状态。
• 有时可以计算出资源的最大使用量。
• 字节码可以在接近线性的时间内编译为机器代码。
• 编译可以更有效地优化较小寄存器的使用。
• 编译可以更有效地优化 gas 计量注入。

规范

依赖项

EIP-1702. 通用账户版本控制方案。 该提案需要一个版本控制方案，以允许其字节码（以及最终的 eWasm 字节码）与同一区块链上现有的字节码一起部署。

提案

我们建议弃用两个现有指令——JUMP 和 JUMPI——并提出新指令来支持其合法用途。 特别是，必须仍然可以将 Solidity 和 Vyper 代码编译为 EVM 字节码，而不会显着降低性能或增加 gas 价格。

尤其重要的是与 eWasm 之间以及与机器代码之间的高效转换。为此，我们在 Wasm、x86、ARM 和提议的 EVM 指令之间保持紧密的对应关系。

预备知识

这些形式

INSTRUCTION

INSTRUCTION x

INSTRUCTION x, y

分别命名一个没有参数、一个参数和两个参数的 INSTRUCTION。指令在字节码中表示为单字节操作码。任何参数都以内联方式作为操作码后面的立即数据字节布局，解释为固定长度的、MSB 在先的、二进制补码的、双字节正整数。（负值保留用于扩展。）

分支和子程序

JUMP 和 JUMPI 的两个最重要的用途是静态跳转和返回跳转。有条件和无条件的静态跳转是控制流的主要内容。返回跳转实现为动态跳转到推送到堆栈上的返回地址。通过静态跳转和动态返回跳转的组合，您可以（并且 Solidity 确实）实现子程序。问题在于静态分析无法确定返回跳转将要到达的位置，因此它必须分析每种可能性（繁重的分析）。

静态跳转由以下提供

JUMPTO jump_target

JUMPIF jump_target

它们与 JUMP 和 JUMPI 相同，不同之处在于它们跳转到立即数 jump_target，而不是堆栈上的地址。

为了支持子程序，提供了 BEGINSUB、JUMPSUB 和 RETURNSUB。简要描述如下，完整语义如下。

BEGINSUB n_args, n_results

标记子程序的单个入口。 n_args 项在进入时从堆栈中取出，并在从子程序返回时将 n_results 项放置在堆栈上。子程序在下一个 BEGINSUB 指令（或下面的 BEGINDATA）或字节码结束时结束。

JUMPSUB jump_target

跳转到立即子程序地址。

RETURNSUB

从当前子程序返回到进入它的 JUMPSUB 之后的指令。

开关、回调和虚函数

动态跳转还用于 O(1) 间接：选择要跳转到的地址以推送到堆栈并跳转到该地址。因此，我们还建议使用另外两个指令来提供受约束的间接。我们使用内联存储的 JUMPDEST 或 BEGINSUB 偏移向量来支持这些指令，可以使用堆栈上的索引来选择这些偏移向量。这会将验证限制为所有可能目标的指定子集。避免了二次爆炸的危险，因为存储跳转向量所需的空间与编写最坏情况利用代码所需的空间一样多。

到 JUMPDEST 的动态跳转用于实现 O(1) 跳转表，这对于密集开关语句很有用。Wasm 和大多数 CPU 提供类似的指令。

JUMPV n, jump_targets

通过堆栈上的基于零的索引跳转到 n 个 JUMPDEST 偏移量向量中的一个。该向量以内联方式存储在 BEGINDATA 字节码之后的 jump_targets 偏移量处，作为 MSB 在前、二进制补码、双字节正整数。如果索引大于或等于 n - 1，则使用最后一个（默认）偏移量。

到 BEGINSUB 的动态跳转用于实现 O(1) 虚函数和回调，在大多数 CPU 上最多需要两次指针解引用。Wasm 提供类似的指令。

JUMPSUBV n, jump_targets

通过堆栈上的基于零的索引跳转到 n 个 BEGINSUB 偏移量向量中的一个。该向量以内联方式存储在 DATA 字节码之后的 jump_targets 偏移量处，作为 MSB 在前、二进制补码、双字节正整数。如果索引大于或等于 n - 1，则使用最后一个（默认）偏移量。

变量访问

这些操作提供对子程序中固定堆栈偏移量处的子程序参数和局部变量的便捷访问。否则，只能直接寻址十六个变量。

PUTLOCAL n

将堆栈弹出到局部变量 n。

GETLOCAL n

将局部变量 n 推送到堆栈上。

局部变量 n 是帧指针 FP[-n] 下的第 n 个堆栈项，如下定义。

数据

需要有一种方法将无法访问的数据放置到将被跳过且未经验证的字节码中。间接跳转向量将不是有效代码。初始化代码必须从可能不是有效代码的数据创建运行时代码。并且无法访问的数据可能会被程序用于其他目的。

BEGINDATA

指定到字节码结尾的所有后续字节都是数据，而不是可访问的代码。

结构

有效的 EIP-615 EVM 字节码以有效的标头开始。这是魔术数字“\0evm”，后跟语义版本控制编号“\1\5\0”。（对于 Wasm，标头为“\0asm\1”）。

标头之后是 main 例程的 BEGINSUB 操作码。它不带参数，也不返回值。其他子例程可以跟随 main 例程，并且可选的 BEGINDATA 操作码可以标记数据部分的开始。

语义

此处根据以下内容描述了跳转到子程序和从子程序返回：

• EVM 数据堆栈（如 Yellow Paper 中定义），通常简称为“堆栈”。
• JUMPSUB 和 JUMPSUBV 偏移的返回堆栈。
• 帧指针的帧堆栈。

我们将采用以下约定来描述机器状态：

• 程序计数器 PC（与往常一样）是当前正在执行的指令的字节偏移量。
• 堆栈指针 SP 对应于 Yellow Paper 的机器状态的子状态 s。   * SP[0] 是可以在堆栈上推送新项目的位置。   * SP[1] 是堆栈上的第一个项目，可以从堆栈中弹出。   * 堆栈向较低的地址增长。
• 帧指针 FP 在进入当前正在执行的子例程时设置为 SP + n_args。   * 帧指针和当前堆栈指针之间的堆栈项称为帧。   * 帧中当前的项目数 FP - SP 为帧大小。

注意：将帧指针定义为包含参数是非传统的，但更适合我们的堆栈语义，并简化了提案的其余部分。

帧指针和返回堆栈是子程序机制的内部结构，程序无法直接访问。这是必要的，以防止程序以可能无效的方式修改其自身的状态。

EVM 字节码的执行从没有参数的 main 例程开始，SP 和 FP 设置为 0，并且返回堆栈上有一个值—code_size - 1。（在此偏移量之后执行虚拟字节 0 会导致 EVM 停止。因此，执行没有先前的 JUMPSUB 或 JUMBSUBV 的 RETURNSUB（即在 main 例程中）会执行 STOP。）

子程序的执行从 JUMPSUB 或 JUMPSUBV 开始，它们

• 将 PC 推送到返回堆栈，
• 将 FP 推送到帧堆栈   * 因此，暂停当前子程序的执行，
• 将 FP 设置为 SP + n_args，以及
• 将 PC 设置为指定的 BEGINSUB 地址   * 因此，开始执行新的子程序。

在嵌套子程序的执行期间暂停子程序的执行，并在嵌套子程序执行完成后恢复，并在遇到 RETURNSUB 时结束，该函数

• 将 FP 设置为虚拟帧堆栈的顶部并弹出堆栈，
• 将 SP 设置为 FP + n_results，
• 将 PC 设置为返回堆栈的顶部并弹出堆栈，以及
• 将 PC 前进到下一条指令

因此，恢复封闭的子程序或 main 例程的执行。STOP 或 RETURN 也结束子程序的执行。

例如，从此堆栈开始，

_________________
      | 本地变量    20 <- FP
帧    |             21
______|___________  22
                       <- SP

并在推送两个参数并使用 JUMPSUB 分支到 BEGINSUB 2, 3 之后

PUSH 10
PUSH 11
JUMPSUB 开始处

并初始化三个局部变量

PUSH 99
PUSH 98
PUSH 97

堆栈看起来像这样

                    20
                    21
__________________  22
      | 参数      10 <- FP
帧    |___________  11
      | 本地变量    99
      |             98
______|___________  97
                       <- SP

经过一定量的计算后，堆栈可能看起来像这样

                    20
                    21
__________________  22
      | 返回值      44 <- FP
      |             43
帧    |___________  42
      | 本地变量    13
______|___________  14
                       <- SP

并且在 RETURNSUB 之后看起来像这样

_________________
      | 本地变量    20 <- FP
      |             21
帧    |___________  22
      | 返回值      44
      |             43
______|___________  42
                       <- SP

有效性

我们希望仅当程序的任何执行都不会导致异常停止状态时，才认为 EVM 代码有效，但是我们必须在线性时间内验证代码。因此，我们的验证不考虑代码的数据和计算，而仅考虑其控制流和堆栈使用。这意味着我们将拒绝具有无效代码路径的程序，即使这些路径不可访问。可以验证大多数条件，并且无需在运行时进行检查；例外情况是足够的 gas 和足够的堆栈。因此，静态分析可能会产生属于需要运行时检查的公认代码类的假阴性。除了这些情况，我们可以在验证时以线性复杂度验证大型类。

_执行_定义如 Yellow Paper 中所示 - EVM 状态中的一系列更改。有效代码的条件由状态更改来维护。在运行时，如果指令的执行违反了条件，则该执行处于异常停止状态。Yellow Paper 定义了五个这样的状态。

1 Gas 不足

2 超过 1024 个堆栈项

3 堆栈项不足

4 无效的跳转目标

5 无效的指令

我们建议扩展和扩展 Yellow Paper 条件，以处理我们提出的新指令。

为了处理返回堆栈，我们扩展了堆栈大小的条件：

2a 数据堆栈的大小不超过 1024。

2b 返回堆栈的大小不超过 1024。

鉴于我们对数据堆栈的更详细描述，我们将条件 3（堆栈下溢）重新声明为

3 SP 必须小于或等于 FP

由于各种 DUP 和 SWAP 操作（以及 PUTLOCAL 和 GETLOCAL）定义为从堆栈中取出项并将其放回，因此这可以防止它们访问帧指针下方的数据，因为从堆栈中取出太多项意味着 SP 小于 FP。

为了处理新的跳转指令和子例程边界，我们扩展了跳转和跳转目标的条件。

4a JUMPTO、JUMPIF 和 JUMPV 仅寻址 JUMPDEST 指令。

4b JUMPSUB 和 JUMPSUBV 仅寻址 BEGINSUB 指令。

4c JUMP 指令不寻址它们发生的子例程之外的指令。

我们有两个新的执行条件，以确保子例程对堆栈的一致使用：

6 对于 JUMPSUB 和 JUMPSUBV，帧大小至少是跳转到的 BEGINSUB 的 n_args。

7 对于 RETURNSUB，帧大小等于封闭 BEGINSUB 的 n_results。

最后，我们有一个可以防止堆栈病态使用的条件：

8 对于代码中的每个指令，帧大小是恒定的。

实际上，我们必须在运行时测试条件 1 和 2 - 足够的 gas 和足够的堆栈。我们不知道有多少 gas，我们不知道递归可能有多深，即使对于非递归程序，堆栈深度的分析也不是微不足道的。

我们静态验证所有其余条件。

成本和代码

所有指令都是 O(1)，只有一个小常数，每个指令只需要几个机器操作，而 JUMP 或 JUMPI 通常在每次跳转之前都会对 JUMPDEST 偏移数组执行 O(log n) 二分搜索。由于 JUMPI 的成本_高_，而 JUMP 的成本_中等_，我们建议 JUMPV 和 JUMPSUBV 的成本应为_中等_，JUMPSUB 和 JUMPIF 应为 低，而 JUMPTO 和其余指令应为_非常低_。测量会告诉我们。

我们建议使用以下操作码：

0xb0 JUMPTO
0xb1 JUMPIF
0xb2 JUMPV
0xb3 JUMPSUB
0xb4 JUMPSUBV
0xb5 BEGINSUB
0xb6 BEGINDATA
0xb7 RETURNSUB
0xb8 PUTLOCAL
0xb9 GETLOCAL

向后兼容性

这些更改需要在适当的间隔分阶段实施：

1. 如果接受此 EIP，则应弃用无效代码。工具应停止生成无效代码，用户应停止编写无效代码，客户端应警告有关加载无效代码。

2. 稍后的硬分叉将要求客户端仅将有效代码放置在区块链上。请注意，尽管发生了分叉，但旧的 EVM 代码仍然需要无限期地支持；较旧的合约将继续运行，并创建新的合约。

如果需要，可以通过继续接受未版本化为新的代码（但没有验证）来无限期地延长弃用期。也就是说，通过延迟或取消第 2 阶段。

无论如何，我们需要一个像 EIP-1702 这样的版本控制方案，以允许当前代码和 EIP-615 代码在同一区块链上共存。

原理

此设计受到现有 EVM 语义、eWasm 兼容性要求和以太坊环境安全需求的严格限制。它还受到了第一作者先前实现 Java 和 Scheme 解释器的工作的影响。因此，几乎没有替代设计空间。

如上所述，该方法只是弃用有问题的动态跳转，然后询问提供他们支持的功能需要哪些操作码。这些需要包括 eWasm 提供的那些，而 eWasm 本身是根据典型的硬件建模的。唯一真正的创新是将帧指针和返回指针移动到它们自己的堆栈，以防止任何覆盖它们的可能性。（尽管 Forth 也使用返回堆栈。）这允许将子程序参数视为局部变量，并有助于返回多个值。

实施

实施此提案并不困难。至少，可以简单地用新的操作码扩展解释器，否则保持不变地运行。新的操作码只需要帧指针和返回偏移的堆栈以及上面描述的几个推送、弹出和赋值。大部分工作是验证器，在大多数语言中几乎可以从上面的伪代码中转录。

在 Greg Colvin 的 Aleth 分支 中提供了一个经过轻量测试的 C++ 参考实现。此版本需要大约 110 行新的解释器代码和一个注释完善的 178 行验证器。

附录 A

验证

验证包括两项任务：

• 检查跳转目标是否正确且指令有效。
• 检查子例程是否满足有关控制流和堆栈使用的条件。

我们在下面的伪 C 中概述了这两个验证函数。为了简化演示，仅处理了五个原函数（JUMPV 和 JUMPSUBV 只会增加循环遍历其向量的复杂性），我们假设辅助函数用于从直接数据中提取指令参数并管理堆栈指针和程序计数器，并且放弃了一些优化。

验证跳转

验证跳转是否到有效地址需要对字节码进行两次顺序传递——一次用于构建跳转目标和子例程入口点的集合，另一次用于检查跳转到的地址是否在适当的集合中。

    bytecode[code_size]   // 包含要验证的 EVM 字节码
    is_sub[code_size]     // PC 处是否存在 BEGINSUB？
    is_dest[code_size]    // PC 处是否存在 JUMPDEST？
    sub_for_pc[code_size] // PC 在哪个 BEGINSUB 中？

    bool validate_jumps(PC)
    {
        current_sub = PC

        // 构建 BEGINSUB 和 JUMPDEST 的集合
        for (PC = 0; instruction = bytecode[PC]; PC = advance_pc(PC))
        {
            if instruction 无效
                return false
            if instruction 是 BEGINDATA
                break;
            if instruction 是 BEGINSUB
                is_sub[PC] = true
                current_sub = PC
                sub_for_pc[PC] = current_sub
            if instruction 是 JUMPDEST
                is_dest[PC] = true
            sub_for_pc[PC] = current_sub
        }

        // 检查目标是否在子例程中
        for (PC = 0; instruction = bytecode[PC]; PC = advance_pc(PC))
        {
            if instruction 是 BEGINDATA
                break;
            if instruction 是 BEGINSUB
                current_sub = PC
            if instruction 是 JUMPSUB
                if is_sub[jump_target(PC)] 是 false
                    return false
            if instruction 是 JUMPTO or JUMPIF
                if is_dest[jump_target(PC)] 是 false
                    return false
            if sub_for_pc[PC] 不是 current_sub
                return false
       }
       return true
    }

请注意，EVM 已经在运行此类代码来检查动态跳转，包括每次运行合约时构建跳转目标集，并在每次跳转之前在跳转目标集中执行查找。

子程序验证

基本方法是调用 validate_subroutine(i, 0, 0)，对于 i 等于 EVM 代码中从每个 BEGINDATA 偏移开始的第一个指令。validate_subroutine() 依次遍历指令，在遇到 JUMP 和 JUMPI 指令时进行递归。当达到之前访问过的目标时，它会返回，从而中断循环。如果子例程有效，则返回 true，否则返回 false。

    bytecode[code_size]     // 包含要验证的 EVM 字节码
    frame_size[code_size ]  // 用 -1 填充

    // 我们单独验证每个子例程，就像在顶层一样
    // * PC 是代码中开始验证的偏移量
    // * return_pc 是 RETURNSUB 返回到的返回堆栈上的顶部 PC
    // * 在顶层，FP = SP = 0 既是帧大小又是堆栈大小
    // * 当项目被推送时，SP 会变得更负，因此堆栈大小为 -SP
    validate_subroutine(PC, return_pc, SP)
    {
        // 依次遍历代码，对跳转进行递归
        while true
        {
            instruction = bytecode[PC]

            // 如果设置了帧大小，我们之前来过这里
            if frame_size[PC] >= 0
            {
                // 检查恒定的帧大小
                if instruction 是 JUMPDEST
                    if -SP != frame_size[PC]
                        return false

                // 返回以中断循环
                return true
            }
            frame_size[PC] = -SP

            // 指令对堆栈的影响
            n_removed = removed_items(instructions)
            n_added = added_items(instruction)

            // 检查堆栈下溢
            if -SP < n_removed
                return false

            // 删除和添加堆栈项的净效应
            SP += n_removed
            SP -= n_added

            // 检查堆栈溢出
            if -SP > 1024
                return false

            if instruction 是 STOP、RETURN 或 SUICIDE
                return true

            // 违反了单个入口
            if instruction 是 BEGINSUB
                 return false

            // 返回到顶部或从递归到 JUMPSUB
            if instruction 是 RETURNSUB
                return true;;

            if instruction 是 JUMPSUB
            {
                // 检查是否有足够的参数
                sub_pc = jump_target(PC)
                if -SP < n_args(sub_pc)
                    return false
                return true
            }

            // 将 PC 重置为跳转目的地
            if instruction 是 JUMPTO
            {
                PC = jump_target(PC)
                continue
            }

            // 递归跳转到代码进行验证
            if instruction 是 JUMPIF
            {
                if not validate_subroutine(jump_target(PC), return_pc, SP)
                    return false
            }

            // 根据指令前进 PC
            PC = advance_pc(PC)
        }

        // 检查结果的正确数量
        if (-SP != n_results(return_pc)
            return false
        return true
    }

附录 B

EVM 分析

存在一个庞大且不断增长的研究人员、作者、教师、审计师和分析工具生态系统，它们提供的软件和服务专注于 EVM 代码的正确性和安全性。下面给出一个小样本。

一些工具

• 合约库
• EthereumJ
• Exthereum
• Harmony
• JEB
• Mythril
• Securify
• Skale
• Status

一些论文

• 以太坊VM字节码的形式验证工具
• EVM的Lem形式化和一些Isabelle/HOL证明
• 以太坊智能合约攻击调查
• 为交互式定理证明器定义以太坊虚拟机
• 以太坊 2.0 规范
• 智能合约的形式验证
• JelloPaper：EVM在K中可读的语义
• KEVM：以太坊虚拟机的完整语义。
• 使智能合约更智能
• Securify：智能合约的实用安全分析
• 雷霆协议
• 在Isabelle/HOL中验证以太坊智能合约字节码 *EVM 1.5的Lem形式化

版权

通过 CC0 放弃版权和相关权利。

Citation

Please cite this document as:

Greg Colvin <greg@colvin.org>, Brooklyn Zelenka (@expede), Paweł Bylica (@chfast), Christian Reitwiessner (@chriseth), "EIP-615: EVM 的子程序和静态跳转 [DRAFT]," Ethereum Improvement Proposals, no. 615, December 2016. [Online serial]. Available: https://eips.ethereum.org/EIPS/eip-615.