ZK 漏洞將使得駭客可以提交用於證明虛假交易的偽造 ZK 證明，並讓 ZK 證明檢查器接受。
作者：CertiK
封面： Photo by Singh on Unsplash
在先前的文章中，我們討論了零知識證明的先進形式化驗證：如何驗證一條 ZK 指令。透過形式化驗證每條 zkWasm 指令，我們能夠完全驗證整個 zkWasm 電路的技術安全性和正確性。在本文中，我們將專注於發現漏洞的視角，分析在審計和驗證過程中發現的具體漏洞，以及從中得到的經驗和教訓。如要了解有關零知識證明（ZKP）區塊鏈的先進形式化驗證的一般討論，請參見零知識證明區塊鏈的先進形式化驗證一文。
在討論 ZK 漏洞之前，讓我們先來了解 CertiK 是如何進行 ZK 形式化驗證的。對於像 ZK 虛擬機器（zkVM）這樣的複雜系統，形式化驗證（FV）的第一步是明確需要驗證的內容及其性質。這需要對 ZK 系統的設計、程式碼實作和測試設定進行全面的審查。這個過程與常規的審計有所重疊，但不同之處在於，審查後需要確立驗證的目標和性質。在 CertiK，我們稱之為面向驗證的審計。審計和驗證工作通常是一個整體。對於 zkWasm，我們對其同時進行了審計和形式化驗證。
什麼是 ZK 漏洞？
零知識證明系統的核心特徵在於允許將離線或私密執行的計算（例如區塊鏈交易）的簡短加密證明傳遞給零知識證明驗證器，並由其檢查和確認，以確信該計算確已按聲明的情況發生過。就此而言，ZK 漏洞將使得駭客可以提交用於證明虛假交易的偽造 ZK 證明，並讓 ZK 證明檢查器接受。
對於 zkVM 的證明器而言，ZK 證明過程涉及運行程式、產生每一步的執行記錄，並將執行記錄的資料轉換成一組數字表格（該過程稱為「算術化」）。這些數字之間必須滿足一組約束（即「電路」），其中包括了具體表單元格之間的聯繫方程式、固定的常數、表間的資料庫查找約束，以及每對相鄰表行間所需滿足的多項式方程式（亦即 “門”）。鏈上驗證可以由此確認的確存在某張能滿足所有限制的表，同時又保證不會看到表中的具體數字。
每一個約束的準確性至關重要。任何約束中的一個錯誤，無論是偏弱或缺失，都可能使得駭客能夠提交一個誤導性的證明，這些表格看似代表了智能合約的一次有效運行，但實際上並非如此。與傳統 VM 相比，zkVM 交易的不透明性放大了這些漏洞。在非 ZK 鏈中，交易的計算細節是公開記錄在區塊之上的；而 zkVM 則不將這些細節儲存於鏈上。透明度的缺失使得攻擊的具體情況很難被確定，甚至連攻擊是否已發生都很難確定。
執行 zkVM 指令規則的 ZK 電路極為複雜。對於 zkWasm 來說，其 ZK 電路的實現涉及超過 6,000 行的 Rust 程式碼和數百個約束條件。這種複雜性通常意味著可能存在多個漏洞正等待被發現。
的確，我們透過對於 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 系統及其組件的影響。
免責聲明：作為區塊鏈資訊平台，本站所發布文章僅代表作者及來賓個人觀點，與 Web3Caff 立場無關。文章內的資訊僅供參考，均不構成任何投資建議及要約，並請您遵守所在國家或地區的相關法律法規。
