# zkEVM 与 ZK 系统安全性：约束设计、内存一致性与 soundness footguns > 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。[^zksync-circuits] [^scroll-proof] 常见 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 三层聚合。[^zksync-circuits] [^zksync-mainvm] [^zksync-storage] [^scroll-proof] 安全性审阅需要同时覆盖局部 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。[^zksync-storage] 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。[^tob-under] ### 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 [^zksync-circuits]: ZKsync Era Docs, *Concrete Circuits Overview*, . [^zksync-mainvm]: ZKsync Era Docs, *Main VM*, . [^zksync-storage]: ZKsync Era Docs, *StorageSorter*, . [^scroll-proof]: Scroll Docs, *Proof generation*, . [^tob-under]: Trail of Bits, *A Riel Dilemma in Halo2 CE*, .