在上一篇文章中，我們討論了零知識證明 （ZKP） 系統的高級形式驗證：如何驗證 ZK 指令。通過對每條zkWasm指令進行正式驗證，我們可以充分保證整個zkWasm電路的技術安全性和正確性。在本文中，我們將重點關注漏洞發現的角度，分析在審計和驗證過程中發現的特定漏洞，以及從中吸取的經驗教訓。關於ZKP區塊鏈高級形式驗證的一般性討論，請參考ZKP區塊鏈高級形式驗證一文。

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

什麼是 ZK 漏洞？

零知識證明 （ZKP） 系統的核心特徵是它們允許將離線或私下執行的計算（例如區塊鏈交易）的簡短加密證明傳輸給 ZKP 驗證器。驗證者檢查並確認證明，以確保計算按聲明進行。在這種情況下，ZK 漏洞將使駭客能夠提交偽造的 ZK 證明以進行虛假交易，並讓 ZKP 驗證者接受它們。

對於 zkVM 驗證者，ZK 證明過程涉及運行程式，為每個步驟生成執行記錄，並將這些執行記錄轉換為一組數值表（該過程稱為“算術化”）。這些數字必須滿足一組約束（“電路”），其中包括特定表單元格之間的關係、固定常量、表之間的資料庫查找約束以及每對相鄰表行必須滿足的多項式方程（或“門”）。鏈上驗證可以確認是否存在滿足所有約束的表，而無需透露表中的具體數位。

zkWasm 中的算術化表

每個約束的準確性都至關重要。約束中的任何錯誤，無論是太弱還是太缺失，都可能允許駭客提交誤導性證明。這些表可能看起來代表了智能合約的有效執行，但實際上並非如此。與傳統虛擬機相比，zkVM 事務的不透明性放大了這些漏洞。在非ZK鏈中，交易計算的細節被公開記錄在區塊鏈上;但是，zkVM不會將這些詳細資訊存儲在鏈上。由於缺乏透明度，很難確定攻擊的具體情況，甚至很難確定攻擊是否已經發生。

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

zkWasm 電路架構

事實上，通過對 zkWasm 的審計和形式驗證，我們發現了幾個這樣的漏洞。下面，我們將討論兩個具有代表性的例子，並研究它們之間的區別。

代碼漏洞：Load8 數據注入攻擊

第一個漏洞涉及 zkWasm 中的 Load8 指令。在 zkWasm 中，堆記憶體讀取是使用一組 LoadN 指令完成的，其中 N 是要載入的數據的大小。例如，Load64 應該從 zkWasm 記憶體位址讀取 64 位數據。Load8 應該從記憶體中讀取 8 位數據（即一個字節），並用零填充它以創建 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 在調用和返回的生命週期中跟蹤的動態數據被稱為“調用幀”。由於 zkWasm 按順序執行指令，因此所有調用幀都可以根據它們在運行時出現的次數進行排序。下面是在 zkWasm 上運行的調用/返回代碼的示例。

用戶可以調用 buy_token（） 函數來購買代幣（可能通過支付或轉移其他貴重物品）。其核心步驟之一是通過調用 add_token（） 函數將代幣賬戶餘額增加 1。由於 ZK 證明器本身不支援調用幀數據結構，因此需要執行表 （E-Table） 和跳轉表 （J-Table） 來記錄和跟蹤這些調用幀的完整歷史記錄。

上圖說明瞭 buy_token（） 調用 add_token（） 並從 add_token（） 傳回到 buy_token（） 的過程。可以看出，代幣賬戶餘額增加了1。在執行表中，每個執行步驟佔用一行，包括正在執行的當前調用幀號、當前上下文函數名稱（僅用於說明目的）、函數內當前正在運行的指令的編號以及存儲在表中的當前指令（僅用於說明目的）。在跳轉表中，每個調用幀佔用一行，存儲其調用方幀的編號、調用方函數上下文名稱（僅用於說明目的）和調用方幀的下一個指令位置（以便該幀可以返回）。在這兩個表中，都有一個“jops”列，用於跟蹤當前指令是否為調用/返回（在執行表中）以及該幀的調用/返回指令總數（在跳轉表中）。

