⚠️ Review Standards Track: Core

EIP-5450: EOF - 栈验证

EOF 函数的部署时栈使用验证。

Authors	Andrei Maiboroda (@gumb0), Paweł Bylica (@chfast), Alex Beregszaszi (@axic), Danno Ferrin (@shemnon)
Created	2022-08-12
Requires	EIP-3540, EIP-3670, EIP-4200, EIP-4750

摘要

引入 EOF 代码段的扩展验证，以保证在已验证合约的执行期间既不会发生栈下溢也不会发生栈溢出。

动机

当前的 EVM 对每个执行的指令执行许多有效性检查，例如检查指令是否已定义、栈溢出和下溢以及剩余的 gas 量是否足够。

此 EIP 通过验证是否不会发生任何异常情况，并阻止任何无效代码的执行和部署，从而最大限度地减少了运行时所需的此类检查的数量。

操作数栈验证具有以下几个优点：

• 移除所有指令的运行时栈下溢检查，
• 移除除了 CALLF 和 JUMPF（JUMPF 在单独的 EIP 中引入）之外的所有指令的运行时栈溢出检查，
• 确保执行以其中一个终止指令结束，
• 阻止部署具有无法访问指令的代码，从而阻止将代码段用于数据存储。

它也有一些缺点：

• 增加了对代码结构的约束（类似于 JVM、CPython 字节码、WebAssembly、SPIR-V 等）；但是，如果这些约束被证明对用户不友好，则可以以向后兼容的方式解除这些约束，
• 自然地，将栈验证实现为第二个验证阶段；但是，这不是严格要求的，并且验证的计算和空间复杂度在任何实现变体中都保持线性。

这些验证规则创建的保证还提高了 EVM 代码的 AOT (Ahead-Of-Time) 和 JIT (Just-In-Time) 编译的可行性。单次通过的转译可以安全地执行代码验证，并且可以应用高级栈/寄存器处理与栈高度验证。虽然对于主要受存储状态大小限制的 Mainnet 验证器节点影响不大，但这些可以显着加快见证验证和其他非 Mainnet 用例。

规范

代码验证

备注: 我们依赖于 EIP-4750 定义的操作数栈和类型段的概念。

每个代码段都独立验证。

指令验证

在 EIP-3670 中定义的第一个验证阶段（以及由 EIP-4200 和 EIP-4750 扩展）中，独立检查指令以检查其操作码和立即数是否有效。

操作数栈验证

在第二个验证阶段，对代码执行控制流分析。

此处的操作数栈高度是指此函数可以访问的栈值的数量，即它不考虑调用者函数帧的值（但包括此函数的输入）。请注意，验证过程不需要实际的操作数栈实现，而只需要跟踪其高度。

终止指令是指以下指令之一：

• 结束函数执行：RETF、JUMPF，或
• 结束调用帧执行：STOP、RETURN、RETURNCODE、REVERT、INVALID。

注意：JUMPF 和 RETURNCODE 在单独的 EIP 中引入。

向前跳转是指相对偏移量大于或等于 0 的任何 RJUMP/RJUMPI/RJUMPV 指令。向后跳转是指相对偏移量小于 0 的任何 RJUMP/RJUMPI/RJUMPV 指令，包括跳转到同一跳转指令。

代码中的指令在代码上的单个线性过程中扫描。 对于每个指令，操作数栈高度边界被记录为 stack_height_min 和 stack_height_max。

第一个指令的记录栈高度边界被初始化为等于与代码匹配的函数类型的输入数量（stack_height_min = stack_height_max = type[code_section_index].inputs）。

对于每个指令：

1. 检查此指令是否具有记录的栈高度边界。 如果没有，则表示它既没有被之前的向前跳转引用，也不是顺序指令流的一部分，并且此代码验证失败。
   • 这是验证算法的先决条件，并且代码生成器需要以一种方式对代码基本块进行排序，即没有块仅被向后跳转引用。 任何程序都可以通过按反向后序对代码基本块进行排序来满足此要求。
