在之前的文章中，我們討論了零知識證明的先進形式化驗證：如何驗證一條 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 鏈或橋的另一端的智能合約。基于 zkVM 非基于 zkVM

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

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

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

• FV 電路 + 非 FV 智能合約 = 非 FV 零知識證明
• 非 FV 電路 + FV 智能合約 = 非 FV 零知識證明
• FV 電路 + FV 智能合約 = FV 零知識證明