深入剖析兩個ZK漏洞

在先前的文章中，我們討論了零知識證明的先進形式化驗證：如何驗證一條ZK指令。透過形式化驗證每條zkWasm指令，我們能夠完全驗證整個zkWasm電路的技術安全性和正確性。在本文中，我們將專注於發現漏洞的視角，分析在審計和驗證過程中發現的具體漏洞，以及從中得到的經驗和教訓。如要了解有關零知識證明（ZKP）區塊鏈的先進形式化驗證的一般討論，請參見零知識證明區塊鏈的先進形式化驗證一文。

在討論ZK漏洞之前，讓我們先來了解CertiK是如何進行ZK形式化驗證的。對於像ZK虛擬機器（zkVM）這樣的複雜系統，形式化驗證（FV）的第一步是明確需要驗證的內容及其性質。這需要對ZK系統的設計、程式碼實現和測試設定進行全面的審查。這個過程與常規的審計有所重疊，但不同之處在於，審查後需要確立驗證的目標和性質。在CertiK，我們稱之為面向驗證的審計。審計和驗證工作通常是一個整體。對於zkWasm，我們對其同時進行了審計和形式化驗證。

什麼是ZK漏洞？

零知識證明系統的核心特徵在於允許將離線或私密執行的計算（例如區塊鏈交易）的簡短加密證明傳遞給零知識證明驗證器，並由其檢查和確認，以確信該計算確已按聲明的情況發生過。就此而言，ZK漏洞將使得駭客可以提交用於證明虛假交易的偽造ZK證明，並讓ZK證明檢查器接受。

對於zkVM的證明器而言，ZK證明過程涉及運行程式、產生每一步的執行記錄，並將執行記錄的資料轉換成一組數字表格（該過程稱為「算術化」）。這些數字之間必須滿足一組約束（即「電路」），其中包括了具體表單元格之間的聯繫方程式、固定的常數、表間的資料庫查找約束，以及每對相鄰表行間所需滿足的多項式方程式（亦即“門”）。鏈上驗證可以由此確認的確存在某張能滿足所有限制的表，同時又保證不會看到表中的具體數字。

 zkWasm算術化表

每一個約束的準確性至關重要。任何約束中的一個錯誤，無論是偏弱或缺失，都可能使得駭客能夠提交一個誤導性的證明，這些表格看似代表了智能合約的一次有效運行，但實際上並非如此。與傳統VM相比，zkVM交易的不透明性放大了這些漏洞。在非ZK鏈中，交易的計算細節是公開記錄在區塊之上的；而zkVM則不將這些細節儲存於鏈上。透明度的缺失使得攻擊的具體情況很難被確定，甚至連攻擊是否已發生都很難確定。

執行zkVM指令規則的ZK電路極為複雜。對於zkWasm來說，其ZK電路的實現涉及超過6,000行的Rust程式碼和數百個約束條件。這種複雜性通常意味著可能存在多個漏洞正等待被發現。

 zkWasm電路架構

的確，我們透過對於zkWasm審計和形式化驗證發現了多個這樣的漏洞。下面，我們將討論兩個代表性的例子，並討論它們之間的差異。

程式碼漏洞：Load8資料注入攻擊

第一個漏洞涉及zkWasm的Load8指令。在zkWasm中，堆記憶體的讀取是透過一組LoadN指令來完成的，其中N是要載入的資料的大小。例如，Load64應該從zkWasm記憶體位址讀出64位元的資料。 Load8應該從記憶體中讀出8位元的資料（即一個位元組），並用0前綴填充以創建一個64位元的值。 zkWasm內部將記憶體表示為64位元組的數組，因此其需要「選取」記憶體數組的一部分。為此使用了四個中間變數（u16_cells），這些變數合起來構成了完整的64位元載入值。

這些LoadN指令的約束定義如下：

這個約束分為Load32、Load16和Load8這三種情況。 Load64沒有任何約束，因為記憶體單元剛好就是64位元的。對於Load32的情況，程式碼確保了記憶體單元中的高4個位元組（32位元）必須為零。

對於Load16的情況，記憶體單元中的高6個位元組（48位元）必須為零。

對於Load8的情況，應該要求記憶體單元中的高7個位元組（56位元）為零。遺憾的是，在程式碼中並非如此。

如你所見，只有高9至16位被限制為零。其他的高48位元可以是任意值，卻仍然可以偽裝成「從記憶體中讀取的」。

透過利用這個漏洞，駭客可以篡改一個合法執行序列的ZK證明，使得Load8指令的運行加載這些意外的字節，從而導致資料損壞。並且，透過精心安排週邊的程式碼和數據，可能會觸發虛假的運作和轉賬，從而竊取數據和資產。這種偽造的交易可以透過zkWasm檢查器的檢查，並被區塊鏈錯誤地認定為真實交易。

修復這個漏洞其實相當簡單。

