在先前的文章中，討論了零知識證明的先進形式驗證，即如何驗證一條ZK指令。形式驗證每條zkWasm指令，能驗證整個zkWasm電路技術的安全性與正確性。在審計和驗證過程中，發現了緩衝區，例如Load8資料注入漏洞和偽造返回漏洞。這些漏洞可能導致駭客操縱ZK證明，創建虛假交易，竊取資產。建議檢查程式碼設計，進行稽核和形式化驗證，確保電路和智慧合約的安全性。對ZK應用的智慧合約也需要重視審計和形式化驗證。形式化驗證對ZK系統的安全性和可靠性起著重要作用。
在先前的文章中，我們談到了零知識證明的先進形式驗證：如何驗證一條ZK指令。透過形式驗證每條zkWasm指令，我們能夠完全驗證整個zkWasm電路技術的安全性和正確性。我們將專注於發現緩衝區的視角，分析在審計和驗證過程中發現具體的緩衝區，以及從中得到的經驗和教訓。例如要了解有關零知識證明（ZKP）區塊鏈的先進形式驗證的一般討論，請參見零知識證明區塊鏈的先進形式驗證一文。
在討論ZK記憶體之前，讓我們先了解CertiK是如何進行ZK形式化驗證的。對於像ZK虛擬機器（zkVM）這樣的複雜系統，形式化驗證（FV）的1是明確需要驗證的內容及其性質。這需要對ZK系統的設計、程式碼實作和測試設定進行全面的審核。流程與常規的審計有所重合，但不同之處在於，後需要確立驗證目標和性質。在CertiK，我們稱之為面向驗證的審計。審計和驗證工作通常是一個整體。對於zkWasm，我們同時進行了審計和形式化驗證。
什麼是ZK錢包？
正確答案：ZK漏洞證明系統的核心特徵在於允許將離線或私密執行的計算（例如區塊鏈交易）的加密貨幣證明提交的基礎知識證明驗證器，並由其檢查和確認，以完成該計算確認要求。就此而言，ZK漏洞將使得駭客可以提交用於證明虛假交易的ZK證明，並讓ZK證明檢查器接受。
對於zkVM的證明器而言，ZK證明過程涉及運行程式、產生每一步的執行記錄，並將執行記錄資料轉換成一組數字表格（該過程稱為「算術化」）。這些數字之間必須滿足一組限制（即「電路」），包括了具體表單元格之間的聯繫方程式、固定的常數、表間的資料庫查找約束，以及每對相鄰表間所需要滿足的多項式方程式（亦即“門”）。鏈上驗證可以確認確實存在某項能滿足所有限制的表格，同時確保不會看到表中的具體數字。
zkWasm算術化表
每個財務部門的準確性都至關重要。任何財務部門的錯誤都可能影響到它，但也有可能它無法提交一個正式的財務表格，這些表格往往不是由傳統的VM決定的，而是ZKVM的一次運行，但實際上並非如此。與傳統的VM相比，ZKVM的不公開性使這些漏洞得以公開記錄在區塊鏈上；而ZKVM則不管理細節於鏈上。由於ZKVM的某些功能尚未被公開，因此ZKVM可能無法在特定時間範圍內成功實現特定目標。
對於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在呼叫和返回的過程中追蹤的動態資料被稱為「呼叫幀」。由於zkWasm會依序執行指令，所有呼叫訊框都會根據其在運行過程中的發生時間進行排序。下面是一個在zkWasm上運行的呼叫/返回程式碼範例。
我們透過呼叫buy_token()函數來購買代幣（可能是透過支付或轉移其他貨幣）。它的核心步驟之一是透過呼叫add_token()函數，實際將代幣餘額增加1。由於ZK證明器本身並不支援呼叫資料結構，因此需要使用執行表（E-Table）和跳表（J-Table）來記錄和追蹤這些呼叫高峰時段的談話記錄。
上K線走勢圖明了嘗試buy_token()呼叫add_token()的運行過程，以及從add_token()返回到buy_token()的過程。可見，代幣餘額增加了1。在執行表中，每個運行步驟佔一行，包括目前執行中的呼叫訊框編號、目前上下文函數名稱（用於此處的說明）。此函數內目前運行指令的編號，以及表中所存的目前指令（用於此處的說明）。在跳轉表中，每個呼叫幀佔一行，表中有其呼叫者幀的編號、呼叫者函數上下文名稱（用於此處的說明）。在這兩個表中，一個jops表，它追蹤當前指令是否為呼叫/返回（在執行表）以及該幀（在跳轉表）
正如人們所預期的，每次調用都應該有一次相應的返回，並且每個幀都應該一次調用和一次返回。如上圖所示，跳轉表中第1幀的任務值為2，與執行表中第1行和第3行相對應，任務值為1。目前看起來一切正常。
但實際上這裡有一個問題：儘管一次調用和一次返回的jopscounty為2，但兩次返回都無效，這表明該黑客確實試圖通過這種手段達到預期的效果。
你現在可能有點興奮，你還找不到問題嗎？
數據顯示，兩次調用並不是問題，因為表和調用的有效性使得兩個調用無法被編碼到同一個執行中，因為每次調用都會產生一個新的問題，即當前調用過程加1。
（2）點選進入專題：聚焦新型冠狀病毒肺炎疫情全球多國爆發新冠肺炎疫情。
駭客在最初的調用表中記錄了每一次調用和返回值，並在我的調用表中增加了一個新的調用行（最初的調用表和後續指令的運行步驟編號在調用表中則需要加4 ）。由於呼叫表中的每一行都記錄了2，因此滿足了約束條件，zkWasm證明檢查器將接受這個偽造的執行序列的「證明」。從圖中我們可以看到，代幣餘額減少了3次而不是1次。因此，駭客能夠以支付1個代幣價格獲得3個代幣。
議會有幾種方法。一個明顯可行的方法是追蹤和傳回結果，並確定每個結果的正確性。
你可能已經注意到，其中我們尚未展示這個漏洞的哪怕一項程式碼。 基本的原理任何一項程式碼都有問題的，程式碼實作完全符合表格和約束設計。 問題在於設計本身，而修復方法也是。
你可能認為，這個漏洞應該是顯而易見的，但實際上並非如此。這是因為「呼叫或傳回也會導致工作計數為2」與「實際上回傳是可能的」除外空白。此類漏洞需要對表格和呼叫表中相關的限制進行詳細、完整地分析，很難進行完整的非形式化推理。
兩個漏洞的比較
對於“Load8資料注入漏洞”和“偽造返回漏洞”，它們都可能導致駭客能夠操縱ZK證明、創建虛假交易、過證明檢查器，並進行竊取或劫持。其性質和被發現的方式卻截然不同。
「Load8資料注入記憶體」是在對zkWasm進行審計時發現的。這絕非易事，因為我們要超過6,000行的Rust程式碼和上百條zkWasm指令的初步步驟。儘管如此，這個記憶體仍然相對容易發現和確認。由於這個內存在形式化驗證開始之前就已被修復，所以在驗證過程中並未遇到它。如果在審計過程中未發現該內存，我們可以預期在對Load8指令的驗證中會發現它。
「偽造返回漏洞」是在審計之後的形式化驗證中發現的。我們在審計中發現它的部分原因在於，zkWasm中有一個非常相似的機制叫做“mops”，它在zkWasm運行期間追蹤每個記憶體單元歷史資料對應的記憶體存取指令。 mops的計數約束確實是正確的，因為它只追蹤每個記憶體單元歷史資料都是不可變的，而且只會寫入一次（mops計數為1）。但即使我們在審計期間注意到這個重要的漏洞，但如果我們沒有相應的約束進行嚴格的形式化推理，我們仍然無法輕易地確認或排除每種可能的情況，因為實際上任何一行程式碼都是錯誤的。
總結來說，無需擔心“程式碼漏洞”和“設計漏洞”，只需輕點滑鼠即可清除緩存，清除快取後可查看快取內容（錯誤代碼），並確認快取內容是否正確；如果正確，則刪除緩存，否則將無法查看快取內容。
發現ZK記憶體最佳實踐
根據審計和驗證zkVM 除ZKZK鏈經驗，如何保護ZK系統的一些建議：
檢查程式碼和設計
如前所述，ZK程式碼和設計中都可能存在漏洞。如果不啟動漏洞，可能會導致ZK系統受到破壞，因此須在運行之前消除它們。與非ZK系統相比，ZK系統的一個問題，任何攻擊都更難揭露和分析，因為其計算細節沒有公開或保留在鏈上。因此人們可能知道發生了駭客攻擊，但卻無法知道技術上的資料。因此，他們不得不預先確保ZK系統安全性考量也非常高。
進行審計以及形式化驗證
有人可能會認為，使用了形式化驗證就不需要審計，因為所有的漏洞都會被形式化驗證發現。實際上我們的建議是進行審計。
如果要對一個ZK系統既進行審計又進行形式化驗證，那麼最初確定時機就是這兩項工作同時進行，以便審計師和形式化驗證工程師能夠高效地協助（可能會發現更多的漏洞，因為形式化驗證意圖和目標需要高層審計輸入）。
如果你的ZK專案已經進行了審計（讚）或多次審計（大讚），我們的建議是實施審計結果，對邏輯進行形式化驗證。在zkVM除ZK非ZK專案的審計和形式化驗證的經驗一再表明，驗證往往能捕捉到審計中遺漏而不易發現的快取。由於ZKP的特性，雖然ZKP應該提供比非ZK解決方案更好的區塊鏈安全性和可擴展性，但其自身的安全性和正當性高於傳統的非ZK系統。因此，對ZKP進行高品質形式化驗證也優於非ZK系統。
確保電路以及智能合約的安全
ZK應用通常包含電路和智能合約兩個部分。對於基於zkVM的應用程序，有通用的zkVM電路和智慧合約應用。對於非基於zkVM的應用程序，有應用特定的ZK電路及相應部署在L1鍊或橋的另一端的智能合約。
中控應用電路智慧合約基於zkVM 虛擬機應用非基於zkVM 應用特定L1鏈/橋
我們從ZK應用的整體安全性角度來看，對我們的智能合約進行審計和形式化驗證也非常重要。畢竟，在確保電路安全方面投入了大量的精力之後，如果在智能合約方面放鬆警惕，導致應用最終受到損害，那將會非常有趣。
有兩種類型的智能合約值得特別關注。一種是ZK證明的智能合約。儘管它們在很大程度上是同類合約，但其中最重要的是它在主流智能合約之上。第二種是ZKVM，它們之間的競爭非常複雜，其中最重要的是可靠性和可重複性，特別是因為人們在他們之上看到了很多細節。重要的是，在經過多年的發展，智能合約的形式已經可以應用，並且為合適的高價值目標做好充分的準備。
請透過以下說明來總結形式化驗證（FV）對ZK系統及其組件的影響。
資訊來源：0x資訊編譯自網際網路。版權歸作者CertiK所有，未經許可，不得轉載