零知識證明的先進形式化驗證：兩個ZK漏洞的深度剖析

2024-05-29 16:05:28

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

ZK應用電路智能合約基於zkVMzkVM應用非基於zkVM應用特定L1鏈/橋

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

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

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