Unconstrained Machines
三句話摘要
ZISK ZKVM 安全審計：架構模組化設計帶來的安全優勢與三個關鍵漏洞揭露。 ZKVM 的模組化電路設計天然契合安全審計需求，但 under-constrained 類漏洞無法靠測試發現，必須將 SAT solving 或形式化驗證納入標準審計流程。 模組化架構同時提升效能與安全性：ZISK 將 ROM、記憶體、暫存器、範圍檢查、執行邏輯各自拆成獨立電路，每個元件可並行證明以降低延遲，同時每個元件介面清晰，安全審計時可單獨換入換出測試。
重點整理
重點- 1
模組化架構同時提升效能與安全性：ZISK 將 ROM、記憶體、暫存器、範圍檢查、執行邏輯各自拆成獨立電路，每個元件可並行證明以降低延遲，同時每個元件介面清晰，安全審計時可單獨換入換出測試。
- 2
邏輯錯誤因 transpiler 未使用問題 opcode 而未被發現：LEQ 高位元缺失與 32/64-bit 不一致問題，在原始 RISC 轉 ZISK 的 transpiler 中因未觸及相關 opcode 而躲過測試，顯示測試套件對路徑覆蓋的盲區。
- 3
Under-constrained 錯誤最難偵測，需形式化方法輔助：初始進位旗標未受約束，允許攻擊者翻轉 0/1，造成 off-by-one 錯誤。這類問題無法靠傳統測試找到，必須透過直接推理、SAT solving 或形式化驗證工具。
- 4
ZKVM 是形式化驗證真正有價值的應用場域：講者過去曾對 DeFi 合約使用形式化驗證持懷疑態度，但認為 ZKVM 的嚴謹數學結構才是形式化方法能發揮效用的地方。
實用技巧與重點
乾貨- 平台：ZISK ZKVM、相容 64-bit RISC-V
- 優化目標：低延遲、real-time 並行 ZK 證明
- 元件列表：ROM circuit、Memory circuit、Register circuit、Range check circuit、Execution circuit
- 漏洞一：LEQ（less than or equal）opcode — 僅檢查最高位元，相等時未繼續檢查次高位元，修復方案：加入 carry-over 機制
- 漏洞二：32-bit opcode 在 64-bit 機器上的高位元定義（bit 3 vs bit 7）在系統兩處不一致，引發多個相關錯誤
- 漏洞三：`has_initial_carry` 旗標未被約束（unconstrained），允許進位初始值任意翻轉，造成 off-by-one 錯誤；存在 factor-of-2 的細節但仍可被利用
- 工具：Z3 SAT solver — 成功重現已知漏洞，並額外發現一個回歸錯誤（regression bug）
- 偵測方式對比：邏輯錯誤 → 測試套件可偵測；under-constrained → 需 direct reasoning / SAT solving / 形式化驗證
結論
結論“ZKVM 的模組化電路設計天然契合安全審計需求，但 under-constrained 類漏洞無法靠測試發現，必須將 SAT solving 或形式化驗證納入標準審計流程。”
完整解析
詳細ZISK 是一個與 64-bit RISC-V 指令集相容的 ZKVM（零知識虛擬機），其核心設計目標是低延遲的實時 ZK 證明。它將整個虛擬機的執行流程拆解為多個獨立元件：負責確保每條指令合法預載的 ROM 電路、確保記憶體讀寫一致性與地址對齊的 Memory 電路、追蹤暫存器最新狀態的 Register 電路、負責時間戳範圍驗證的 Range check 電路，以及確保指令執行正確性的 Execution 電路。每個元件可獨立並行生成證明，這是實現低延遲的關鍵。值得注意的是，這種模組化設計在安全審計上也帶來額外紅利：每個元件介面清晰，審計人員可以單獨替換與測試，大幅降低了複雜系統的審計難度。
本次安全審計共發現三個漏洞。第一個是 LEQ（小於等於）opcode 的邏輯錯誤：ZISK 採用逐位元組二進位查找表來驗證 XOR 或比較運算（因為 prover 可以自行選擇所有輸入值，必須確保一致性），但 LEQ 的實作只檢查最高位元，在兩個值相等時未繼續比對次高位元，導致驗證不完整。修復方案是加入 carry-over 機制處理相等情況。第二個漏洞涉及 32-bit opcode 在 64-bit 機器上的「高位元」定義問題：究竟是第 3 個位元組還是第 7 個位元組算高位元，只要系統內部一致即可，但系統兩個不同部分的定義不一致，引發了多個衍生錯誤。
第三個也是最具挑戰性的漏洞，屬於 under-constrained 問題：`has_initial_carry` 旗標控制加法運算的初始進位值（某些運算應從 1 開始，某些從 0 開始），但這個旗標在系統中未被正式約束，意味著攻擊者可以任意將初始進位的 0 翻成 1 或 1 翻成 0，造成 off-by-one 錯誤。即使存在 factor-of-2 的額外複雜度，漏洞仍然可被利用。這類 under-constrained 錯誤與前兩個邏輯錯誤最大的區別在於偵測難度：前兩個因為 RISC→ZISK transpiler 未觸及這些 opcode，測試套件完全沒有覆蓋到，最終在實際使用中並未造成問題，但理論上可透過完整的測試套件發現；而 under-constrained 問題本質上必須靠直接形式化推理、SAT solving 或專用工具才能找出。
在工具實驗方面，審計團隊使用 Z3 SAT solver 進行輔助分析，不僅成功重現了已發現的漏洞，還意外找到一個回歸錯誤。講者認為 ZKVM 這類系統由於有嚴謹的數學結構，正是形式化驗證真正能發揮效益的場域，與他四年前對 DeFi 合約使用形式化驗證的懷疑態度形成對比，並期待 ZISK 未來能全面引入正式驗證流程。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
