ZK-Rollup 电路欠约束：为什么一个缺失约束能伪造合法状态证明

摘要：ZK 电路安全失败通常不是证明系统被攻破

ZK-Rollup 的安全性不只取决于 Groth16、PLONK 或 Halo2 是否满足密码学声音性。更常见的工程风险是：电路约束没有完整表达执行语义，证明系统只证明“某组变量满足这些多项式”，却没有证明“这就是合法的状态转换”。这类欠约束（Under-constrained）漏洞会让证明者为非法余额、错误地址、缺失范围检查或伪造状态根生成可验证证明。本文从 R1CS/Plonkish 约束模型、Circom 与 Halo2 的赋值语义、SMT 形式化验证和静态分析路径出发，说明欠约束为何难以被单元测试发现，以及 AllSwap 这类跨链路由系统为什么需要把证明电路质量纳入结算风险模型。

问题边界：证明有效不等于状态转换正确

本文讨论的是防御性电路审计，不提供可复用攻击 payload、真实协议目标选择或漏洞利用步骤。系统角色包括：Rollup 排序器、证明者、链下执行器、ZK 电路、链上验证合约、用户、跨链路由器和审计工具。攻击者能力假设为：可以控制 witness 输入，可以构造边界状态，可以寻找未被约束的中间变量，可以提交满足约束但不符合业务语义的证明；不假设攻击者能破解哈希函数、伪造可信设置或破坏椭圆曲线离散对数。

关键边界在于“计算程序”和“约束系统”不是同一件事。程序可以写出 `z = f(x)`，但证明系统只看到若干有限域方程。若方程没有强制 `z` 被 `x` 唯一决定，证明者就可能选择另一个 `z'`，让电路通过但业务状态错误。Circom 文档对 witness-only 赋值和带约束赋值的区分正是这个问题的最小样本：前者只给 witness 赋值，后者同时生成约束。Halo2/Plonkish 电路也类似，advice cell 被赋值并不自动意味着它参与了有效 gate、lookup 或 equality constraint。

在 Rollup 场景中，欠约束的破坏面比普通隐私应用更大。一个身份电路少约束了某个 bit，最多影响一笔证明的声明；一个状态转换电路少约束了 balance、nonce、storage key 或 Merkle path，可能影响整个批次的状态根。链上验证器只能看到 proof 和 public inputs，无法复算链下执行轨迹。一旦错误 proof 被接受，后续跨链提现、桥释放、流动性结算和退款归因都会继承错误状态。

形式模型：从唯一性到轨迹一致性

把链下执行函数记为：

```text T(s_old, txs) = (s_new, receipts, aux) ```

其中 `s_old` 是旧状态根，`txs` 是交易序列，`s_new` 是新状态根，`receipts` 是执行回执，`aux` 包含读写表、Merkle path、range-check 分解和哈希中间值。ZK 电路真正生成的是约束关系：

```text C(public, witness) = 0 public = (s_old, s_new, batch_hash, data_commitment) witness = (txs, traces, reads, writes, paths, intermediate) ```

安全目标不是“存在一个 witness 使 C 为 0”，而是更强的语义等价：

```text C(public, witness) = 0 iff witness encodes a valid execution of T ```

欠约束发生在右到左以外的方向：存在 `witness_bad`，它满足 `C = 0`，但不对应合法执行。更精确地说，若某个输出变量或中间变量没有被 public input 和前序 witness 唯一决定，则证明者拥有自由度。Picus/PLDI 相关工作把问题抽象为有限域多项式方程中的唯一性推理；USENIX Security 2024 的 Circom 静态分析研究进一步强调，真实漏洞往往来自程序轨迹与约束集合之间的偏差，而不是单个数学公式写错。

对工程师更有用的检查不是“约束数量够不够多”，而是“每个安全相关变量是否被正确消费”。一个电路可以有百万级约束，仍然漏掉一个决定资产归属的布尔选择器。反过来，一个小电路只要所有输出都由输入唯一决定，并且范围、域分离和查表边界清晰，也可以是安全的。约束安全是语义覆盖问题，不是规模问题。

欠约束的工程来源

第一类来源是 witness 赋值和约束生成混淆。Circom 的 witness-only 赋值常用于位运算、除法、哈希预处理等难以直接写成二次约束的计算，但赋值后必须补充约束。例如把 `a` 分解成 bits 时，只生成 witness bits 不够，还必须证明每个 bit 满足 `b * (1 - b) = 0`，并证明加权求和还原原值。否则证明者可以给出看似合理的 bit 数组，却让原值范围检查失效。