正如預期的那樣，每個調用應該有相應的返回，每個幀應該只有一個調用和一個返回。如上圖所示，跳轉表中第一幀的“jops”值為 2，對應執行表中的第一行和第三行，其中“jops”值為 1。目前一切看起來都很正常。

但是，這裡有一個問題：雖然一次調用和一次返回會將幀的“jops”計數增加到 2，但兩次調用或兩次返回也會導致計數為 2。每幀有兩個調用或兩個返回可能看起來很荒謬，但重要的是要記住，這正是駭客試圖通過打破預期來做的事情。

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

事實證明，兩個調用不是問題，因為執行表和跳轉表的約束阻止了兩個調用被編碼到幀的同一行中，因為每個調用都會生成一個新的幀號，即當前調用幀號加 1。

然而，對於兩次返回來說，情況就沒有那麼幸運了：由於返回時沒有創建新幀，駭客確實可以獲取合法執行序列的執行表和跳轉表，並注入偽造的返回（和相應的幀）。例如，buy_token（） 調用 add_token（） 的先前執行表和跳轉表示例可能會被駭客篡改為以下情況：

駭客在執行表中的原始調用和返回之間注入了兩個偽造的返回，並在跳轉表中添加了一個新的偽造幀行（執行表中的原始返回和後續指令執行步驟需要遞增 4）。由於跳轉表中每行的 「jops」 計數為 2，因此滿足約束條件，並且 zkWasm 證明檢查器將接受此偽造執行序列的 「證明」。。從圖中可以看出，代幣賬戶餘額增加了 3 倍而不是 1 倍。因此，駭客可以以 3 的價格獲得 1 個代幣。

有多種方法可以解決這個問題。一個明顯的方法是分別跟蹤呼叫和返回，並確保每個幀只有一個呼叫和一個返回。

您可能已經注意到，到目前為止，我們還沒有針對此漏洞顯示任何代碼行。主要原因是沒有有問題的代碼行;代碼實現與表和約束設計完全一致。問題出在設計本身，修復也是如此。

您可能認為這個漏洞應該是顯而易見的，但實際上並非如此。這是因為「兩次調用或兩次返回也會導致『jops』計數為 2“和”實際上可能兩次返回“之間存在差距。後者需要對執行表和跳轉表中的各種約束進行詳細而全面的分析，這使得執行完整的非正式推理具有挑戰性。

兩個漏洞的比較

“Load8 數據注入漏洞”和“偽造返回漏洞”都有可能讓駭客操縱 ZK 證明、創建虛假交易、欺騙證明檢查人員以及進行盜竊或劫持。然而，它們的性質和被發現的方式卻大不相同。

“Load8 數據注入漏洞”是在 zkWasm 審計過程中發現的。這不是一件容易的事，因為我們必須審查 6,000 多行 Rust 代碼中的數百個約束和數十條 zkWasm 指令。儘管如此，該漏洞相對容易檢測和確認。由於此漏洞在正式驗證開始之前已修復，因此在驗證過程中未遇到該漏洞。如果在審計過程中沒有發現此漏洞，我們可以預期在驗證Load8指令期間會發現它。

“偽造退貨漏洞”是在審計后的正式驗證中發現的。我們在審計過程中沒有發現它的一個原因是 zkWasm 有一個類似於 “jops” 的機制，稱為 “mops”，它跟蹤 zkWasm 運行時與每個記憶體單元的歷史數據相對應的記憶體訪問指令。對拖把計數的約束確實是正確的，因為它只跟蹤一種類型的記憶體指令，即記憶體寫入，並且每個記憶體單元的歷史數據是不可變的，並且只寫入一次（拖把計數為 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系統及其元件的影響，具體總結如下幾點。

陳述：

1. 本文轉載自【panewslab】，版權歸原作者【CertiK】所有，如對轉載有異議，請聯繫Gate Learn團隊，團隊將按照相關程序儘快處理。

2. 免責聲明：本文所表達的觀點和意見僅代表作者的個人觀點，不構成任何投資建議。

3. 文章的其他語言版本由 Gate Learn 團隊翻譯， 未在 Gate.io 中提及，翻譯後的文章不得轉載、分發或抄襲。