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

在討論 ZK 漏洞之前，讓我們先來了解 CertiK 是如何進行 ZK 形式化驗證的。對于像 ZK 虛擬機（zkVM）這樣的復雜系統(tǒng)，形式化驗證（FV）的第一步是明確需要驗證的內(nèi)容及其性質(zhì)。這需要對 ZK 系統(tǒng)的設計、代碼實現(xiàn)和測試設置進行全面的審查。這個過程與常規(guī)的審計有所重合，但不同之處在于，審查后需要確立驗證的目標和性質(zhì)。在 CertiK，我們稱其為面向驗證的審計。審計和驗證工作通常是一個整體。對于 zkWasm，我們對其同時進行了審計和形式化驗證。

什么是 ZK 漏洞?

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

對于 zkVM 的證明器而言，ZK 證明過程涉及運行程序、生成每一步的執(zhí)行記錄，并把執(zhí)行記錄的數(shù)據(jù)轉換成一組數(shù)字表格（該過程稱為「算術化」）。這些數(shù)字之間必須滿足一組約束（即「電路」），其中包括了具體表單元格之間的聯(lián)系方程、固定的常數(shù)、表間的數(shù)據(jù)庫查找約束，以及每對相鄰表行間所需要滿足的多項式方程（亦即「門」）。鏈上驗證可以由此確認的確存在某張能滿足所有約束的表，同時又保證不會看到表中的具體數(shù)字。

zkWasm 算術化表

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

執(zhí)行 zkVM 指令規(guī)則的 ZK 電路極其復雜。對于 zkWasm 來說，其 ZK 電路的實現(xiàn)涉及超過 6,000 行的 Rust 代碼和數(shù)百個約束。這種復雜性通常意味著可能存在多個漏洞正等待著被發(fā)現(xiàn)。

zkWasm 電路架構

的確，我們通過對于 zkWasm 審計和形式化驗證發(fā)現(xiàn)了多個這樣的漏洞。下面，我們將討論兩個具有代表性的例子，并討論它們之間的差異。

代碼漏洞：Load8 數(shù)據(jù)注入攻擊

第一個漏洞涉及 zkWasm 的 Load8 指令。在 zkWasm 中，堆內(nèi)存的讀取是通過一組 LoadN 指令來完成的，其中 N 是要加載的數(shù)據(jù)的大小。例如，Load64 應該從 zkWasm 內(nèi)存地址讀出 64 位的數(shù)據(jù)。Load8 應該從內(nèi)存中讀出 8 位的數(shù)據(jù)（即一個字節(jié)），并用 0 前綴填充以創(chuàng)建一個 64 位的值。zkWasm 內(nèi)部將內(nèi)存表示為 64 位字節(jié)的數(shù)組，因此其需要「選取」內(nèi)存數(shù)組的一部分。為此使用了四個中間變量（u16_cells），這些變量合起來構成了完整的 64 位加載值。

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

這個約束分為 Load32、Load16 和 Load8 這三種情況。Load64 沒有任何約束，因為內(nèi)存單元正好就是 64 位的。對于 Load32 的情況，代碼確保了內(nèi)存單元中的高 4 個字節(jié)（32 位）必須為零。

對于 Load16 的情況，內(nèi)存單元中的高 6 個字節(jié)（48 位）必須為零。

對于 Load8 的情況，應該要求內(nèi)存單元中的高 7 個字節(jié)（56 位）為零。遺憾的是，在代碼中并非如此。

正如你所見，只有高 9 至 16 位被限制為零。其他的高 48 位可以是任意值，卻仍然可以偽裝成「從內(nèi)存中讀取的」。

通過利用這個漏洞，黑客可以篡改一個合法執(zhí)行序列的 ZK 證明，使得 Load8 指令的運行加載這些意外的字節(jié)，從而導致數(shù)據(jù)損壞。并且，通過精心安排周邊的代碼和數(shù)據(jù)，可能會觸發(fā)虛假的運行和轉賬，從而竊取數(shù)據(jù)和資產(chǎn)。這種偽造的交易可以通過 zkWasm 檢查器的檢查，并被區(qū)塊鏈錯誤地認定為真實交易。

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

該漏洞代表了一類被稱為「代碼漏洞」的 ZK 漏洞，因為它們源于代碼的編寫，并可以通過較小的局部代碼修改來輕松修復。正如你可能會同意的那樣，這些漏洞也相對更容易被人看出來。

設計漏洞：偽造返回攻擊

讓我們來看看另一個漏洞，這次是關于 zkWasm 的調(diào)用和返回。調(diào)用和返回是基本的 VM 指令，它們允許一個運行的上下文（例如函數(shù)）去調(diào)用另一個，并在被調(diào)用者完成其執(zhí)行后，恢復調(diào)用者上下文的執(zhí)行。每次調(diào)用都預期稍后會返回一次。zkWasm 在調(diào)用和返回的生命周期中所追蹤的動態(tài)數(shù)據(jù)被稱為「調(diào)用幀（call frame）」。由于 zkWasm 按順序執(zhí)行指令，所有調(diào)用幀可以根據(jù)其在運行過程中的發(fā)生時間進行排序。下面是一個在 zkWasm 上運行的調(diào)用 / 返回代碼示例。

用戶可以調(diào)用 buy_token() 函數(shù)來購買代幣（可能是通過支付或轉移其他有價值的東西）。它的核心步驟之一是通過調(diào)用 add_token() 函數(shù)，實際將代幣賬戶余額增加 1。由于 ZK 證明器本身并不支持調(diào)用幀數(shù)據(jù)結構，因此需要使用執(zhí)行表（E-Table）和跳轉表（J-Table）來記錄和追蹤這些調(diào)用幀的完整歷史記錄。