這個漏洞代表了一類被稱為「程式碼漏洞」的ZK漏洞，因為它們源自於程式碼的編寫，並且可以透過較小的局部程式碼修改來輕鬆修復。正如你可能會同意的那樣，這些漏洞也相對更容易被人看出來。

設計漏洞：偽造返回攻擊

讓我們來看看另一個漏洞，這次是關於zkWasm的呼叫和返回。呼叫和返回是基本的VM指令，它們允許一個運行的上下文（例如函數）去呼叫另一個，並在被呼叫者完成其執行後，恢復呼叫者上下文的執行。每次呼叫都預期稍後會回傳一次。 zkWasm在調用和返回的生命週期中所追蹤的動態資料被稱為「調用幀（call frame）」。由於zkWasm會依序執行指令，所有呼叫訊框可以根據其在運行過程中的發生時間進行排序。下面是一個在zkWasm上運行的呼叫/返回程式碼範例。

用戶可以呼叫buy_token()函數來購買代幣（可能是透過支付或轉移其他有價值的東西）。它的核心步驟之一是透過呼叫add_token()函數，實際將代幣帳戶餘額增加1。由於ZK證明器本身並不支援呼叫幀資料結構，因此需要使用執行表（E-Table）和跳躍表（J-Table）來記錄和追蹤這些呼叫幀的完整歷史記錄。

上圖說明了buy_token()呼叫add_token()的運行過程，以及從add_token()回到buy_token()的過程。可以看到，代幣帳戶餘額增加了1。在執行表中，每個運行步驟佔一行，其中包括目前執行中的呼叫訊框編號、目前上下文函數名稱（僅用於此處的說明）、該函數內目前運行指令的編號，以及表中所存的當前指令（僅用於此處的說明）。在跳轉表中，每個呼叫幀佔一行，表中存有其呼叫者幀的編號、呼叫者函數上下文名稱（僅用於此處的說明）、呼叫者幀的下一指令位置（以便該幀可以返回）。在這兩個表中，都有一個jops列，它追蹤當前指令是否為呼叫/返回（在執行表）以及該幀（在跳轉表）發生的呼叫/返回指令總數。

正如人們所預期的，每次調用都應該有一次相應的返回，並且每個幀應該只有一次調用和一次返回。如上圖所示，跳轉表中第1幀的jops值為2，與執行表中的第1行和第3行相對應，那裡的jops值為1。目前看起來一切正常。

但實際上這裡有一個問題：儘管一次呼叫和一次返回將使幀的jops計數為2，但兩次調用或兩次返回也會使計數為2。每個畫面有兩次呼叫或兩次返回聽起來可能很荒謬，但要牢記的是，這正是駭客試圖透過打破預期要做的事情。

你現在可能有點興奮了，但我們真的找到問題了嗎？

結果表明，兩次調用並不是問題，因為執行表和調用表的約束使得兩個調用無法被編碼到同一幀的行中，因為每次調用都會產生一個新的幀編號，即當前調用幀編號加1。

而兩次返回的情況就沒那麼幸運了：由於在返回時不會創建新的幀，駭客確實有可能獲取合法運行序列的執行表和調用表，並註入偽造的返回（以及相應的幀）。例如，先前執行表和呼叫表中buy_token()呼叫add_token()的範例可以被駭客竄改為下列情況：

駭客在執行表中原來的呼叫和返回之間注入了兩次偽造的返回，並在呼叫表中增加了一個新的偽造的幀行（原來的返回和後續指令的運行步驟編號在執行表中則需要加4）。由於呼叫表中每一行的jops計數均為2，因此滿足了約束條件，zkWasm證明檢查器將接受這個偽造的執行序列的「證明」。從圖中可以看出，代幣帳戶餘額增加了3次而不是1次。因此，駭客能夠以支付1個代幣的價格獲得3個代幣。

解決這個問題有多種方法。一個明顯的方法是分別單獨追蹤呼叫和返回，並確保每一幀恰好有一次呼叫和一次返回。

你可能已經注意到，到目前為止我們尚未展示這個漏洞的哪怕一行程式碼。主流的原因是沒有任何一行程式碼是有問題的，程式碼實作完全符合表格和約束設計。問題在於設計本身，而修復方法也是。

你可能認為，這個漏洞應該是顯而易見的，但實際上並非如此。這是因為「兩次呼叫或兩次返回也會導致jops計數為2」與「實際上兩次返回是可能的」之間存在空白。後者需要對執行表和呼叫表中相關的各種限制進行詳細、完整地分析，很難進行完整的非形式化推理。

兩個漏洞的比較

對於“Load8資料注入漏洞”和“偽造返回漏洞”，它們都可能導致駭客能夠操縱ZK證明、創建虛假交易、欺騙證明檢查器，並進行竊取或劫持。但他們的性質和被發現的方式卻截然不同。