2. 确定指令对操作数栈的影响：
   1. 检查记录的栈高度边界是否满足指令要求。 具体来说：
      • 对于 CALLF 指令，根据类型段中定义的类型，记录的栈高度下限必须至少是被调用函数的输入数量，
      • 对于 RETF 指令，记录的下限和上限都必须相等，并且必须完全是与代码匹配的函数的输出数量，
      • 对于 JUMPF 到返回函数，记录的下限和上限必须完全等于 type[current_section_index].outputs + type[target_section_index].inputs - type[target_section_index].outputs，
      • 对于 JUMPF 到非返回函数，根据类型段中定义的类型，记录的栈高度下限必须至少是目标函数的输入数量，
      • 对于任何其他指令，记录的栈高度下限必须至少是指令所需的输入数量，
      • 除了 RETF 和 JUMPF 之外，没有对终止指令进行额外的检查，这意味着允许最后留在栈上的项目在结束 EVM 执行的指令上存在。
   2. 对于 CALLF 和 JUMPF 检查可能的栈溢出：如果记录的栈高度上限大于 1024 - types[target_section_index].max_stack_increase，则验证失败。
   3. 计算指令执行后的新栈高度边界。 上限和下限更新相同的值：
      • 在 CALLF 之后，栈高度边界通过加上 types[target_section_index].outputs - types[target_section_index].inputs 来调整，
      • 在任何其他非终止指令之后，栈高度边界通过减去指令输入数量并加上指令输出数量来调整，
      • 终止指令不需要更新栈高度边界。
3. 确定可以跟随当前指令的后继指令列表：
   1. 如果当前指令既不是终止指令也不是无条件跳转（RJUMP），则为下一个指令。
   2. 如果当前指令是有条件（RJUMPI 或 RJUMPV）或无条件跳转（RJUMP），则为所有当前指令目标。
4. 对于每个后继指令：
   1. 检查指令是否存在于代码中（即，执行不能“掉出”代码）。
   2. 如果通过先前的指令的向前跳转或顺序流访问后继指令：
      1. 如果指令没有记录的栈高度边界（第一次被访问），则将指令栈高度边界记录为在 2.3 中计算的值。
      2. 否则，该指令已被访问过（通过先前看到的向前跳转）。 更新此指令的记录栈高度边界，以便它们包含在 2.3 中计算的边界，即 target_stack_min = min(target_stack_min, current_stack_min) 并且 target_stack_max = max(target_stack_max, current_stack_max)，其中 (target_stack_min, target_stack_max) 是后继边界，而 (current_stack_min, current_stack_max) 是在 2.3 中计算的边界。
   3. 如果通过向后跳转访问后继指令，检查记录的栈高度边界是否等于在 2.3 中计算的值。 如果它们不相等，则验证失败，即我们看到向后跳转到不同的栈高度。

在访问所有指令后，确定函数最大操作数栈高度增加量：

1. 计算最大栈高度 max_stack_height 作为所有记录的栈高度上限的最大值。
2. 计算最大栈高度增加量 max_stack_increase 作为 max_stack_height - type[current_section_index].inputs。
3. 检查最大栈高度增加量 max_stack_increase 是否与类型段中相应的代码段的值匹配：types[current_section_index].max_stack_increase。

注意：尽管我们仅检查 max_stack_increase 是否与类型段定义匹配，这会保证它不会通过 EOF 标头定义超过 1023，但也可以保证 max_stack_height 不会超过 1024，因为否则 CALLF 和 JUMPF 对此段的验证会在操作数栈溢出检查时失败。 每个段都需要具有以其为目标的 CALLF 或 JUMPF，除了第 0 段（不允许无法访问的段）。 第 0 段需要具有 0 个输入，这意味着 max_stack_increase 等于 max_stack_height。

此过程的计算和空间复杂度为 O(len(code))。 每个指令最多被访问一次。

执行

鉴于部署时验证保证，EVM 实现不再需要为每个执行的指令进行运行时栈下溢或溢出检查。 异常是 CALLF 和 JUMPF 对整个被调用函数执行操作数栈溢出检查。

理由

已验证代码的属性

根据操作数栈验证验证的任何代码段都具有以下属性：

