Think thickly
所有文章 标签 分类 文档 关于 友链
Think thickly

目录

zkEVM 与 ZK 系统安全性：约束设计、内存一致性与 soundness footguns

 收录于 Cryptography
   约 3543 字   预计阅读 8 分钟 

Scope. 本文审计 zkEVM 的 constrained surface：opcode row、memory/storage queues、lookup、state commitments 与 recursive accumulator 之间是否形成闭环。产品吞吐量和功能覆盖不在讨论范围内。

proof 只覆盖进入约束、commitment 和 transcript 的对象。zkEVM 会把 opcode 语义、memory read/write、storage queue、状态根更新、lookup 表和递归聚合拆成 constraint obligations；soundness 要求这些局部义务共同绑定同一条 execution trace。1 2

常见 failure mode 是 linkage 丢失：selector 没有绑定正确路径，queue payload 没有等于前一层结果，limb lookup 缺少 recomposition，或 challenge 少吸收一个 commitment。此时 prover 可以提交局部合法而全局矛盾的 witness。

证明系统到底在验证什么

zkEVM 对 opcode semantics 做 constraint-obligation mapping：把每条 opcode 的语义拆成局部约束与跨模块一致性义务。

以一条简化的 SSTORE 风格语义为例，程序员脑中的语义大致是：

  1. 从当前上下文读出 address、slot、value
  2. 根据当前 state 计算写入前后的状态差异
  3. 更新 storage、refund、access list 或其他相关状态
  4. 把新的全局状态承诺到下一步

但在约束系统里，这些语义会被分解成：

  1. opcode decoder 约束当前 row 的 selector 是否对应 SSTORE
  2. witness columns 提供 address、slot、value 等局部对象
  3. lookup 和 range checks 保证字节分解、字段范围、编码格式合法
  4. memory / storage queues 记录读写事件
  5. 排序或去重电路检查这些事件满足时间顺序与键一致性
  6. 递归或聚合层最终只验证若干 commitments 与 accumulator 关系

拆分后，每条 linkage 都要在电路中有明确消费者。漏掉一条边，系统只能证明若干局部片段分别合法，无法推出它们描述同一条 opcode execution。

One VM, Many Auxiliary Consistency Tasks

系统可以把全局一致性分配给多电路或多层证明结构。截至 2026-08-08，ZKsync EraVM 文档仍区分 Main VM、StorageSorter、CodeDecommitter、RAMPermutation 等基础电路，并通过 queues 与递归层连接公开输入；Scroll 则已在 Euclid 升级后转向 OpenVM，由 RISC-V 程序承载 EVM 验证逻辑，再按 chunk、batch、bundle 三层聚合。1 3 4 2

安全性审阅需要同时覆盖局部 gate 和模块间闭环。

Key Observation. proof 的目标陈述是：所有拆开的局部 obligations 共同锁定同一条 execution trace。

Memory And State Consistency

opcode arithmetic、hash gadget 和 precompile gadget 负责局部计算；memory and state consistency constraints 负责把这些计算接成同一段历史。

原因很直接。大系统里，单步局部语义通常不难写；难的是保证：

  • 这一步读到的值，真的是前面某一步写进去的值
  • 这次 storage update，真的是对同一个 key 做的前后更新
  • rollback、refund、access list、nonce、balance 等状态共享同一条更新历史
  • 递归聚合前后的 commitments 的确绑定的是同一份历史

这就是 memory and state consistency constraints 的核心。

Memory Consistency

把内存读写写成事件流之后，最朴素的正确性条件其实只有一句：

对同一个地址和时刻，最后一次写入必须决定之后读出的值。

但为了把它变成可证明对象，系统通常会把读写事件编码成某种 queue 或 multiset，再借助排序、permutation、timestamp 检查等机制去表达：

\[ \text{read}(addr, t) \Rightarrow \text{value} = \text{last-write-before}(addr, t). \]

一旦这条关系没有被完整表达，局部电路即便都成立，prover 仍可能让“当前 opcode 看到的 value”和“全局 memory history 里的 value”发生偏离。

Queues, Sorting, And State Roots

