技術詳解 | Divide and Conquer：ZK除法中隱藏的漏洞

2024-09-11 16:09:35

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=(a-r使攻擊者修改除法計算結果。對於日常使用的 a 和 b ，這樣修改 r 通常會導致一個非常大的 q 。

在zkSync的代碼中，乘法約束的設置只是第一步。接下來，它要比較 r 和 b （除數），確保r allocate_subtraction_result_unchecked 執行了這一比較操作，它做的只是計算出r-b，並將結果存入變量 subtraction_result_unchecked 和 remainder_is_less_than_divisor 。其中 remainder_is_less_than_divisor 記錄了長減法是否發生了借位。借位了則意味着r conditionally_enforce_true 約束保證正確性）。之後 b 、r-b ( subtraction_result_unchecked )、 r 、 of ( r emainder_is_less_than_divisor )會被放入 AddSubRelation 。

在指令循環結束前，通過 enforce_addition_relation 函數施加 UIntXAddGate 加法門約束。確保(r-b)+b=r+of*2^256，其中 of 代表的是加法過程中產生的進位。這個約束的邏輯在於，r-b的結果應該為負數，域內表現為一個非常大的正數。為了讓這個結果能夠被正確表示，r-b與 b 相加時，必然會超過2^256導致進位，使得 remainder_is_less_than_divisor 的約束得以滿足：

這么一套約束的目的是避免攻擊者通過構造另一組商 q 來繞過除法約束，進而僞造計算結果。比如我們設定新的q=r+b*k，很容易就找到了一組也符合乘法關系的witness篡改計算結果。這個約束在實際代碼中也很容易被忽略。例如，Polygon項目就曾經在代碼中誤加了過於寬松的r

在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=q-k就可以產生同樣合法的 q 和 r 的組合了。