形式化验证与SP1 Hypercube中的一个bug

本文深入剖析了Succinct Labs与Nethermind对SP1 Hypercube RISC-V zkVM的形式化验证工作。作者详细解释了验证的范围、假设、公理以及各个芯片的定理，并指出尽管验证了51个操作码的正确性，但存在多个未覆盖或错误的情况。通过测试发现了JALR指令的bug（未清除最低位），并利用LLM审计发现了SLTI指令的空证明和加载指令的错误规范。文章最后对形式化验证的沟通和验证提出了建议，强调需要明确的规范、可重现性和更多的验证。

致谢： 感谢 Tamir Hemo、Alex Hicks、Petar Maksimović、Derek Sorensen 和 Devon Tuma 审阅本文的初稿。

2025-10-09，Succinct Labs 博客发布以下公告：

我们很高兴地宣布，Nethermind 安全形式化验证团队与 Succinct Labs 已联手，在 Lean 证明助手中形式化验证 SP1 Hypercube（https://learnblockchain.cn/article/19280/）RISC-V zkVM 所有核心 RV-64 芯片的正确性。

这篇技术博文将详细解析形式化验证具体实现了什么，这为 SP1 Hypercube 的某些部分建立了强大的安全属性。它将强调一些已知的形式化验证局限性，并将描述最近发现并披露给 Succinct 的额外未知差距。文章最后提出了一些建议，关于 zkVM 安全专业社区如何更好地沟通形式化验证，以提高以太坊的安全性。

形式化验证声明

通俗地说，形式化验证软件承诺将软件的可信计算基（TCB）缩减为一组可以高度审查的简短组件列表。可信组件通常包括以下内容：

  • 基础逻辑；在本例中，是 Lean 的类型理论及其在 Lean 内核中的实现。Lean 的 elaborator（将高级 Lean 翻译为内核语言）不被信任，因为其实现中的错误不会允许证明 False，但可能导致内核验证的是某个不同于预期声明的有效证明。
  • 规范；在本例中，最终的真实来源是 Sail RISC-V 规范。Sail 是一种用于描述指令集架构的领域特定语言，Sail RISC-V 模型由 Golden Model 任务组 维护。
  • 提取管道 将内容引入验证环境；在本例中，约束从 Rust 提取到 Lean，RISC-V 规范从 Sail 提取到 Lean。
  • 提取后的任何处理（例如，编译为较低级别的代码然后执行）不影响提取工件的语义。
  • 定理陈述本身 以及所依赖的任何公理或假设。
  • 如果执行程序，Lean 的运行时执行 也被信任。这不适用于此处。

如果上述内容没有问题，那么该公告意味着存在 Lean 证明，表明 SP1 的若干约束实现了由 Sail RISC-V 规范定义的相应 RISC-V 机器指令；即满足约束意味着正确执行了相应指令。（这里有一些细微差别：另一个方向——正确执行 RISC-V 指令意味着满足相应约束——并未被证明，因为这需要对 SP1 的证明生成进行推理。）

这有助于增强对系统安全的信心。即使是一个带有额外假设的较弱陈述，通过帮助安全专业人员将精力集中在形式化验证未覆盖的特性上，也仍然有用。

公告中讨论的内容

形式化验证的源代码是公开的，该博文是一篇面向具有该主题丰富背景的读者的概述。博文中的一些声明包括：

具体来说，相关 RISC-V 操作码的行为已根据官方 64 位 RISC-V Sail 规范进行了验证。……我们已使用 Lean 证明助手验证了 64 位 SP1 Hypercube RISC-V zkVM 的整个核心相对于官方 RISC-V Sail 规范的正确性。这涵盖了以下 62 个操作码：

  • 41 个 ALU 相关操作码：ADD, ADDW, ADDI, ADDIW, SUB, SUBW, XOR, XORI, OR, ORI, AND, ANDI, SLL, SLLI, SLLW, SLLIW, SRL, SRLI, SRLW, SRLIW, SRA, SRAI, SRAW, SRAIW, SLT, SLTI, SLTU, SLTIU, MUL, MULH, MULHU, MULHSU, MULW, DIV, DIVU, DIVW, DIVUW, REM, REMU, REMW, REMUW
  • 10 个控制流相关操作码：JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LUI, AUIPC
  • 11 个内存相关操作码：SB, SH, SW, SD, LB, LBU, LH, LHU, LW, LWU, LD