1. 没有无法访问的指令
2. 没有仅通过向后跳转可访问的指令
3. 操作数栈下溢不会发生。
4. 操作数栈溢出只能在 CALLF 或 JUMPF 指令处发生。
5. 以不同栈高度执行的多个向前跳转指令可能以同一指令为目标； 为所有可能的高度验证目标基本块的栈。
6. 任何向后跳转指令只能以使用相等栈高度执行的指令为目标； 这可以防止部署具有无界栈推送或弹出的循环。
7. 代码段中的最终指令是终止指令或 RJUMP。

仅在 CALLF/JUMPF 中进行栈溢出检查

在此 EIP 中，我们提供了一种更有效的 EVM 变体，其中仅在使用被调用函数的 max_stack_height 信息的 CALLF 和 JUMPF 指令中执行栈溢出检查。 这降低了 EVM 程序的灵活性，因为 max_stack_height 对应于函数中最坏情况的控制流路径。

无法访问的代码

操作数栈验证算法拒绝任何具有无法访问指令的代码。 可以非常廉价地执行此检查。 它可以防止部署退化的代码。 此外，它能够将指令验证和操作数栈验证组合到单个过程中。

终止时清除栈

当前要求在 RETF 指令之后，操作数栈为空（在当前函数上下文中）。 否则，RETF 语义会更复杂。 对于 n 函数输出，s 是 RETF 处的栈高度，EVM 必须擦除 s-n 个非顶部栈项，并将 n 个栈项移动到被擦除项的位置。 这种操作的成本可能相对便宜，但不是恒定的。 但是，取消该要求并如上所述修改 RETF 语义是向后 兼容的，并且可以在将来轻松引入。

更严格的栈验证

最初提出了另一种栈验证的变体，其中不是线性扫描代码段，而是通过以广度优先搜索方式跟踪每个跳转指令的目标来检查所有代码路径，跟踪每个被访问指令的栈高度，并检查每个可能的代码路径到特定指令，其栈高度保持不变。

此变体的优点是算法会更简单（我们不需要跟踪栈高度边界，而只需要每个指令的单个栈高度值），并且对代码基本块的排序没有额外的要求（见下文）。

但是，编译器团队反对这种严格的栈高度要求。 编译器使用的一种突出模式（这不可能实现）是从不同的栈高度跳转到终止助手（以 RETURN 或 REVERT 结尾的代码块）。 例如，这对于一系列 assert 语句很常见，每个语句都编译为 RJUMPI 到共享的终止助手。 强制执行恒定栈要求意味着在跳转到此类助手之前，必须弹出栈上的额外项，这会显着增加代码大小和消耗的 gas，并且会失去将这些常见终止序列提取到助手中的目的。

基本块排序

栈验证算法的先决条件是以一种方式对代码基本块进行排序，即没有块仅被向后跳转引用。

这是必需的，以便可以在代码段之上的一次线性传递中检查每个指令。 在代码段上的前向传递允许该算法“扩展”每个前向跳转目标的栈高度边界，并且仍然保持线性复杂度。 尝试在以广度优先搜索方式扫描代码时执行跳转目标栈边界扩展将需要在其栈高度边界扩展后重新检查整个代码路径，这将导致二次复杂度。

此要求并非 EOF 独有，但也存在于某些低级 IR 中，如 SPIR-V 和 LLVM MIR。

向后兼容性

此更改需要“网络升级”，因为它修改了共识规则。

它对向后兼容性没有风险，因为它仅针对 EOF1 合约引入，对于这些合约，不允许部署未定义的指令，因此没有使用这些指令的现有合约。 新指令不是为旧版字节码（非 EOF 格式的代码）引入的。

安全考虑

如上所述，所提出的验证算法具有线性计算和空间复杂度，并且其成本由事务数据成本 EIP-2028 覆盖。

版权

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

Citation

Please cite this document as:

Andrei Maiboroda (@gumb0), Paweł Bylica (@chfast), Alex Beregszaszi (@axic), Danno Ferrin (@shemnon), "EIP-5450: EOF - 栈验证 [DRAFT]," Ethereum Improvement Proposals, no. 5450, August 2022. [Online serial]. Available: https://eips.ethereum.org/EIPS/eip-5450.