auxiliary circuits 承担以下 global consistency 工作：

  • memory queue 负责把局部读写事件送入全局历史
  • sorter 负责把同一 key 或地址的事件排到可比较顺序
  • state root / storage root 更新负责把局部变化压成 commitment 边界
  • recursion / aggregation 层负责把很多局部 obligations 再压成更小的 verifier surface

ZKsync 的 StorageSorter 展示了这种分工：Main VM 输出 queues，排序与去重电路再检查 storage requests 的顺序、permutation accumulators 和 read consistency。4

memory consistency 是各执行模块共同满足的 global invariant。

Under-Constrained Circuits Usually Mean Missing Linkage

under-constrained circuits 这个词很常见，但很多时候说得还是太抽象。更直接一点：

under-constrained circuit 会保留本应由预期语义锁定的 witness 自由度。

换句话说，某些自由度本来应该被锁死，却仍留在 witness 里。

Local Checks Can All Pass

这类 bug 的可怕之处在于，它们经常满足下面的表象：

  • selector 检查通过了
  • lookup 表查到了
  • range check 也过了
  • queue 事件格式合法
  • 最终 quotient 看上去没有问题

但这些只说明“局部片段各自合法”，不说明“它们描述的是同一个 execution fact”。

Trail of Bits 在 Halo2 相关案例里展示过同类问题：约束系统若没有连接本应相等的对象，会接受设计者未预期的 witness。5

A Toy Soundness Bug From Missing Constraint Linkage

设一个简化 opcode 在 8-bit 范围内计算 \(r=a+b\)，随后把事件

\[ q=(\mathit{addr},\mathit{ts},v) \]

追加到 memory queue。selector \(s=1\) 表示当前行启用。已有约束只有：

\[ s(s-1)=0, \qquad s(r-a-b)=0, \]

以及 \(a,b,r,v\in[0,255]\) 的 lookup 和 queue tuple 的格式检查。下面两份 witness 都通过这些局部约束：

字段 含义 Honest witness Adversarial witness 已有局部检查
\(s\) opcode selector 1 1 boolean
\(a\) ALU 左输入 7 7 8-bit lookup
\(b\) ALU 右输入 5 5 8-bit lookup
\(r\) ALU 输出 12 12 \(s(r-a-b)=0\), 8-bit lookup
\(\mathit{addr}\) 写入地址 9 9 queue format
\(\mathit{ts}\) 时间戳 4 4 queue format
\(v\) queue payload 12 99 8-bit lookup, queue format

逐项代入可得：两行都有 \(1(12-7-5)=0\)，所有数值也都落在 8-bit 表内。memory consistency 电路只消费 queue 中的 \(v\)，因此攻击行会把 99 带入后续历史。

缺失的约束是

\[ s(v-r)=0. \]

诚实行给出 \(1(12-12)=0\)，攻击行给出 \(1(99-12)=87\ne0\)。若 opcode 禁用时 queue 也必须为空，还要同时约束 event enable、queue length delta 和 payload 的 gated canonical value；只补 \(v=r\) 不能覆盖 selector 与队列计数之间的断边。

这张表提供一种直接的负向测试：固定所有诚实列，只修改跨模块 payload。若 witness generator 或 prover 仍能生成可验证 proof，审计者就得到了一条可复现的 under-constraint，而非泛化的“可能缺约束”描述。

Lookup、Range 与 Transcript 都会扩大攻击面

写到这里，危险边界已经比较清楚了。下面两类对象尤其容易让人产生“已经检查过了”的错觉。

Lookup And Range Assumptions

lookup and range assumptions 确实能显著降低电路复杂度，但它们也引入了额外信任边界：

  • table 本身是否真表达了你想要的语义
  • limb 合法是否真的推出原对象合法
  • decomposition 与 recomposition 是否双向绑定
  • 不同列之间是否只做了局部 membership，却缺少全局一致性

例如一个 256-bit word 被拆成若干 limb，每个 limb 都通过 range check，并不自动推出原 word 被正确使用。若缺少

\[ x = \sum_{i=0}^{k-1} 2^{w i} x_i \]

这样的 recomposition 约束，系统可能只证明“这些 limb 分别在范围内”，却没有证明“它们就是这个 word 的真实分解”。

这类问题和上面的 queue linkage 是同一类 bug：局部合法，不等于全局语义闭合。

Fiat-Shamir And Transcript Misuse Pitfalls

