為了深入理解形式化驗證技術是如何應用於 zkVM（零知識虛擬機）之上的，本文將聚焦於單一指令的驗證。
作者：Certik
封面： Photo by Cory Bunge on Unsplash
為了深入理解形式化驗證技術是如何應用於 zkVM（零知識虛擬機）之上的，本文將聚焦於單一指令的驗證。關於 ZKP（零知識證明）先進形式化驗證的整體情況，請查閱我們同期發布的「零知識證明區塊鏈的先進形式化驗證」文章。
什麼是 ZK 指令的驗證？
zkVM（零知識虛擬機）能夠創建簡短的證明對象，以作為證據來證明特定程式可以在某些輸入上運行、並成功終止。在 Web3.0 領域，zkVM 的應用使得吞吐量變高，這是因為 L1 節點只需要驗證智能合約從輸入態到輸出態轉變過程的簡短證明，而實際的合約程式碼執行則可以在鏈下完成。
zkVM 證明器首先會執行程式以產生每個步驟的執行記錄，然後將執行記錄的資料轉換為一組數字表格（該過程稱為「算術化」）。這些數之間必須滿足一組約束（即電路），其中包括了具體表單元格之間的聯繫方程式、固定的常數、表間的資料庫查找約束，以及每對相鄰表行間所需要滿足的多項式方程式（亦即「門」）。鏈上驗證可以由此確認的確存在某張能滿足所有限制的表，同時又保證不會看到表中的具體數字。
每個 VM 指令的執行都面臨許多這樣的約束，這裡我們將 VM 指令的這組約束簡稱為它的「ZK 指令」。下面是用 Rust 語言編寫的一個 zkWasm 記憶體載入指令約束的範例。
ZK 指令的形式化驗證是透過對這些程式碼進行形式化推理來完成的，我們首先將其翻譯成形式化語言。
即便只有單一約束包含錯誤，攻擊者都因此而有可能提交惡意的 ZK 證明。惡意證明所對應的資料表格並不對應智能合約的合法運作。與以太坊等非 ZK 鏈不同，後者有許多節點運行不同的 EVM（以太坊虛擬機）實現，從而不太可能在同時同地出現相同的錯誤，一個 zkVM 鏈則只有單一的 VM 實現。單就這個角度而言，ZK 鏈比傳統的 Web3.0 系統更脆弱。
更糟的是，和非 ZK 鏈不一樣，由於 zkVM 交易的計算細節並沒有被提交並儲存在鏈上，在攻擊發生後，不僅是要發現攻擊的具體細節非常困難，甚至要識別攻擊本身也會變得極具挑戰性。
zkVM 系統需要極為嚴格的檢視，不幸的是，zkVM 電路的正確性很難保證。
ZK 指令的驗證為何很難？
VM（虛擬機器）是 Web3.0 系統架構中最複雜的部分之一。智慧合約的強大功能是支撐 Web3.0 能力的核心，其力量源自於底層的 VM，它們既靈活又複雜：為了完成通用運算和儲存任務，這些 VM 必須能夠支援眾多的指令和狀態。例如，EVM 的 geth 實作需要超過 7500 行 Go 語言程式碼。類似的，約束這些指令執行的 ZK 電路也同樣龐大且複雜。像在 zkWasm 專案中，ZK 電路的實作需要超過 6000 行 Rust 程式碼。
與專為特定應用（如私人支付）設計的 ZK 系統中使用的專用 ZK 電路相比，zkVM 電路的規模要大得多：其約束規則的數量可能比前者多出一到兩個數量級，而其算術化表格則可能包括數百列、含有數百萬的數字儲存格。
ZK 指令的驗證意味著什麼？
我們在這裡想要去驗證 zkWasm 中的 XOR 指令的正確性。從技術上講，zkWasm 的執行表對應一個合法的 Wasm VM 執行序列。所以宏觀來看，我們想要驗證的是：每次執行這條指令總是會產生一個新的合法的 zkVM 狀態：表中的每一行都對應 VM 的一個合法狀態，而緊接著的一行則總是要透過執行對應的 VM 指令來產生。下圖為 XOR 指令正確性的形式化定理。
這裡「state_rel i st」表示狀態「st」是步驟「i」中智慧合約的合法 zkVM 狀態。 正如你可能猜測的那樣，要證明「state_rel (i+1) …」不是輕而易舉的。
如何驗證 ZK 指令？
儘管 XOR 指令的計算語意很簡單，就是計算兩個整數的位元異或（bitwise xor）並傳回整數結果，但它所涉及的面向卻比較多：首先，它需要從堆疊記憶體中取出兩個整數，進行異或計算，然後將這個計算得出的新整數存回同一個堆疊。此外，此指令的執行步驟應融入整個智慧合約的執行流程中，且其執行順序及時機必須正確。
因此，XOR 指令的執行效果應該是從資料堆疊中彈出兩個數，壓入它們的 XOR 結果，同時增加程式計數器，以指向智慧合約的下一指令。
不難看出，這裡的正確性屬性定義總體上與我們在驗證傳統字節碼 VM（例如以太坊 L1 節點中的 EVM 解釋器）的時候所面對的情況非常相似。它依賴機器狀態（這裡指棧記憶體和執行流）的高階抽象定義，以及關於每個指令預期行為的定義（這裡指算術邏輯）。
然而，如我們下面所將要看到的，由於 ZKP 和 zkVM 的特殊性，其正確性的驗證過程經常與常規 VM 的驗證不同。光是驗證我們這裡的單一指令，就要依賴 zkWASM 中很多表的正確性：其中有一張用於限制數值大小的範圍表，一張用於二進位位計算中間結果的位表（bit table），一張每行都儲存恆定大小的 VM 狀態的執行表（類似物理 CPU 中的暫存器和鎖存器中的資料），以及代表動態可變大小的 VM 狀態（記憶體、資料堆疊和呼叫堆疊）的記憶體表和跳轉表。
第一步：堆疊記憶體
與傳統 VM 類似，我們需要確保指令的兩個整數參數可以從堆疊中讀取，並且其異或結果值被正確地寫回堆疊。堆疊的形式化表述看起來也相當熟悉（還有全域記憶體和堆疊內存，但 XOR 指令不使用它們）。
zkVM 使用一種複雜的方案來表示動態數據，這是因為 ZK 證明器並不能原生支援像堆疊或陣列這樣的資料結構。相反的，對於壓入堆疊的每個數值，記憶體表用單獨的一行來記錄，其中的某些列則用於指示該表項的生效時間。當然，這些表的資料可以被攻擊者所控制，因此也必須加以一些約束，以確保表項真實對應於合約執行中的實際壓棧指令。這是透過精心計算程式執行過程中的壓棧次數來實現的。驗證每一條指令時，我們需要確保這個計數始終正確。此外，我們還有一系列引理，將單一指令產生的約束與實作堆疊操作的表查找和時間範圍檢查相關聯。從最頂層看，記憶體操作的計數約束定義如下。
第二步：算術運算
與傳統 VM 類似，我們希望確保位異或的運算正確無誤。這看起來很容易，畢竟我們的實體電腦 CPU 都能夠一次完成這個操作。
但對於 zkVM 來說，這其實並不簡單。 ZK 證明器原生支援的唯二算術指令是加法和乘法。為了進行二進位位元運算，VM 使用了一個相當複雜的方案，其中一張表存放固定的位元組級運算結果，另一張表則充當「草稿本」，用以在多個表行上展示如何將 64 位數分解為 8 個字節，然後再重新組合出結果。
在傳統的程式語言中非常簡單的異或運算，在這裡則需要很多引理來驗證這些輔助表的正確性。對於我們的指令，我們有：
第三步：執行流
與傳統 VM 類似，我們需要確保程式計數器的數值正確更新。對於像 XOR 這樣的順序指令，每次執行步驟後，程式計數器就需要加一。
由於 zkWasm 被設計用來運行 Wasm 程式碼，因此也要確保在整個執行過程中，Wasm 記憶體的不變性質始終保持不變。
傳統的程式語言對布林值、8 位元整數、64 位元整數等資料型別有原生支持，但在 ZK 電路中，變數始終是在大質數（≈ 2254）模下的整數範圍內變化。由於 VM 通常以 64 位數運行，電路開發者需要使用一套約束系統來確保它們具有正確的數值範圍，而形式化驗證工程師則需要在整個驗證過程中追蹤關於這些範圍的不變性質。執行流程和執行表的推理會涉及到所有的其他輔助表，因此我們需要檢查所有表格資料的範圍是否正確。
類似於記憶體操作數量管理的情形，zkVM 需要一組類似的引理來驗證控制流。具體而言，每個呼叫和返回指令都需要使用呼叫棧。呼叫棧使用與資料棧類似的表方案來實作。對於 XOR 指令，我們並不需要修改呼叫堆疊；但在驗證整個指令時，仍然需要追蹤並驗證控制流程操作計數是否正確。
驗證這條指令
讓我們將所有步驟整合起來，驗證 zkWasm XOR 指令的端對端正確性定理。以下驗證是在互動式證明環境中完成的，其中每一個形式化構造和邏輯推理步驟都經過了最嚴格的機器檢查。
如上所見，形式化驗證 zkVM 電路是可行的。但這是一項艱鉅的任務，需要理解和追蹤許多複雜的不變性質。這反映了被驗證軟體本身的複雜性：驗證中所涉及的每一條引理都需要得到電路開發者的正確處理。鑑於其中的風險很高，讓它們由形式化驗證系統進行機器檢驗，而不是僅僅依靠小心謹慎的人工審查，是非常有價值的。
免責聲明：作為區塊鏈資訊平台，本站所發布文章僅代表作者及來賓個人觀點，與 Web3Caff 立場無關。文章內的資訊僅供參考，均不構成任何投資建議及要約，並請您遵守所在國家或地區的相關法律法規。