这段引文使用了“正确性”一词，但更准确的说法是，它验证了某些操作码的“可靠性”。形式化验证工作按上述分类进行划分。Nethermind 仅负责证明 ALU 操作码的可靠性，而 Succinct 则自行承担证明控制流和内存相关操作码可靠性的任务。

在最后一部分，博文列举了标准假设：Lean 内核的正确性、提取的正确性以及作者对官方 RISC-V 规范翻译的正确性。它还列举了非标准假设和局限性。这些包括：“将不同‘芯片’中证明的陈述绑定在一起”的总线基础设施的正确性（一种优化）、“内存一致性”以及某些查找表的正确性。

代码中的声明

sp1-lean 仓库 在其最新提交 e4fa1b7 中（该提交于公告发布当天推送）包含了 Lean 4 证明。本节从基础开始，逐层列举了假设的内容和证明的内容。

公理

在 Lean 4 中，axiom 声明一个内核无需证明即接受的命题。与 theorem 不同（它必须由内核进行类型检查的证明项来证明），axiom 只是简单地断言。任何（即使是传递性地）依赖于公理的定理，其可信度都等同于该公理：如果公理不一致（断言了错误的东西），那么每个命题都变得可证明。

sp1-lean 证明使用了四个显式公理，声明在 Assumptions.lean 和 SailM.lean 中。

HTIF 禁用
-- SailM.lean line 10
@[simp] axiom plat_enable_htif_eq_false : plat_enable_htif () = false

HTIF（主机/目标接口设施）是一种允许模拟的目标机器与主机通信的机制。它并非必需。事实上，一份非官方规范 最近才准备好。但 RISC-V 的 Sail 模型支持这一概念，因此可以假设在 Lean 中需要处理它。

SP1 内存保护禁用
-- Assumptions.lean line 87
@[simp] axiom mprotect_disabled : public_value () 151 = 0

此公理与 RISC-V 规范无关。SP1 实现其自己的应用级内存保护机制（mprotect）作为自定义 zkVM 系统调用。public_value () 151 是 SP1 约束系统中的一个标志，用于控制 mprotect 是否激活。在每个指令读取器的约束中，都有一个项 (is_real - is_trusted) * (public_value () 151 - 1) 必须为零。当标志为 $0$（mprotect 禁用）时，这简化为 (is_real - is_trusted) * (-1) = 0，强制 is_trusted = is_real。每条执行的指令都必须通过总线查找表针对程序表进行验证。当标志为 $1$（mprotect 启用）时，该项消失，is_trusted 不受约束，允许行在不进行程序检查的情况下执行。该公理假定证明假设 mprotect 关闭，意味着所有指令都经过程序验证。

PMP 检查始终成功
-- Assumptions.lean lines 95-105
-- Comment: "We can't prove this directly because the loop in pmpCheck doesn't unfold."
axiom pmp_check_machine (reg_val offset : BitVec 64)
    (s : SailState) (hs : SailState.isInitialized s) (width : ℕ) :
    EStateM.run (pmpCheck ...) s = EStateM.Result.ok none s
axiom pmp_check_machine' (reg_val offset : BitVec 64)
    (s : SailState) (hs : SailState.isInitialized s) (width : ℕ) :
    EStateM.run (pmpCheck ...) s = EStateM.Result.ok none s

物理内存保护（PMP）定义在 RISC-V 特权架构规范第 3.7 节中。规范指出：“如果没有 PMP 条目匹配 M 模式访问，则访问成功。”SP1 不实现特权模式、CSR 指令或 MRET。它是一个纯 M 模式系统，根据 第 3.1.1 节（“简单的 RISC-V 实现可以仅提供 M 模式”）是最简单的有效 RISC-V 实现。由于 SP1 完全在机器模式下运行，并且未配置任何 PMP 条目（所有地址匹配字段保持在重置状态 OFF），因此所有内存访问应无条件成功。这些公理正是断言了这一点。

