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