「Load8資料注入漏洞」是在對zkWasm進行審計時發現的。這絕非易事，因為我們必須審查超過6,000行的Rust程式碼和上百條zkWasm指令的數百個約束。儘管如此，這個漏洞還是相對容易發現和確認的。由於這個漏洞在形式化驗證開始之前就已被修復，所以在驗證過程中並未遇到它。如果在審​​計過程中未發現漏洞，我們可以預期在Load8指令的驗證中會發現它。

「偽造返回漏洞」是在審計之後的形式化驗證中發現的。我們在審計中未能發現它的部分原因在於，zkWasm中有一個同jops非常相似的機制叫做“mops”，其在zkWasm運行期間追踪每個內存單元歷史數據對應的內存訪問指令。 mops的計數約束確實是正確的，因為其只追蹤了一種類型的記憶體指令，即記憶體寫入；而且每個記憶體單元的歷史資料都是不可變的，並且只會寫入一次（mops計數為1）。但即使我們在審計期間注意到了這個潛在的漏洞，如果不對所有的相關約束進行嚴格的形式化推理，我們將仍然無法輕易地確認或排除每一種可能情況，因為實際上沒有任何一行程式碼是錯誤的。

總結來說，這兩個漏洞分別屬於「程式碼漏洞」和「設計漏洞」。程式碼漏洞相對較為淺顯，更容易被發現（錯誤程式碼），更容易推理和確認；設計漏洞可能非常隱蔽，更難以發現（沒有「錯誤」程式碼），更難以推理和確認。

發現ZK漏洞的最佳實踐

根據我們在審計和形式化驗證zkVM以及其他ZK及非ZK鏈的經驗，以下是關於如何最好地保護ZK系統的一些建議：

檢查程式碼以及設計

如前所述，ZK的程式碼和設計中都可能存在漏洞。這兩種類型的漏洞都可能導致ZK系統受到破壞，因此必須在系統投入運作之前消除它們。與非ZK系統相比，ZK系統的一個問題是，任何攻擊都更難揭露和分析，因為其計算細節沒有公開或保留在鏈上。因此人們可能知道發生了駭客攻擊，但卻無法知道技術層面上是如何發生的。這使得任何ZK漏洞的成本都非常高。相應地，預先確保ZK系統安全性的價值也非常高。

進行審計以及形式化驗證

我們在這裡介紹的兩個漏洞分別是透過審計和形式化驗證發現的。有人可能會認為，使用了形式化驗證就不需要審計了，因為所有的漏洞都會被形式化驗證發現。實際上我們的建議是兩者都要進行。正如本文開頭所解釋的，一個高品質的形式化驗證工作始於對程式碼和設計的徹底審查、檢查和非正式推理；而這項工作本身就與審計重疊。此外，在審計期間發現並排除更簡單的漏洞，將使形式化驗證變得更加簡單和有效率。

如果要對一個ZK系統既進行審計又進行形式化驗證，那麼最佳時機是同時進行這兩項工作，以便審計師和形式化驗證工程師能夠高效地協作（有可能會發現更多的漏洞，因為形式化驗證的物件和目標需要高品質的審計輸入）。

如果你的ZK專案已經進行了審計（讚）或多次審計（大讚），我們的建議是在先前審計結果的基礎上對電路進行形式化驗證。我們在zkVM以及其他ZK和非ZK專案的審計和形式化驗證的經驗一再表明，驗證常常能捕捉到審計中遺漏而不易發現的漏洞。由於ZKP的特性，雖然ZK系統應該提供比非ZK解決方案更好的區塊鏈安全性和可擴展性，但其自身的安全性和正確性的關鍵程度要遠高於傳統的非ZK系統。因此，對ZK系統進行高品質形式化驗證的價值也遠高於非ZK系統。

確保電路以及智能合約的安全

ZK應用通常包含電路和智能合約兩個部分。對於基於zkVM的應用，有通用的zkVM電路和智能合約應用。對於非基於zkVM的應用，有應用特定的ZK電路及相應部署在L1鍊或橋的另一端的智能合約。

我們對zkWasm的審計和形式驗證工作只涉及了zkWasm電路。從ZK應用的整體安全性角度來看，對其智能合約進行審計和形式化驗證也非常重要。畢竟，在為了確保電路安全方面投入了大量精力之後，如果在智能合約方面放鬆警惕，導致應用最終受到損害，那將是非常遺憾的。

有兩種類型的智能合約值得特別關注。第一種是直接處理ZK證明的智能合約。儘管它們的規模可能不是很大，但它們的風險非常高。第二種是運行在zkVM之上的大中型智能合約。我們知道，它們有時會非常複雜，而其中最有價值的應該進行審計和驗證，特別是因為人們無法在鏈上看到它們的執行細節。幸運的是，經過多年的發展，智能合約的形式化驗證現在已經可以實用，並且為合適的高價值目標做好了準備。

讓我們透過以下的說明來總結形式化驗證（FV）對ZK系統及其組件的影響。