上圖說明了 buy_token() 調(diào)用 add_token() 的運行過程，以及從 add_token() 返回到 buy_token() 的過程。可以看到，代幣賬戶余額增加了 1。在執(zhí)行表中，每個運行步驟占一行，其中包括當前執(zhí)行中的調(diào)用幀編號、當前上下文函數(shù)名稱（僅用于此處的說明）、該函數(shù)內(nèi)當前運行指令的編號，以及表中所存的當前指令（僅用于此處的說明）。在跳轉表中，每個調(diào)用幀占一行，表中存有其調(diào)用者幀的編號、調(diào)用者函數(shù)上下文名稱（僅用于此處的說明）、調(diào)用者幀的下一條指令位置（以便該幀可以返回）。在這兩個表中，都有一個 jops 列，它追蹤當前指令是否為調(diào)用 / 返回（在執(zhí)行表）以及該幀（在跳轉表）發(fā)生的調(diào)用 / 返回指令總數(shù)。

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

但實際上這里有一個問題：盡管一次調(diào)用和一次返回將使幀的 jops 計數(shù)為 2，但兩次調(diào)用或者兩次返回也會使計數(shù)為 2。每幀有兩次調(diào)用或兩次返回聽起來可能很荒謬，但要牢記的是，這正是黑客試圖通過打破預期要做的事情。

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

結果表明，兩次調(diào)用并不是問題，因為執(zhí)行表和調(diào)用表的約束使得兩個調(diào)用無法被編碼到同一幀的行中，因為每次調(diào)用都會產(chǎn)生一個新的幀編號，即當前調(diào)用幀編號加 1。

而兩次返回的情況就沒那么幸運了：由于在返回時不會創(chuàng)建新的幀，黑客確實有可能獲取合法運行序列的執(zhí)行表和調(diào)用表，并注入偽造的返回（以及相應的幀）。例如，先前執(zhí)行表和調(diào)用表中 buy_token() 調(diào)用 add_token() 的例子可以被黑客篡改為以下情況：

黑客在執(zhí)行表中原來的調(diào)用和返回之間注入了兩次偽造的返回，并在調(diào)用表中增加了一個新的偽造的幀行（原來的返回和后續(xù)指令的運行步驟編號在執(zhí)行表中則需要加 4）。由于調(diào)用表中每一行的 jops 計數(shù)均為 2，因此滿足了約束條件，zkWasm 證明檢查器將接受這個偽造的執(zhí)行序列的「證明」。從圖中可以看出，代幣賬戶余額增加了 3 次而不是 1 次。因此，黑客能夠以支付 1 個代幣的價格獲得 3 個代幣。

解決這個問題有多種方法。一個明顯的方法就是分別單獨追蹤調(diào)用和返回，并確保每一幀恰好有一次調(diào)用和一次返回。

你可能已經(jīng)注意到，到目前為止我們尚未展示這個漏洞的哪怕一行代碼。主流的原因是沒有任何一行代碼是有問題的，代碼實現(xiàn)完全符合表格和約束設計。問題在于設計本身，而修復方法也是如此。

你可能認為，這個漏洞應該是顯而易見的，但實際上并非如此。這是因為「兩次調(diào)用或兩次返回也會導致 jops 計數(shù)為 2」與「實際上兩次返回是可能的」之間存在空白。后者需要對執(zhí)行表和調(diào)用表中相關的各種約束進行詳細、完整地分析，很難進行完整的非形式化推理。

兩個漏洞的比較

對于「Load8 數(shù)據(jù)注入漏洞」和「偽造返回漏洞」，它們都可能導致黑客能夠操縱 ZK 證明、創(chuàng)建虛假交易、騙過證明檢查器，并進行竊取或劫持。 但他們的性質(zhì)和被發(fā)現(xiàn)的方式卻截然不同。

「Load8 數(shù)據(jù)注入漏洞」是在對 zkWasm 進行審計時發(fā)現(xiàn)的。這絕非易事，因為我們必須審查超過 6,000 行的 Rust 代碼和上百條 zkWasm 指令的數(shù)百個約束。盡管如此，這個漏洞還是相對容易發(fā)現(xiàn)和確認的。由于這個漏洞在形式化驗證開始之前就已被修復，所以在驗證過程中并未遇到它。如果在審計過程中未發(fā)現(xiàn)該漏洞，我們可以預期在對 Load8 指令的驗證中會發(fā)現(xiàn)它。

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

總結來說，這兩種漏洞分別屬于「代碼漏洞」和「設計漏洞」。代碼漏洞相對較為淺顯，更容易被發(fā)現(xiàn)（錯誤代碼），并且更容易推理和確認；設計漏洞可能非常隱蔽，更難以發(fā)現(xiàn)（沒有「錯誤」代碼），更難以推理和確認。

發(fā)現(xiàn) ZK 漏洞的最佳實踐

根據(jù)我們在審計和形式化驗證 zkVM 以及其他 ZK 及非 ZK 鏈的經(jīng)驗，下面是關于如何最好地保護 ZK 系統(tǒng)的一些建議。

檢查代碼以及設計

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

進行審計以及形式化驗證

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

如果要對一個 ZK 系統(tǒng)既進行審計又進行形式化驗證，那么最佳時機是同時進行這兩項工作，以便審計師和形式化驗證工程師能夠高效地協(xié)作（有可能會發(fā)現(xiàn)更多的漏洞，因為形式化驗證的對象和目標需要高質(zhì)量的審計輸入）。

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

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

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

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

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

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

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