本篇將從一個簡單的除法證明問題出發，從工程實務的角度帶你走近 ZK 的世界線。
作者：Certik
原文標題：技術詳解| Divide and Conquer：ZK 除法中隱藏的漏洞
封面： Photo by Nicolas Arnold on Unsplash
ZK 的崛起與演變
曾幾何時，零知識證明（以下簡稱 ZK）仍被認為是密碼學教科書中的理論概念，至少在傳統安全研究中很少被主流社群深入探索。然而在 Web3.0 領域，區塊鏈技術的迅速發展，用短短幾年時間實現了 ZK 從理論到實踐的跨越式進展，一路蓬勃，高歌猛進。
1985 年誕生，2014 年 ZCash 才用 SNARKs 證明了 ZK 不僅是書本上的傳說，也是實打實的 “江湖絕學”，2019 年開始，隨著 zkSync 和 Polygon 的崛起，ZK 從隱私保護的小眾技術，搖身一變成了區塊鏈擴展性問題的關鍵。到了 2022 年，Tornado Cash 轟然倒下，美國財政部的製裁引發了一場關於隱私與自由的廣泛討論，也讓 ZK 成為了茶餘飯後的熱門話題。 2023 年起，隨著 PLONK、Halo2 等新型 ZK 協定的成熟，ZK 技術在區塊鏈領域高速發展，成為 Web3.0 的新寵。
ZK 的崛起不僅是因為它在區塊鏈世界中的廣泛應用，也與這些年來不斷創新的開發工具密不可分。儘管這些工具的核心目標都是將程式碼邏輯電路化，但幾年間，從最初合約級應用的 Circom，到鏈上層為性能優化推出的 EVM 兼容或等價的 zkVM，更新速度之快令人目不暇接，甚至連應用生態腳步都還沒穩住，下一次升級迭代已呼嘯而至。
ZK 原理概述
想理解 ZK，可以從其共通性的漏洞入手。在傳統安全裡有個經驗：直接分析程式碼邏輯來理清全局往往難度極大，有時不如跑個 crash 看 dump 來得直觀，也就是透過漏洞回溯程式碼的方式去理解內在邏輯。
初識 ZK，可能會被各種專有名詞包圍— SNARK、STARK、PLONK、QAP、R1CS、Groth16。這些名詞乍聽也能理解，一旦深入探究，就會發現背後需要紮實的數學功底。所以，很多介紹 ZK 的內容，要嘛是光彩奪目的概念科普，要嘛是晦澀難懂的協議分析，彷彿置身於一片高深莫測的領域。今天這篇文章，希望能帶給你不同的體驗。我們將從一個簡單的除法證明問題出發，從工程實務的角度帶你走近 ZK 的世界線。
在我們討論後續問題之前，我們先用一個實踐向的直覺視角來解釋 ZK，以便後續討論時有一個共同的基礎。在智慧合約和區塊鏈中應用 ZK 技術解決的核心問題是如何在不揭露答案本身的情況下，證明自己知道這個正確的答案，例如一個多項式方程式的解。越過原理，只想說目前有成熟方法能夠實現這個目標：首先，將一個複雜的問題通過多個僅涉及乘法和加法的簡單問題加以描述；然後，將這些簡單問題轉換為矩陣和代表正解的 witness 相乘的形式；接下來，將矩陣轉換為 verification-key；同時，witness 則進一步轉換為 proof。
簡而言之：一個複雜問題被轉化為一組特定的 key，而答案被分解為多個 witness，最終演變為 proof；proof 能夠用 verification-key 以固定的演算法驗證。一方面驗證成功說明產生 proof 的人確實知道問題的正確答案，另一方面透過 proof 卻無法反推出原解，保護了隱私。這個驗證過程可以用於提款的同時不暴露存款憑證；也可以用來證明一個 transaction 引發的合約程式碼執行結果的真實性，進而用短 proof 取代多人執行 transaction 造成的資源消耗。
約束挑戰
由於 ZK 所有相關計算都在橢圓曲線上進行，因此只有加法和乘法是直接定義的。要證明一個複雜問題，必須將其拆解成包含這些基本運算的簡單子問題，即電路化。電路化的過程也是目前出問題最多的地方。
拆分出來的簡單的子問題被稱為 “約束”，它們聯立後必須與原始複雜問題等效。如果某個約束缺失，可能導致建構出符合所有約束但不是正確答案的 witness，從而偽造證明。這些偽造的證明仍然能夠通過 verification-key 的檢查，帶來一系列嚴重後果：如合約層級的雙重支付、或 zkVM 層級的修改計算中間結果等。另一方面，若約束過於嚴格，超出了原問題的需求，則可能導致無法找到合適的 witness，進而導致交易無法被證明，造成鍊級別的拒絕服務攻擊或合約應用的功能失效。第一種利用欠約束偽造證明看起來更有趣，它相當於直接控制了執行過程，類比於傳統安全漏洞利用時的控 PC 指標。
除法的案例分析
下面就來看一個簡單的除法問題在 ZK 的脈絡下該怎麼約束，又能惹出多少亂子。
設想如下場景，zkVM 在運行時，執行了一個 a 除以 b 的運算，並且我們要證明商數是 q，餘數是 r。在這裡，a、b、q、r 都是 witness，我們需要確保它們符合除法的限制。假設 a 和 b 已經由前序執行過程約束決定，我們只關注 q 和 r 的限制。直覺上，既然 a=b*q+r 是除法的乘法表達式，是不是一個約束多項式就夠用了呢？絕對不是！在實際的工程實作中，情況要複雜得多。例如，zkSync 曾經的除法驗證過程涉及的程式碼如下：
首先 a（src0_view）和 b（src1_view）透過 allocate_div_result_unchecked 計算出 q 和 r，這部分只是算數運算，先驗地根據 a 和 b 求出作為 witness 的 q 和 r，不涉及約束。
出於最佳化考慮，zkSync 將乘法和除法放在同一個函數裡進行約束，所以接下來是根據乘或除，透過帶有約束的選擇器取出要約束的變量，即 r、q、b、a，並增加乘法約束 MulDivRelation，也就是要求 a=b*q+r。
MulDivRelation 的乘法約束在指令循環即將結束前才由 enforce_mul_relation 函數施加。然而，由於 zkSync 選擇了 Goldilock 域（域階為 0xffffffff00000001），這個域空間並不足以表示所有的 uint64 類型資料。因此，uint256 需要分解成八個 uint32 來記錄。為了處理這部分的乘法，系統採用了逐輪計算的方式，每一輪通過fma_with_carry門對兩個 uint32 執行乘法約束。
乘法結束時，先用一次enforce_equal門約束計算結果沒有進位，再用一次保證乘加的累積結果和 a 相等。第二個enforce_equal的目的很容易理解，也就是用來滿足我們先前重複提及的 a=b*q+r。
第一個沒有進位的限制確保了商 q 和餘數 r 的值不會超出預期的範圍，避免了計算結果出現溢位。除了進位檢查，另一個常用方法是約束位元長度（透過限製商和餘數位元數，確保計算的結果符合預期的範圍）。 zkSync 記得帶了這個約束，但其實這是個很容易被忽略的細節，像是 renegade 專案計算 fee 相關用到的除法就漏掉過這個約束：
再例如 Circom 中的大整數求模庫函數Bigmod也曾出現過類似的漏洞。具體來說，Bigmod函數在實作過程中，只檢查了商 q 的位元長度，而忽略了對餘數 r 的長度偵測：
之所以要有這個約束，是因為有限域內的溢出會讓結果回滾仍落入域內，使得 q 和 r 不唯一。例如給定一個新的 r'=rk，總是能透過 q'=(ar')*b^(-1) 計算得到一個滿足條件的 q'使攻擊者修改除法計算結果。對於日常使用的 a 和 b，這樣修改 r 通常會導致一個非常大的 q。
在 zkSync 的程式碼中，乘法約束的設定只是第一步。接下來，它要比較 r 和 b（除數），確保 r<b。具體來說，allocate_subtraction_result_unchecked執行了這個比較操作，它所做的只是計算 rb，並將結果存入變數subtraction_result_unchecked和remainder_is_less_than_divisor。其中remainder_is_less_than_divisor記錄了長減法是否發生了借位。借位了則表示 r<b，這是我們期望看到的情況（由conditionally_enforce_true限制保證正確性）。之後 b、rb ( subtraction_result_unchecked )、r、of ( r emainder_is_less_than_divisor ) 會被放入 AddSubRelation。
在指令循環結束前，透過enforce_addition_relation函數施加UIntXAddGate加法門約束。確保 (rb)+b=r+of*2^256，其中 of 代表的是加法過程中產生的進位。這個限制的邏輯在於，rb 的結果應該是負數，域內表現為一個非常大的正數。為了讓這個結果能被正確表示，rb 與 b 相加時，必然會超過 2^256 導致進位，使得remainder_is_less_than_divisor的約束得以滿足：
這麼一套約束的目的是避免攻擊者透過構造另一組商 q'和余數 r'來繞過除法約束，進而偽造計算結果。例如我們設定新的 q'=qk 和 r'=r+b*k，很容易就找到了一組也符合乘法關係的 witness 竄改計算結果。這個約束在實際程式碼中也很容易被忽略。例如，Polygon 專案就曾經在程式碼中誤加了過於寬鬆的 r<a 約束：
在 zkSync 的除法計算過程中，表面上似乎所有必要的約束都已經施加，但程式碼實作上仍然存在漏洞。這個漏洞和 zkSync 的程式碼設計相關，之前提到，uint256 類型的資料是透過八個 uint32 表示的，而每個 uint32 背後實際上是 variable 類型，它代表的是 Goldilock 域中的元素。因此，每個 variable 實際上最大可以表示 0xffffffff00000000。
如果希望 uint32 中的 variable 僅表示 32 位元整數，則必須為每個 uint32 額外施加位元長度約束，以確保其數值範圍受限。但在allocate_subtraction_result_unchecked函數中，並沒有對計算結果subt raction_result_unchecked中的每個 uint32 施加這種位元長度約束。這意味著，雖然subtraction_result_unchecked被定義為[uint32; 8]，但其中每個 uint32 實際上表示的最大值是 0xffffffff00000000，而不是期望的 32 位元限制。
因此，如果把subtraction_result_unchecked中最後一個 uint32 的第 32 位元篡改為 1，則後面加法閘的計算過程中必然會有進位，使得remainder_is_less_than_divisor約束天然滿足。之後令 r'=r+b*k 和 q'=qk 就可以產生同樣合法的 q 和 r 的組合了。
總結
透過探討除法約束在工程實作中一些 tricky 的細節，我們初步感受了一下 ZK 世界的複雜與精妙。每個細節都可能隱藏著影響整個系統安全性的潛在風險，也正是這些細微之處構成了 ZK 證明技術的核心，推動了其在區塊鏈領域的廣泛應用。在未來的篇章裡，CertiK 將繼續深入 ZK 的技術細節，敬請期待。
免責聲明：作為區塊鏈資訊平台，本站所發布文章僅代表作者及來賓個人觀點，與 Web3Caff 立場無關。文章內的資訊僅供參考，均不構成任何投資建議及要約，並請您遵守所在國家或地區的相關法律法規。