第二类来源是选择器、查找表和自定义门未启用。Halo2/Plonkish 电路通过 fixed/advice/instance columns、selector、custom gate 和 lookup 组合表达语义。一个 cell 被赋值后，如果 selector 没有在对应 row 打开，或 lookup 没有把它纳入表约束，它只是一块 witness 内存，不是被证明的事实。CEUR 上关于 Halo2 自动分析的工作把 unconstrained cells、unused gates 和 selector 错配列为高风险信号，原因就在这里。

第三类来源是范围和别名错误。有限域中的值天然按模数运算，业务语义却经常要求 uint64、uint160、uint256 或地址域。若电路没有证明 `x` 落在业务要求的 k 位整数范围内，两个不同整数可能在有限域中被视作同一个元素。对于余额、amount、nonce 和 storage slot，这会导致“一证多解”：链下执行器以整数语义解释，电路以有限域语义解释，两者边界不一致。

第四类来源是 Merkle/状态树路径没有完整约束。ZK-Rollup 的状态电路不仅要检查哈希路径，还要约束叶子编码、路径方向、树高、空叶语义、旧值和新值转换。如果只约束 root recomputation，却漏掉 key 与 path index 的绑定，证明者可能证明“某个叶子在树里”，但不是“目标账户的这个存储槽被正确更新”。

第五类来源是 public input 绑定不完整。证明如果没有绑定 chainId、batch number、data commitment、verifier address 或电路版本，同一个 proof 可能在错误上下文里被重放。对跨链结算而言，`s_new` 正确还不够；它必须属于正确 Rollup、正确批次、正确 DA 承诺和正确桥消息队列。

形式化验证：把电路当成有限域程序审计

形式化验证的目标不是证明“没有 bug”这种空泛结论，而是证明若干可机器检查的安全性质。第一层是变量约束覆盖：每个 output、public input 相关中间值、状态根组成值、余额变更值都必须出现在非平凡约束中。Circomspect 这类静态分析器能发现 under-constrained signal、unused variable、可疑 assert、BN254 特定常量误用等模式，适合作为 CI 的第一道门。

第二层是唯一性检查。给定 public input 和一部分 witness，SMT 或代数求解器尝试寻找两个不同 witness，使它们都满足约束但输出不同：

```text C(public, w1) = 0 C(public, w2) = 0 critical(w1) != critical(w2) ```

若该公式可满足，就说明电路至少在某个关键变量上没有唯一性。Z3 这类 SMT 求解器适合表达 bit-vector、数组、整数范围和控制流条件；Picus 一类工具则直接面向有限域多项式方程推理，减少语言前端差异带来的误判。

第三层是轨迹一致性测试。zkFuzz 提出的思路更接近程序测试：比较程序执行轨迹允许的值和约束系统允许的值。如果修改计算逻辑后，约束仍然接受不应接受的 witness，就说明电路没有锁住语义。这对 Rollup 特别重要，因为执行轨迹不只是输出状态根，还包括每条交易的读写、nonce 增长、gas 消耗、日志、退出消息和失败回滚。

第四层是差分约束审计。对同一个状态转换，至少保留三种表示：高层规格、执行器 trace、约束系统。任何优化都必须能解释它如何保持语义等价。比如把 Keccak 路径换成 Poseidon 辅助承诺，不能只说“更 SNARK-friendly”；必须证明链上 public input、DA 数据和电路内哈希域之间没有重放或替换空间。

Rollup 状态电路的具体检查面

在 ZK-Rollup 里，最危险的欠约束通常不出现在单个算术 gadget，而出现在多个组件交界处。交易执行电路认为余额已经更新，状态树电路认为叶子已经重算，批次聚合电路认为新状态根已经发布；如果三者之间缺少同一组 account key、storage key、nonce 和 write index 绑定，证明仍可能局部正确、全局错误。审计时要把“组件通过”降级为中间结论，只有跨组件不变量成立，才能认为批次状态转换被证明。

读写表是第一处重点。每次 `SLOAD`、`SSTORE`、余额扣减、手续费扣除、事件日志写入，都应该进入统一的 read-write table，并按交易序号、调用深度、账户、slot 和访问类型排序。若电路只检查表内每一行格式正确，却没有检查同一个 key 的前后值连续性，就可能出现读旧值、写新值、再用另一个旧值继续计算的幽灵状态。对跨链提现消息而言，这会直接影响“消息是否已消费”的判断。