这些公理的存在是由于 Lean 的技术限制，而不是因为该声明存在疑问。Lean 内核通过逐步归结项来验证证明，评估表达式直到它们达到范式。Sail 模型的 pmpCheck 函数包含一个递归循环，该循环遍历所有 PMP 条目，并且此循环超出了 Lean 的归约预算（由 maxHeartbeats 控制）。内核无法通过暴力计算得出结果，因此作者将其声明为公理。

先决条件：约束表和 Main

SP1 将其电路组织成“芯片”，每个芯片处理一组 RISC-V 指令。每个芯片都有一个约束表，其中每一行代表一条指令的执行，每一列都是一个 KoalaBear 域元素（Fin KB，其中 $KB$ 是素数 $2^{31} - 2^{24} + 1$）。列数因芯片而异；例如，ADD 芯片有 $34$ 列，JALR 芯片有 $39$ 列，DivRem 芯片有 $247$ 列。列的含义因芯片而异。它们可以从生成的约束代码如何将 Main[N] 值传递给命名结构体字段的方式中恢复，但并未在独立的模式中定义。

定理的假设

除了全局公理之外，各个可靠性定理还带有假设：定理必须满足的前提条件。每个假设都是证明覆盖范围结束、信任开始的地方。以下是所有芯片定理中不同假设类型的完整列举。

标准假设（所有芯片）

每个定理都需要这三个假设。第一个 cstrs 断言芯片的生成的约束多项式被 Main 中的列值满足。在 SP1 的证明系统中，每个执行步骤产生一行域元素；证明者必须证明这些值满足芯片的约束多项式。cstrs 假设说：假设它们满足。然后证明展示接下来的结论。

(cstrs : (constraints Main).allHold)

第二个 h_is_real 区分真实执行行和填充行。SP1 的约束表被填充到 2 的幂次大小；填充行的 is_real = 0，并且不期望满足语义约束。此假设将定理限制为表示实际指令执行的行。

(h_is_real : Main[N] = 1)  -- N varies by chip (e.g., Main[33] for ADD)

第三个 state_cstrs 将约束列与指令执行之前的具体 Sail 机器状态联系起来。它断言 Main 中编码的寄存器和内存值与输入状态 s 匹配。例如，PC 列匹配 s.regs[PC]，操作数列匹配相应的寄存器值。然后定理的结论证明输出状态一致：Sail 规范和 SP1 实现从该输入开始运行时产生相同的结果。

(state_cstrs : (constraints Main).initialState s)

这使得每个芯片定理成为单步可靠性声明，即“如果输入状态匹配列，那么这一步指令是正确的”。将这些组合成全迹可靠性论证需要总线参数和内存一致性基础设施，博文将其列为未经验证的非标准假设。

状态初始化（JAL、JALR、分支、内存芯片）

对于读取 PC 或访问内存的指令的定理，还需要：

(hs : isInitialized s)

Sail 机器状态将寄存器存储在哈希映射中。isInitialized 定义为 ∀ reg : Register, reg ∈ s.regs：每个寄存器键都存在于映射中。这与寄存器值非零无关；而是关于键的存在，以便 s.regs.get Register.PC (hs _) 有良好定义。没有这个假设，寄存器读取在类型级别将是未定义的。仅 ALU 的芯片（ADD、SUB、MUL 等）不需要这个，因为它们只从约束列读取寄存器值，而不是直接从 Sail 状态读取。

操作码选择器（多操作码芯片）

有些芯片使用单个约束系统处理多个操作码。例如，BranchChip 涵盖了 BEQ、BNE、BLT、BGE、BLTU 和 BGEU。它不是为所有六个操作码提供一个定理，而是每个操作码都有一个单独的定理，每个定理都有一个像 h_is_beq : Main[29] = 1 这样的假设来选择哪个操作码标志是活动的。这些不是环境假设，而是情况拆分，选择 SP1 实现与之比较的 Sail 规范函数。

这种模式出现在 $8$ 个芯片中，涵盖约 $40$ 个操作码变体：

h_is_trusted（仅 ADDW）
-- AddwChip.lean line 39
(h_is_trusted : Main[32] = 1)

SP1 中的每个指令读取器都有一个 is_trusted 列。当 is_trusted = 1 时，读取器以多重性 is_trusted 发出一个 send (.program ...) 总线交互。这是一个查找表，证明该指令存在于加载的程序表中。当 is_trusted = 0 时，不会发生查找，指令在没有程序检查的情况下执行。

