在關於零知識證明的先進形式化驗證的系列文章中，我們已經討論瞭如何驗證ZK指令以及對兩個ZK漏洞的深度剖析。
如同在公開報告（https://skynet.certik.com/projects/zkwasm）和程式碼庫（https://github.com/CertiKProject/zkwasm-fv）中所顯示的，透過形式化驗證每一條zkWasm指令，我們找到並修復了每一個漏洞，從而能夠完全驗證整個zkWasm電路的技術安全性和正確性。
儘管我們已展示了驗證一條zkWasm指令的過程，並介紹了相關的專案初步概念，但熟悉形式化驗證讀者可能更想了解zkVM與其他較小的ZK系統、或其他類型的字節碼VM在驗證上的獨特之處。在本文中，我們將深入討論在驗證zkWasm記憶體子系統時所遇到的一些技術要點。記憶體是zkVM最獨特的部分，處理好這一點對所有其他zkVM的驗證都至關重要。
形式化驗證：虛擬機器（VM）對ZK虛擬機器（zkVM）
我們的最終目標是驗證zkWasm的正確性，其與普通的字節碼解釋器（VM，例如以太坊節點所使用的EVM解釋器）的正確性定理相似。亦即，解釋器的每一執行步驟都與基於該語言操作語意的合法步驟相對應。如下圖所示，如果字節碼解釋器的資料結構目前狀態為SL，且該狀態在Wasm機器的高階規格中被標記為狀態SH，那麼當解釋器步進到狀態SL'時，必須存在一個對應的合法高級狀態SH'，且Wasm規範中規定了SH必須步進到SH'。
同樣地，zkVM也有一個類似的正確性定理：zkWasm執行表中新的每一行都與一個基於該語言操作語義的合法步驟相對應。如下圖所示，如果執行表中某行資料結構的目前狀態是SR，且該狀態在Wasm機器的高階規格中表示為狀態SH，那麼執行表的下一行狀態SR'必須對應一個高階狀態SH' ，且Wasm規範中規定了SH必須步進到SH'。
由此可見，無論是在VM或zkVM中，高階狀態和Wasm步驟的規範是一致的，因此可以藉鏡先前對程式語言解釋器或編譯器的驗證經驗。而zkVM驗證的特殊之處在於其構成系統低階狀態的資料結構類型。
首先，如我們在先前的文章中所述，zk證明器在本質上是對大素數取模的整數運算，而Wasm規範和普通解釋器處理的是32位元或64位元整數。 zkVM實作的大部分內容都涉及到此，因此，在驗證中也需要做相應的處理。然而，這是一個「本地局部」問題：因為需要處理算術運算，每行程式碼變得更複雜，但程式碼和證明的整體結構並沒有改變。
另一個主要的區別是如何處理動態大小的資料結構。在常規的字節碼解釋器中，記憶體、資料堆疊和呼叫堆疊都被實作為可變資料結構，同樣的，Wasm規範將記憶體表示為具有get/set方法的資料類型。例如，Geth的EVM解釋器有一個Memory資料類型，它被實作為表示物理記憶體的位元組數組，並透過Set32和GetPtr方法寫入和讀取。為了實作一條記憶體儲存指令，Geth呼叫Set32來修改實體記憶體。
func opMstore(pc *uint64, interpreter *EVMInterpreter, scope *ScopeContext) ([]byte, error) { // pop value of the stack mStart, val := scope.Stack.pop(), scope.Stack.pop() scope.Memory.Set32(mStart.Uint64(), &val) return nil, nil}
在上述解釋器的正確性證明中，我們在對解釋器中的具體內存和在規範中的抽象內存進行賦值之後，證明其高級狀態和低級狀態相互匹配，這相對來說是比較容易的。
然而，對於zkVM而言，情況將變得更加複雜。
zkWasm的記憶體表和記憶體抽象層
在zkVM中，執行表上有用於固定大小資料的資料列（類似CPU中的暫存器），但它不能用來處理動態大小的資料結構，這些資料結構要透過尋找輔助表來實現。 zkWasm的執行表有一個EID列，該列的取值為1、2、3…，並且有記憶體表和跳表兩個輔助表，分別用於表示記憶體資料和呼叫堆疊。
以下是一個提款程式的實作範例：
int balance, amount;void main () {balance = 100; amount = 10;balance -= amount; // withdraw}
執行表的內容和結構相當簡單。它有6個執行步驟（EID1到6），每個步驟都有一行列出其操作碼（opcode），如果該指令是記憶體讀取或寫入，則還會列出其位址和資料：
記憶體表中的每一行都包含位址、資料、起始EID和終止EID。起始EID是寫入該資料到該位址的執行步驟的EID，終止EID是下一個將會寫入該位址的執行步驟的EID。 （它還包含一個計數，我們稍後將詳細討論。）對於Wasm記憶體讀取指令電路，其使用查找限制來確保表中存在一個合適的表項，使得讀取指令的EID在起始到終止的範圍內。 （類似地，跳轉表的每一行對應於呼叫堆疊的一幀，每行均標有創建它的呼叫指令步驟的EID。）
這個記憶體系統與常規VM解釋器的差異很大：記憶體表不是逐步更新的可變內存，而是包含整個執行軌跡中所有記憶體存取的歷史記錄。為了簡化程式設計師的工作，zkWasm提供了一個抽象層，透過兩個便捷入口函數來實現。分別是：
alloc_memory_table_lookup_write_cell
和
Alloc_memory_table_lookup_read_cell
其參數如下：
例如，zkWasm 中實作記憶體儲存指令的程式碼包含了一次對write alloc函數的呼叫：
let memory_table_lookup_heap_write1 = allocator .alloc_memory_table_lookup_write_cell_with_value( "store write res1", constraint_builder, eid, move |____| constant_from!(LocationTypeHeapd expation04) | ___| constant_from!(0), // is 32-bit move |____| constant_from!(1), // (always) enabled );letstore_value_in_heap1=memory_table_lookup_heap_write1.value_cell;
alloc函數負責處理表之間的查找約束以及將當前eid與記憶體表條目相關聯的算術約束。由此，程式設計師可以將這些表看作普通內存，並且在程式碼執行之後store_value_in_heap1的值已被賦給了load_block_index位址。
類似地，記憶體讀取指令使用read_alloc函數實作。在上面的範例執行序列中，每個載入指令都有一個讀取約束，每個儲存指令都有一個寫入約束，每個約束都由記憶體表中的一個條目所滿足。
形式化驗證的結構應與被驗證軟體中所使用的抽象相對應，使得證明可以遵循與程式碼相同的邏輯。對於zkWasm，這意味著我們需要將記憶體表電路和「alloc read/write cell」函數作為一個模組來進行驗證，其介面則像是可變記憶體。給定這樣的介面後，每個指令電路的驗證可以以類似於常規解釋器的方式進行，而額外的ZK複雜性則被封裝在記憶體子系統模組中。
在驗證中，我們具體實現了「內存表其實可以被看作是一個可變資料結構」這個想法。亦即，編寫函數memory_at type，其完整掃描記憶體表、並建立對應的位址資料映射。 （這裡變數type的取值範圍為三種不同類型的Wasm記憶體資料：堆疊、資料堆疊和全域變數。）而後，我們證明由alloc函數產生的記憶體限制等價於使用set和get函數對應位址資料映射所進行的資料變更。我們可以證明：
- 對於每一eid，如果以下約束成立
memory_table_lookup_read_celleidtypeoffsetvalue
則
get(memory_ateidtype)offset=Somevalue
- 並且，如果以下約束成立
memory_table_lookup_write_cell eid type offset value
則
memory_at (eid+1) type = set (memory_at eid type) offset value
在此之後，每個指令的驗證可以建立在對位址資料映射的get和set操作之上，這與非ZK字節碼解釋器相似。
zkWasm的記憶體寫入計數機制
不過，上述的簡化描述並未揭示記憶體表和跳轉表的全部內容。在zkVM的框架下，這些表可能會受到攻擊者的操控，攻擊者可以輕易地透過插入一行資料來操縱記憶體載入指令，傳回任意數值。
以提款程序為例，攻擊者有機會在提款操作前，透過偽造一個$110的記憶體寫入操作，將虛假資料注入到帳戶餘額中。這個過程可以透過在記憶體表中添加一行數據，並修改記憶體表和執行表中現有單元格的數值來實現。這將導致其可以進行「免費」的提款操作，因為帳戶餘額在操作後將仍然保持在$100。
為確保記憶體表（和跳躍表）僅包含由實際執行的記憶體寫入（和呼叫及返回）指令產生的有效條目，zkWasm採用了一種特殊的計數機制來監控條目數量。具體來說，記憶體表設有一個專門的列，用於持續追蹤記憶體寫入條目的總數。同時，執行表中也包含了一個計數器，用於統計每個指令預期進行的記憶體寫入操作的次數。透過設定一個相等約束，從而確保這兩個計數是一致的。這種方法的邏輯十分直觀：每當記憶體進行寫入操作，就會被計數一次，而記憶體表中相應地也應有一筆記錄。因此，攻擊者無法在記憶體表中插入任何額外的條目。
上面的邏輯陳述有點模糊，在機械化證明的過程中，需要使其更精確。首先，我們需要修正前述記憶體寫入引理的陳述。我們定義函數mops_at eid type，對具有給定eid和type的記憶體表條目計數（大多數指令將在一個eid處建立0或1個條目）。該定理的完整陳述有一個額外的前提條件，指出沒有虛假的內存表條目：
如果以下約束成立
(memory_table_lookup_write_celleidtypeoffsetvalue)
並且以下新增約束成立
(mops_ateidtype)=1
則
(memory_at(eid+1)type)=set(memory_ateidtype)offsetvalue
這要求我們的驗證比前述情況更精確。 僅從相等約束條件中得出記憶體表條目總數等於執行中的總記憶體寫入次數並不足以完成驗證。為了證明指令的正確性，我們需要知道每個指令對應了正確數目的記憶體表條目。例如，我們需要排除攻擊者是否可能在執行序列中略去某條指令的記憶體表條目，並為另一個無關指令建立一個惡意的新記憶體表條目。
為了證明這一點，我們採用了從上到下的方式，對給定指令對應的記憶體表條目數量進行限制，這包括了三個步驟。首先，我們根據指令類型為執行序列中的指令預估了所應該建立的條目數量。我們稱從第i 個步驟到執行結束的預期寫入次數為instructions_mops i，並稱從第i 條指令到執行結束在記憶體表中的對應條目數為cum_mops (eid i)。透過分析每個指令的查找約束，我們可以證明其所建立的條目不少於預期，從而可以得出所追蹤的每一段[i ... numRows] 所創建的條目不少於預期：
Lemma cum_mops_bound': forall ni, 0 ≤ i -> i + Z.of_nat n = etable_numRow ->MTable.cum_mops(etable_valueseid_celli)(max_eid+1)≥instructions_mops'in.
其次，如果能證明表中的條目數不多於預期，那麼它就恰好具有正確數量的條目，而這一點是顯而易見的。
Lemma cum_mops_equal' : forall ni, 0 ≤ i -> i + Z.of_nat n = etable_numRow -> MTable.cum_mops (etable_values eid_cell i) (max_eid+1) ≤ instructions_mops' in -->MTabletable_pse-cidue(n_val 1)=instructions_mops'in.
現在進行第三步。我們的正確性定理宣告：對於任意n，cum_mops和instructions_mops在表中從第n行到末尾的部分總是一致的：
Lemma cum_mops_equal : forall n, 0 <= Z.of_nat n < etable_numRow ->MTable.cum_mops(etable_valueseid_cell(Z.of_natn))(max_eid+1)=instructions_mops(Z.of_natn)
透過對n進行歸納總結來完成驗證。表中的第一行是zkWasm的等式約束，表示記憶體表中條目的總數是正確的，即cum_mops 0 = instructions_mops 0。對於接下來的行，歸納假設告訴我們：
cum_mopsn=instructions_mopsn
並且我們希望證明
cum_mops (n+1) = instructions_mops (n+1)
注意此處
cum_mops n = mop_at n + cum_mops (n+1)
並且
instructions_mops n = instruction_mops n + instructions_mops (n+1)
因此，我們可以得到
mops_at n + cum_mops (n+1) = instruction_mops n + instructions_mops (n+1)
先前，我們已經證明了每條指令將創造不少於預期數量的條目，例如
mops_at n ≥ instruction_mops n.
所以可以得出
cum_mops (n+1) ≤ instructions_mops (n+1)
這裡我們需要應用上述第二個引理。
如此詳細地說明證明過程，是形式化驗證的典型特徵，也是驗證特定程式碼片段通常比編寫它需要更長時間的原因。然而這樣做是否值得？在這裡的情況下是值得的，因為我們在證明的過程中的確發現了一個跳表計數機制的關鍵錯誤。先前的文章中已經詳細描述了這個錯誤——總結來說，舊版本的程式碼同時計入了呼叫和返回指令，而攻擊者可以透過在執行序列中添加額外的返回指令，來為偽造的跳躍表條目騰出空間。儘管不正確的計數機制可以滿足對每條調用和返回指令都計數的直覺，但當我們試圖將這種直覺細化為更精確的定理陳述時，問題就會凸顯出來。
使證明過程模組化
從上面的討論中，我們可以看到在關於每個指令電路的證明和關於執行表的計數列的證明之間存在著一種循環依賴關係。要證明指令電路的正確性，我們需要對其中的記憶體寫入進行推理；即需要知道在特定EID處內存表條目的數量、以及需要證明執行表中的內存寫入操作計數是正確的；而這又需要證明每條指令至少執行了最少數量的記憶體寫入操作。
此外，還有一個需要考慮的因素，zkWasm專案相當龐大，因此驗證工作需要模組化，以便多位驗證工程師分工處理。因此，對計數機制的證明解構時需要特別注意其複雜度。例如，對於LocalGet指令，有兩個定理如下：
Theorem opcode_mops_correct_local_get : forall i, 0 <= i -> etable_values eid_cell i > 0 -> opcode_mops_correct LocalGet i.
Theorem LocalGetOp_correct : forall i st y xs, 0 <= i -> etable_values enabled_cell i = 1 -> mops_at_correct i -> etable_values (ops_cell LocalGet) i = 1 -> state_rel ist - wasues (opsn_valGet) i = 1 -> state_rel ist - wass_relset_sf -states_rel tablest -> state_rel. i) > 1 -> nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = Some y ->state_rel(i+1)(update_stack(incr_iidst)(y::xs)).
第一個定理聲明
opcode_mops_correct LocalGet i
展開定義後，表示指令在第i行至少建立了一個記憶體表條目（數字1是在zkWasm的LocalGet操作碼規格中指定的）。
第二個定理是該指令的完整正確性定理，它引用
mops_at_correct i
作為假設，這意味著該指令準確地創建了一個記憶體表條目。
驗證工程師可以分別獨立證明這兩個定理，然後將它們與關於執行表的證明結合起來，從而證得整個系統的正確性。值得注意的是，所有針對單一指令的證明都可以在讀取/寫入約束的層面上進行，而無須了解記憶體表的具體實作。因此，項目分為三個可以獨立處理的部分。
總結
逐行驗證zkVM的電路與驗證其他領域的ZK應用並沒有本質區別，因為它們都需要對算術約束進行類似的推理。從高層來看，zkVM的驗證需要用到許多運用於程式語言解釋器和編譯器形式化驗證的方法。這裡主要的差別在於動態大小的虛擬機器狀態。然而，透過精心建構驗證結構來匹配實作中所使用的抽象層，這些差異的影響可以被最小化，從而使得每條指令都可以像對常規解釋器那樣，基於get-set介面來進行獨立的模組化驗證。