哈希和承诺域是第二处重点。zkEVM 为了降低约束成本，常把执行 trace、状态树路径、日志承诺和 DA commitment 拆成不同子电路。如果子电路之间只传递一个 field element，而没有绑定域标签、批次编号和输入序列，证明者可能把一个子系统中的合法承诺搬到另一个语义位置。安全做法是让每个承诺都包含 domain tag、schema version 和 batch context，而不是只依赖位置约定。

失败交易也是第三处重点。Rollup 执行器会遇到 revert、out-of-gas、签名无效、nonce 错误和账户不存在。电路必须证明失败交易没有产生不该产生的状态写入，同时又正确扣除了应扣费用或记录了回执。如果只证明成功路径，或把失败路径当作“没有输出”的特殊情况，攻击者就可能在边界状态里制造账本和回执不一致。跨链路由依赖回执判断释放或退款，这类不一致会变成用户可见的结算歧义。

审计状态机：从代码 review 到结算前闸门

一个可执行的电路安全流水线可以建模为：

```text spec, zkDSL, compiler IR, constraints, proving key, verifier, on-chain binding ```

每一层都要保留可追溯证据。`spec` 写清状态转换不变量，例如总供应量守恒、账户余额非负、nonce 单调、退出消息只能消费一次。`zkDSL` 层检查赋值和约束是否配对。`compiler IR` 层检查优化器是否删掉了安全相关约束。`constraints` 层做唯一性与覆盖检查。`proving key` 和 `verifier` 层绑定电路版本、public input 顺序和验证合约地址。`on-chain binding` 层确认 proof 只能用于对应批次和对应 Rollup。

最容易被忽略的是版本管理。电路升级不是普通后端发布。只要 public input 顺序、lookup table、range-check 宽度、哈希域、状态叶子编码或 verifier key 改变，旧 proof 的语义就不再等价。生产系统应该把 `circuitId`、`constraintHash`、`verifierKeyHash` 和 `publicInputSchemaVersion` 写入链上可验证上下文。否则审计时看到 proof 通过，也无法确认它通过的是哪个语义版本。

对 Rollup 结算层而言，还需要“失败前置”。如果电路发现异常，正确动作不是在 proof 生成后再依赖人工判断，而是在 batch 提交前阻断状态根传播。高风险批次应进入 quarantine 状态：禁止桥释放、暂停大额提现、允许用户查询但不推进最终结算。这个状态机比事后追回资产可靠得多。

失败模式与检测信号

第一种失败模式是未约束输出。证明者可以改变 amount、recipient、nonce 或 state leaf 的某个分量，同时仍满足其他约束。检测信号包括中间变量只出现在一条约束中、输出没有反向约束、selector 覆盖率异常低。防御是输出唯一性测试、critical signal 白名单和约束覆盖报告。

第二种失败模式是范围检查缺失。有限域元素被错误当成业务整数，导致溢出、别名或符号边界错配。检测信号包括 bit decomposition 只赋值不还原、lookup table 没有覆盖所有 limb、跨字段转换没有上界证明。防御是统一 range-check gadget、limb 宽度审计和字段模数相关测试。

第三种失败模式是状态路径绑定不完整。电路证明某个 Merkle path 有效，但没有证明 path 对应目标账户或目标存储槽。检测信号包括 key、path index、leaf preimage 和 root recomputation 分散在不同组件中，没有共同 public binding。防御是把 account key、storage key、old value、new value、path direction 和 root 放入同一状态转换断言。

第四种失败模式是约束优化器误删或重写。编译器常量折叠、约束简化、unused signal 删除本身是正常优化，但若高层代码依赖 assert 或 witness-only 计算，优化后可能留下语义空洞。防御是保留约束哈希、对 `O0/O1/O2` 生成物做差分检查，并把 IR/constraint artifacts 纳入审计。

第五种失败模式是 verifier/public input 绑定错误。链上合约验证了 proof，却把 public inputs 按错误顺序解码，或没有绑定 batch data commitment。检测信号包括 verifier 合约升级后未更新 schema、多个电路复用同一入口、proof 能在测试网和主网共享上下文。防御是 domain separation、schema hash、chainId、verifier address 和 batch commitment 强绑定。

AllSwap 相关性：跨链路由要关心 proof 语义质量