正如上面的“SP1 内存保护禁用”公理所解释的，当 mprotect 禁用时，约束强制 is_trusted = is_real，因此这个假设可以从 h_is_real 和 cstrs 推导出来。大多数芯片证明会自动推导出这一点。ADDW 定理 显式地表达了它，可能是因为在自动推导到位之前证明就已经编写好了，或者因为 ALU 读取器更复杂的结构使得自动提取不方便。

h_valid_pc（仅 JALR）
-- JalrChip.lean line 38
-- Write value is a valid PC value. This can be proved from constraints on newest sp1 branch
(h_valid_pc : (Main[15].val + Main[21].val) % 4 = 0)

JALR 定理 假设 $\text{next_pc} % 4 = 0$，这是每个其他分支/跳转芯片都携带的相同对齐假设。由于 SP1 的 JALR 省略了规范中的 $& \sim 1$ 步骤，这相当于要求未掩码和 $(rs1 + imm) % 4 = 0$。源代码注释承认这一点未经证明，并推迟到更新的 SP1 分支。这是与本文发现最相关的假设，并且是下面“此漏洞超出了形式化验证工作的范围”一节的核心主题。

hs_config（所有内存芯片）
-- e.g. StoreWordChip.lean line 34
(hs_config : SailState.isValidMemConfig s hs)

每个存储和加载定理都需要 isValidMemConfig，这是一个具有七个字段的结构：

structure SailState.isValidMemConfig (s : SailState) (hs : SailState.isInitialized s) where
  h_mprv_disabled : BitVec.ofNat 1 (BitVec.toNat (s.regs.get Register.mstatus (hs _)) >>> 17) = 0#1
  h_cur_privilege  : s.regs.get Register.cur_privilege (hs _) = Privilege.Machine
  h_clint_base     : s.regs.get Register.plat_clint_base (hs _) = 0
  h_clint_size     : s.regs.get Register.plat_clint_size (hs _) = 0
  h_plat_ram_base  : s.regs.get Register.plat_ram_base (hs _) = 0
  h_plat_rom_base  : s.regs.get Register.plat_rom_base (hs _) = 0
  h_plat_ram_size  : s.regs.get Register.plat_ram_size (hs _) = BitVec.ofNat 64 (2^64 - 1)

这假设了机器特权模式（特权架构规范第 3.1 节）、MPRV 禁用（无地址转换覆盖）、CLINT 基址和大小为零（无中断控制器区域）、ROM 基址为零，以及 RAM 覆盖整个 64 位地址空间。这些反映了 SP1 的实际执行模型，但并非从约束系统推导出来的。

