Writing and Auditing ZK Circuits — Petr Korolev | OXORIO
三句話摘要
ZK 電路安全審計的核心攻擊向量與防禦實踐，以 Privacy Pools 真實案例說明如何被利用。 ZK 電路中「賦值」與「約束」的一字之差，就是讓整個 Soundness 崩潰的致命差異，審計時每個訊號的約束完整性都必須逐一手動驗證。 1. 未約束電路（Under-Constrained Circuits）是 ZK 最常見且最危險的漏洞
重點整理
重點- 1
1. 未約束電路（Under-Constrained Circuits）是 ZK 最常見且最危險的漏洞
- 2
Circom 中 `<--` 只做賦值、不做驗證，`<==` 才同時賦值並加入約束。開發者若混用，Prover 可生成「語法合法但語意無效」的證明，讓協議完全失去 Soundness 保證。
- 3
2. 算術溢位必須手動對照橢圓曲線的 Prime 上界
- 4
ZK 電路沒有內建溢位保護，必須明確確認所有訊號不超過所用曲線的 Field 大小（如 BN254）。2019 年的漏洞曾同時影響 Mixim、Zokrates、Snarkjs 等主流函式庫，允許雙重花費。
- 5
3. 編譯器優化會靜默刪除「未用到」的輸入訊號
- 6
若某輸入訊號未在電路計算中使用，Circom 編譯器會直接移除，導致鏈上合約無法綁定該輸入，任何人可帶入任意值生成有效證明。解法是加入人工計算（如信號自乘並加約束）強迫編譯器保留。
- 7
4. 不要自行修改底層密碼學函式庫
- 8
Privacy Pools 案例中，團隊 Fork 了 `num2bits` 並加入自定義邏輯，卻在迴圈內以 `<--` 而非 `<==` 賦值，導致攻擊者可篡改 `isamToBits` 回傳值，進而控制交易類型（存款 vs 提款），影響協議大量資金。
實用技巧與重點
乾貨- 具體數字與參數
- BN254 橢圓曲線 Field 大小 vs Solidity 的 256-bit，差距可被利用做溢位攻擊
- Privacy Pools 的 `isamToBits` 關鍵比較值：240（存款/提款分界）
- Circom 2.0 的 proof 生成速度相比舊版提升約 10~100 倍
- 漏洞名稱與案例
- Frozen Heart Vulnerability（PLONK 協議，Trail of Bits 發現，Defcon 日本有完整演講）
- Tornado Cash 信任設定洩漏事件（2019）
- 2019 年橢圓曲線溢位漏洞：同時影響 Mixim、Zokrates、Snarkjs、Nargs
- Privacy Pools 嚴重漏洞（Aario 審計，已修復，報告公開於 GitHub）
- 工具與資源
- Circom（電路語言）
- Groth16（最主流生產環境 Proving System）
- PLONK、Halo（新興 Proving System，尚未經充分安全審計）
- zkSecurity（zksecurity.xyz，Trail of Bits 出品，含壞範例與建議）
- Trail of Bits 靜態分析工具（Static Analyzer）
- 模糊測試（Fuzzing Framework）用於 ZK 電路
- 操作流程
- 防止非法輸入：用 `num2bits` 轉成 bit 陣列 → 確認正數範圍 → 確認不超過 Field 上界 → 用 `IsZero` 確認值不等於 1
- 防止編譯器優化刪除訊號：加入 `signal * signal → 加 constraint` 人工佔位
- 信任設定（Trusted Setup）：多方計算（MPC），參與方越多越安全；所有毒廢料（Toxic Waste）必須被銷毀
結論
結論“ZK 電路中「賦值」與「約束」的一字之差，就是讓整個 Soundness 崩潰的致命差異，審計時每個訊號的約束完整性都必須逐一手動驗證。”
完整解析
詳細ZK-SNARK 的開發棧層次複雜，從橢圓曲線密碼學、Proving System（Groth16、PLONK、Halo），到最上層的電路語言（如 Circom），每一層的設計缺陷都會滲透到下一層。Peter 在本次演講中聚焦電路層，說明為什麼 ZK 電路的安全審計與傳統 Solidity 審計根本不同，並以真實漏洞與 Aario 最新審計案例示範具體攻擊路徑。
最核心的問題是「訊號賦值」與「訊號約束」的混淆。Circom 中 `<--` 只是把右側值寫入訊號，不產生任何數學約束；`<==` 才同時賦值並產生約束。若開發者在應該用 `<==` 的地方寫了 `<--`，電路的 Soundness 就被打穿——Prover 可以提交任意數值，只要讓最終輸出看起來符合約束，系統就會接受，即使中間過程完全是偽造的。類似的問題出現在輸出端：若未明確約束輸出值，對方可以讓輸出保持未定義狀態，使整份證明不再代表任何有意義的計算。這類「未約束電路」漏洞在每次 ZK 審計中幾乎都會出現，類比 Solidity 中的重入攻擊一樣普遍。
算術溢位在 ZK 電路中比一般程式更為危險，因為電路工作在有限域（Finite Field）內，負數不存在，所有數值都以模 Prime 表示。2019 年，研究員 Roman Simonov 發現一個橢圓曲線溢位漏洞，允許攻擊者輸入超過 Field 上界的數值觸發環繞效應，實現雙重花費。這個漏洞同時存在於 Mixim、Zokrates、Snarkjs、Nargs 等當時幾乎所有主流 ZK 函式庫，充分說明 ZK 生態系整體仍處於早期階段，即便是廣泛使用的框架也需要持續安全驗證。
Aario 最新的 Privacy Pools 審計案例將上述問題融合呈現。Privacy Pools 是 Tornado Cash 的合規升級版（用戶可生成「我不在黑名單集合中」的 ZK 證明），團隊技術實力強，但仍在電路實作中犯了幾個致命錯誤。他們 Fork 了官方 `num2bits` 函式並加入自定義邏輯，在迴圈內以 `<--` 進行 bit 分解賦值，而非 `<==`。後雖加入二進位檢查與最終約束，但中間的 bit 陣列實際上未被充分約束。攻擊者可以在不違反任何約束的前提下，插入特殊構造的訊號值，令 `isamToBits` 回傳非預期結果。由於協議以該回傳值與閾值 240 比較來決定操作類型（存款或提款），攻擊者可藉此篡改操作類型，對協議資金造成重大損失。所有漏洞現已修復，完整報告公開於 Aario 的 GitHub。
Peter 最後建議開發者：使用靜態分析工具與模糊測試、絕對不要修改底層密碼學函式庫、謹慎評估尚未接受生產環境安全審計的新 Proving System（如部分 folding schemes 與 pairing-based 系統），並持續關注 ZK 社群論壇，因為攻擊向量與工具鏈每月都在演進。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