AllSwap 不是 ZK-Rollup 的电路开发者，但跨链交换会依赖 Rollup 最终性、桥消息、提现证明和退款路径。若某个 Rollup 的状态 proof 存在欠约束风险，路由层看到的“已证明批次”可能并不等于“可安全释放资产”。因此路由风控不应只看费用、延迟和流动性，还应记录证明系统的审计状态、verifier key 版本、最近电路升级、DA 承诺绑定和异常批次处理策略。

一个实际的路由风险模型可以把 ZK 证明质量拆成五项：`constraintCoverageRisk`、`formalVerificationRisk`、`verifierBindingRisk`、`upgradeRisk`、`incidentResponseRisk`。前两项来自电路审计和工具输出，第三项来自链上 verifier 和 public input schema，第四项来自最近是否发生电路或 proving key 升级，第五项来自异常批次是否支持暂停、退款和限额。价格更便宜的路线如果依赖刚升级且未充分审计的电路，并不一定优于稍慢但证明语义稳定的路线。

对用户界面而言，不需要暴露“欠约束变量”这种细节，但应该把状态拆清楚：`batchSubmitted`、`proofGenerated`、`proofVerified`、`withdrawalFinalized`、`refundAvailable` 是不同阶段。尤其在跨链场景里，证明通过之前不应把目标链释放描述成确定结果；电路或 verifier 异常时，应优先保证退款归因和资产状态可解释。

当证明质量信号降级时，路由器可以采用分层处置，而不是简单下线整条路径。小额、低风险资产可以降低限额并延长确认窗口；大额交易可以切换到审计状态更稳定的结算路径；已经进入执行中的订单应优先保留退款和状态查询能力。这样做的目的不是替 Rollup 做安全背书，而是避免把 proof 语义风险直接转嫁给用户。

未解决问题

第一，电路语义规格仍缺少行业统一格式。审计报告可以描述风险，但机器很难比较两个 Rollup 的约束覆盖率和 public input 绑定质量。

第二，形式化工具存在规模瓶颈。SMT、符号执行和代数求解可以发现深层问题，但面对 zkEVM 级别的巨型电路，如何分片证明安全性质仍是工程难题。

第三，编译器可信边界没有完全解决。zkDSL、IR、constraint simplification 和 proving key 之间的语义保持需要可复现构建和 artifact hash，而很多项目仍把它当作内部发布细节。

第四，跨链系统缺少证明质量的实时信号。路由器能看到交易延迟和失败率，却很难直接观察电路是否刚刚变更、某个批次是否绕过常规证明路径。

第五，用户可理解性仍然困难。好的产品不应把电路术语推给用户，但必须把等待原因、退款状态、结算风险和异常暂停解释清楚。

参考资料

[1] Circom Documentation, Constraint Generation, https://docs.circom.io/circom-language/constraint-generation/

[2] Circom Documentation, Signals, https://docs.circom.io/circom-language/signals/

[3] Circom Documentation, Constraint Simplification, https://docs.circom.io/circom-language/circom-insight/simplification/

[4] Zcash Halo2 Book, PLONKish Arithmetization, https://zcash.github.io/halo2/concepts/arithmetization.html

[5] Zcash Halo2 Book, Tips and Tricks, https://zcash.github.io/halo2/user/tips-and-tricks.html

[6] Ariel Gabizon, Zachary J. Williamson, Oana Ciobotaru, PLONK, IACR ePrint 2019/953, https://eprint.iacr.org/2019/953

[7] Shankara Pailoor et al., Automated Detection of Underconstrained Circuits in Zero-Knowledge Proofs, IACR ePrint 2023/512, https://eprint.iacr.org/2023/512

[8] Hongbo Wen et al., Practical Security Analysis of Zero-Knowledge Proof Circuits, USENIX Security 2024, https://www.usenix.org/conference/usenixsecurity24/presentation/wen

[9] Trail of Bits, Circomspect Static Analyzer, https://github.com/trailofbits/circomspect

[10] Trail of Bits, Circomspect Analysis Passes, https://github.com/trailofbits/circomspect/blob/main/doc/analysis_passes.md

[11] Leonardo de Moura and Nikolaj Bjørner, Z3: An Efficient SMT Solver, Microsoft Research, https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/

[12] Hideaki Takahashi et al., zkFuzz: Foundation and Framework for Effective Fuzzing of Zero-Knowledge Circuits, arXiv 2025, https://arxiv.org/abs/2504.11961