Fiat–Shamir 的常见工程风险来自 transcript 覆盖不全，而非底层哈希碰撞。

如果 challenge 没有绑定：

  • 某个 auxiliary queue commitment
  • 某个 lookup table commitment
  • 某个 recursive layer 的 accumulator state
  • 某个 instance boundary 上的公开承诺

那么 prover 可能在 challenge 生成后仍保留额外自由度，等于把一部分应该固定的 witness 留到了后面。

transcript 要把所有待 challenge 绑定的 commitments 放进不可回退的顺序。顺序、覆盖面或域分离出错，都会在 system boundary 留下适应性自由度。

System-Level Soundness Boundary

现在可以回到开头那句话：proof 只覆盖被约束并被 commitment 绑定的对象。

所以 system-level soundness boundary 必须明确区分两件事：

  1. 电路层是否完整表达了预期语义
  2. 系统运行模式是否真的在消费这些被证明的语义

如果某个 dev/test mode 允许 mock finalization、跳过真实 proof，或把 bridge / settlement 步骤交给外部治理逻辑，这些路径就超出了密码学证明自动覆盖的范围。审计需要把运行配置与 production verifier 的实际调用链一起纳入边界。

这一区分用于列出 proof 之外的 trust assumptions；某个模块有 proof，不能推出部署系统已经消除所有额外信任。

Engineering Attack Surface Checklist

如果把这篇压成一份审计清单，我会先查这几类点：

  1. opcode semantics to constraint obligation mapping 是否有缺边
  2. memory and state consistency constraints 是否真的闭合到队列、排序与状态承诺
  3. 是否存在 under-constrained circuits，尤其是 selector、equality linkage、recomposition linkage 漏掉的地方
  4. lookup and range assumptions 是否只检查了局部合法性，而没有检查全局绑定
  5. Fiat-Shamir and transcript misuse pitfalls 是否可能让 challenge 在少吸收对象的情况下生成
  6. recursive aggregation 有没有遗漏某个 accumulator / commitment 边界
  7. 系统部署与运维模式是否超出了 proof 覆盖的 system-level soundness boundary

这七项共同构成本文的 engineering attack surface。

Summary

zkEVM 的安全性不能只看“有没有证明系统”，而要看证明系统到底绑定了什么。

这条线可以压成四句话：

  1. zkEVM 通过 opcode-semantics-to-constraint-obligation mapping 构造证明对象
  2. memory consistency 与更一般的 memory and state consistency constraints 是全局 backbone
  3. missing constraint linkage 是 under-constrained circuits 的高频来源
  4. lookup and range assumptions、Fiat-Shamir transcript、recursive aggregation 与部署模式一起定义了 system-level soundness boundary

工程验收需要回答：系统声称的 execution semantics 是否完整、闭合地进入约束、commitment 与 transcript。

工程实现对接

如果把这篇落回工程动作，最值得保留的是三件事：

  • 设计阶段先画 dependency graph，明确每个 opcode 结果最终被哪些 queue、state root、accumulator 消费
  • 审计阶段优先沿 dependency graph 查 missing linkage，再检查局部代数公式
  • 测试阶段构造 adversarial witness，用“局部都合法、全局不一致”的方式去撞 under-constrained circuits

这些动作直接针对 zk 系统的常见失效路径。

References

  1. ZKsync Era Docs, Concrete Circuits Overview, https://docs.zksync.io/zksync-protocol/era-vm/circuits/circuits. ↩︎ ↩︎

  2. Scroll Docs, Proof generation, https://docs.scroll.io/en/technology/prover/proof-generation/. ↩︎ ↩︎

  3. ZKsync Era Docs, Main VM, https://docs.zksync.io/zksync-protocol/era-vm/circuits/circuits/main-vm. ↩︎

  4. ZKsync Era Docs, StorageSorter, https://docs.zksync.io/zksync-protocol/era-vm/circuits/circuits/sorting/storage-sorter. ↩︎ ↩︎

  5. Trail of Bits, A Riel Dilemma in Halo2 CE, https://blog.trailofbits.com/2024/02/20/a-riel-dilemma-in-halo2-ce/. ↩︎

更新于 2026-05-30  207eeaf
阅读原始文档
 Cryptography, Zkevm, Soundness, Plonkish, Engineering
返回 | 主页