h_fits_in_mem（所有内存芯片）
-- e.g. StoreWordChip.lean line 38
(h_fits_in_mem :
  let reg_val := (Word.toBitVec64 #v[Main[15], Main[16], Main[17], Main[18]]).toNat
  let offset := (BitVec.signExtend 64 (sp1_imm_c Main)).toNat
  let ram_size := (s.regs.get Register.plat_ram_size (hs _)).toNat
  reg_val + offset + 4 ≤ ram_size)

每个存储和加载定理都假设目标地址适合内存。边界因访问宽度和方向而异：

  • 存储：$\text{reg_val} + \text{offset} + \text{width} \leq \text{ram_size}$，其中宽度为 $1$（SB）、$2$（SH）、$4$（SW）或 $8$（SD）
  • 加载：$\text{reg_val} + \text{offset} + \text{width} < 2^{64}$，一个较弱的无溢出边界，用于 LB/LH/LW 及其无符号变体
h_is_aligned（仅 SH、SW、SD）
-- e.g. StoreWordChip.lean line 45
-- dt: This should eventually come from trusted instruction assumption
(h_is_aligned : is_aligned_vaddr (virtaddr.Virtaddr
  (Word.toBitVec64 #v[Main[15], Main[16], Main[17], Main[18]] + BitVec.signExtend 64
    (BitVec.ofNat 12 (Word.toNat #v[Main[21], Main[22], Main[23], Main[24]])))) 4 = true)

存储半字、存储字和存储双字要求有效地址自然对齐：

  • 对于 SH 为 2 字节
  • 对于 SW 为 4 字节
  • 对于 SD 为 8 字节

源代码注释“dt: This should eventually come from trusted instruction assumption”表明这原本打算从约束系统推导，但目前是假设的。存储字节（SB）不需要这个，因为字节访问是平凡对齐的。没有加载定理需要对齐。

定理表述的内容

每个芯片都有一个逐行可靠性定理，形式为“状态初始化”假设子节中描述的单步形式。例如，ADD 芯片定理（注解为我们的）是：

theorem correct_add
    (Main : Vector (Fin KB) 34)            -- 令 Main 为 ADD 约束表的一行。
    (s : SailState)                        -- 令 s 为参考机器的有效状态。
    (h_cstrs : (constraints Main).allHold) -- 如果所有多项式约束都满足，
    (h_is_real : Main[33] = 1)             -- 如果该行不是填充行，
    (state_cstrs : (constraints Main).initialState s)
                                           -- 并且 SP1 的状态与 s 匹配，
    :                                      -- 那么
    (spec_add op_c op_b op_a).run s        -- 参考机器在执行 ADD 后的状态
    =                                      -- 等于
    (sp1_add Main).run s                   -- SP1 Hypercube 在执行 ADD 后的状态。

Main 指的是相关芯片约束表的单行，假定该行已填充了证明值。定理问的是：如果约束接受这一行，它是否描述了一个正确的状态转换？结论的两边都描述了单个 ADD 指令的状态更新。

  • spec_add 是 RISC-V 规范的版本：从状态 $s$ 中读取两个源寄存器，通过 Sail 模型的 execute_RTYPE 计算它们的和，将结果写入目标寄存器，并将下一个 PC 设置为 $PC+4$。
  • sp1_add 是 SP1 的版本：执行相同的寄存器写入，但所有值都从约束列中读取。结果来自 Main[29..32]，下一个 PC 来自 Main[3..5] + 4。

两者都只是几个寄存器写入。.run s 将这些写入应用于输入状态 $s$ 并返回结果机器状态。

通过测试发现漏洞

RISC-V 架构测试 SIG 维护一套规范的测试，即 RISC-V 架构认证测试 (ACT)。在这个测试框架中，被测设备的行为与参考实现（可以是源自 Sail 模型的 C 实现）进行比较。这些是自检的 ELF 文件，其中嵌入了 Sail 参考模型在编译时计算的预期值。

在 SP1 v6.0.2 中对执行器运行 ACT4，在 RV64IM 套件中得到了 $62$ 个通过和 $64$ 个失败。一个失败是 FENCE 指令，SP1 从未实现过它。另一个是 I-jalr-00，即 JALR 指令测试。

JALR 应该做什么以及 SP1 Hypercube 的实现

RISC-V 规范在非特权 ISA 手册的“无条件跳转”部分中定义了 JALR（跳转并链接寄存器）：

间接跳转指令 JALR（跳转并链接寄存器）使用 I 型编码。目标地址 是通过将符号扩展的 12 位 I 立即数加到寄存器 $rs1$，然后将结果的最低位设置为零得到。跳转后的下一条指令地址 ($pc+4$) 被写入寄存器 $rd$。

即，计算出的目标地址为 $(rs1 + imm) & \sim 1$。清除最低位确保结果至少是 2 字节对齐的。

在 SP1 代码库中，我们看到最后一步缺失了。

JALR AIR 将 next_pc 定义为对 op_b (rs1) 和 op_c(imm) 执行 AddOperation 的原始输出，没有位清除操作，然后检查 next_pc 是否能被 $4$ 整除。任何 $rs1 + imm$ 的第 $0$ 位为 $1$ 的输入都将无法通过检查。正确的实现应该在整除性检查之前约束 $\text{next_pc} = \text{raw_sum} & \sim 1$。

// We constrain `next_pc` to be the sum of `op_b` and `op_c`.
let op_input = AddOperationInput::&lt;AB>::new(
    local.adapter.b().map(|x| x.into()),
    local.adapter.c().map(|x| x.into()),
    local.add_operation,
    local.is_real.into(),
);
&lt;AddOperation&lt;AB::F> as SP1Operation&lt;AB>>::eval(builder, op_input);

let next_pc = local.add_operation.value;
builder.assert_zero(next_pc[3]);

// Check that the `next_pc` value is a multiple of 4.
builder.send_byte(
    AB::Expr::from_canonical_u32(ByteOpcode::Range as u32),
    next_pc[0].into() * AB::F::from_canonical_u32(4).inverse(),
    AB::Expr::from_canonical_u32(14),
    AB::Expr::zero(),
    local.is_real,
);

类似地，证明者对应的迹生成代码仅计算加法。如果和不是 4 字节对齐的，范围检查将失败。

cols.is_real = F::one();
cols.op_a_value = event.a.into();
let low_limb = (event.b.wrapping_add(imm) & 0xFFFF) as u16;
blu.add_bit_range_check(low_limb / 4, 14);
cols.add_operation.populate(blu, event.b, imm); -- event.b is the rs1 value

最后，SP1 的执行器有多个后端。在 x86_64 Linux 上（几乎所有的证明基础设施都在此运行），执行器使用 JIT 后端 来发出本机 x86 指令。该后端中的 JALR 实现计算 $rs1 + imm$ 并直接将其存储为下一个 PC。

add Rq(TEMP_A), imm as i32;
mov QWORD [Rq(CONTEXT) + PC_OFFSET], Rq(TEMP_A)

这三个层彼此一致，表明问题在于电路设计。

实际影响可能有限：编译器几乎从不生成第 $0$ 位为 $1$ 的 JALR 目标，因为 $& \sim 1$ 的清除是规范级别的细节，大多数工具链不依赖它。但 RISC-V 规范允许这样做，架构测试套件覆盖了它，并且一个经过形式化验证的系统应该处理它（或将其更明确地记录为限制）。

此漏洞超出了形式化验证工作的范围

如上所述，SP1 的 JALR 芯片的形式化验证 包含了这个 $h_valid_pc$ 假设

(h_valid_pc : (Main[15].val + Main[21].val) % 4 = 0)

在 JALR_correct 定理上：

theorem JALR_correct
    (cstrs : (constraints Main).allHold)
    (h_is_real : Main[30] = 1)
    (hs : isInitialized s)
    -- Write value is a valid PC value. This can be proved from constraints on newest sp1 branch
    (h_valid_pc : (Main[15].val + Main[21].val) % 4 = 0)
    (state_cstrs : (constraints Main).initialState s) :
    let op_b := sp1_op_b Main
    let op_a := sp1_op_a Main
    let op_c := sp1_op_c Main
    (spec_jalr op_c (.Regidx op_b) (.Regidx op_a)).run s = (sp1_jalr Main).run s

这个 $\text{next_pc} % 4 = 0$ 的对齐是所有分支/跳转芯片携带的假设。在 JALR 的情况下，SP1 在计算 $\text{next_pc}$ 时省略了规范中的 $& \sim 1$ 掩码，因此假设适用于未掩码的和 $rs1 + imm$。

编译器可能生成 $rs1 + imm$ 的第 $0$ 位为 $1$ 的 JALR 输入，尽管经过规范强制掩码后目标是 4 字节对齐的。对于这样的程序，可靠性定理不适用，并且在测试中，SP1 证明者崩溃。即使不崩溃，也存在会导致验证者拒绝证明的约束。这是一个完备性漏洞，实际上可能是一个拒绝服务向量。根据形式化验证工作的范围，这不是 sp1-lean 中的差距。这项工作仅试图通过建模 SP1 并表明其语义与 Sail 模型完整语义的子集匹配来建立可靠性保证。这凸显了需要扩大 sp1-lean 的范围，或用其他方法补充形式化方法以确保证明者的正常运行时间。

对于分支和 JAL，trusted_instr 假设对立即数施加了四字节对齐，结合 PC 对齐得出 $\text{next_pc} % 4 = 0$。SP1 不实现 C（压缩指令）扩展，因此一个 2 字节对齐的目标应该引发指令地址未对齐异常。未来的工作将检查是否符合执行终止语义标准，这将覆盖这种情况。

在我们向他们报告 JALR 漏洞后，Succinct 报告说他们在 SP1 v6.1.0 中修复了它（参见 fix: JALR LSB clearing 提交）。我们尚未尝试更新 Lean 证明。

重申标准的价值

当被告知 JALR 漏洞时，Succinct 迅速承认了该发现，并且他们的 SP1 下一个版本包含了一个补丁，展示了他们遵循标准的承诺。

总的来说，标准对于特定用例的最优性与互操作性的好处（包括共享工具的可用性和外部安全分析的适用性）之间存在权衡。人们可以合理地争辩说，不是四字节对齐的两字节对齐目标地址是一种小众可能性，要么在我们的用例中看不到，要么会在测试中被捕获。然而，以太坊需要最强大的可用保证。依赖测试覆盖率加上编译后验证步骤来确保客户程序不包含有效但不支持的指令，对于安全关键基础设施来说太脆弱了。

更广泛地说，以太坊基金会的 zkEVM 团队，在广泛的社区输入和支持下，提出了一套 zkEVM 标准，这些标准建立在官方 RISC-V 规范之上，无需修改。这些目标在于提供互操作性保证和安全改进。

来自 LLM 辅助审计的额外发现

上述 JALR 发现来自合规性测试和手动检查。在得知此问题后，Alex Hicks 使用 LLM 辅助过程对剩余定理进行了系统审计。这暴露了我们现在讨论的额外问题。

一个智能体以 JALR 问题为指导示例，并被要求执行以下任务：

  1. 编译所有声明（定理、引理等）的列表。
  2. 对于每个声明，列出定理目标和假设。
  3. 对于每个定理目标和假设集，评估定理目标以及所使用的任何假设相对于 RISC-V 规范是否合理。

这个过程暴露了两类问题，单靠手动审查假设列表是无法捕获的：一个什么都证明不了的定理（来自矛盾假设的空真）和证明错误东西的定理（用错误值参数化的规范函数）。

空证明

由于从 Sltu 命名空间复制粘贴的错误，LtChip.lean 中的 SLTI 定理 是空真的。Slti 命名空间在第 84 行声明了一个 variable (h_is_sltu : is_sltu Main)，它要求 Main[31] = 0。然后定理 correct_slti 在第 134 行采用一个显式的 (h_is_slti : is_slti Main)，它要求 Main[31] = 1。由于 Lean 4 的变量自动插入，两个假设都出现在最终的定理类型中：

Slti.correct_slti (Main : ...) (s : SailState)
  (h_is_sltu : is_sltu Main)   -- requires Main[31] = 0
  (h_is_slti : is_slti Main)   -- requires Main[31] = 1
  ...

由于 Main[31] 不能同时为 $0$ 和 $1$，这些假设是矛盾的，定理在没有证明任何东西的情况下被解除。不需要 sorry，因为 Lean 的内核可以从 False 推导出任何结论。

虽然这确实意味着 SLTI 在最初的开发中没有有效的可靠性证明，但一旦拼写错误被纠正，很容易按预期证明定理，这意味着 Lt 芯片从一开始就正确实现了 SLTI 指令，并且没有任何相关的潜在利用。通过这个修复（将包含在这个拉取请求中），SP1 将受到保护，免受 SLTI 中的静默回归。

错误的规范

LoadHalf 和 LoadWord 的规范函数使用了错误的访问宽度。LoadHalfChip.lean:26 定义了 spec_lb 为 execute_LOAD ... (width := 1) 而它应该是 width := 2（半字）；LoadWordChip.lean:27 也做了同样的事，而它应该是 width := 4（字）。这些定理证明 LoadHalf 和 LoadWord 芯片约束匹配字节加载语义。即使这些文件中的 sorry 标记被解决，证明也是在证明错误的事情。LH、LHU、LW 和 LWU 实际上未经验证。

形式化验证结果的最终统计

具有逐行可靠性定理的芯片完整列表：

博文声称在三个类别中验证了 $62$ 个操作码。以下列出了每个操作码及其可靠性定理的链接，或注明其缺失。这里引入了两个标签：无定理 意味着约束已提取到 Lean，但没有陈述可靠性证明；sorry 意味着定理依赖于未完成的引理。其余标签（空真 和 错误规范）与前面同名章节中讨论的一致。

SLTI 有一个定理，但由于矛盾假设它空真（参见上面的“空证明”部分）。NOP 不是一个单独的操作码；它是 ADDI x0, x0, 0 的别名，被 ADDI 定理覆盖。

这些通过 trusted_instr 假设目标为 4 字节对齐，这在形式上比规范要求的 2 字节更严格，但不排除任何在 RV64I 中具有良好定义行为且没有 C 扩展的程序（参见上面的“此漏洞超出了形式化验证工作的范围”部分）。JALR 是不同的：$h_valid_pc$ 假设了位清除前的和为 4 字节对齐，排除了 $rs1 + imm$ 的第 $0$ 位为 $1$ 的有效输入，这种情况具有明确的规范行为（清除第 $0$ 位，正常继续）。LUI 和 AUIPC 无定理：该文件导入了约束但不包含证明。

  • 11 个内存相关操作码中的 4 个具有完整、正确的定理：

所有 6 个加载定理都依赖于 sorry（符号扩展引理中的未完成证明）。此外，LH 和 LHU 定理证明的是字节加载语义（宽度=$1$）而不是半字（宽度=$2$），而 LW 和 LWU 类似地证明的是字节加载而不是字加载（宽度=$4$）。即使完成，这些证明验证的是错误规范（参见上面的“错误规范”部分）。

只有 LB 和 LBU 证明了正确的规范，尽管由于 sorry 它们仍然不完整。

LD 无定理：该文件包含定义但没有证明，尽管有完全提取的约束。

除了 62 个操作码的声明之外，FENCE 是 RV64I 基础整数 ISA 的一部分，并且是合规性所必需的，但 SP1 从未实现过它，无论是在执行器中还是在约束系统中。

考虑到所有问题，声称的 62 个操作码中有 51 个具有完整、正确的证明：40 个 ALU 相关（除 SLTI 外全部）、7 个控制流（JAL 和全部六个分支）和 4 个存储（SB、SH、SW、SD）。

关于沟通和验证形式化验证的建议

形式化验证通常被认为是安全分析的终极形式，甚至可能消除对其他安全措施（如实现多样性、测试和源代码审计）的需求。这使得验证工作必须极其谨慎地完成，并且结果的沟通必须始终精确。

关于形式化验证中使用的代码，无论是规范、提取还是定理证明，从业者有责任最大化清晰度。随着近年来 AI 的显著改进，有人可能会争辩说“代码质量”越来越不重要。同样，AI 代理可以轻松地重写代码以提高清晰度，只要人类验证是生成关键系统过程的一部分，那么谨慎的做法是使用使代码可读的抽象和开发模式。

关于组织，我们建议的一个特定实践是拥有少量封装定理。从许多小的单个定理向上推理到关于整个系统的陈述更加困难，而全局定理可能意味着存在更具表达力的抽象。

另一个应该遵循的开发实践是从基本输入显式可重现。就 SP1 而言，在自述文件中指定了 Lean 和 Mathlib 的版本，但将 SP1 提取到 Lean 的过程没有指明使用了哪个 SP1 版本。参考端也是如此：应该固定 Sail RISC-V 模型的提交及其对应的 RISC-V 非特权 ISA 的批准版本，并与证明一起公开，以便读者可以判断验证所声称的标准是哪个修订版。应该提供完整的可重现构建设置。每次提交影响验证所声称的代码时，都应执行提取并重建证明文件。

公开沟通应适当地对进展进行背景化。Succinct 的公告值得称赞，因为它明确指出了假设，但在试图为普通受众简化的过程中，以及由于形式化验证中的实际错误，它包含了显著的误导性陈述。

最后，验证至关重要。对于任何足够大的代码库，漏洞都是统计上的可能性。在形式化验证的情况下，规范是代码，同样的原则适用。规范和安全目标（即定理）在许多情况下很难正确制定；人类和 AI 都会经常犯错。这必须由可以更加确定性的审查过程来缓解。

在公开提出关于代码的声明之前，应该对验证声明进行适当的测试，加上由新视角和 AI 进行的审查。

鉴于形式化验证的强烈承诺，以及许多技术受众普遍认为它是使其他形式的安全分析变得不必要的最終工具，因此在沟通哪些已被证明、哪些尚未被证明时需要极其谨慎。

  • 原文链接： zkevm.ethereum.foundatio...
  • 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ，好文好收益，欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
Cody Gunton
Cody Gunton
江湖只有他的大名，没有他的介绍。

Cody Gunton

如果觉得我的文章对您有用，请随意打赏。你的支持将鼓励我继续创作！

作者暂未设置收款二维码