零知識證明的先進形式化驗證：如何證明零知識內存

在本文中，我們將深入討論在驗證 zkWasm 記憶體子系統時所遇到的一些技術要點。記憶體是 zkVM 最獨特的部分，處理好這一點對所有其他 zkVM 的驗證都至關重要。

作者：Certik

封面： Photo by Steve Johnson on Unsplash

在關於零知識證明的先進形式化驗證的系列文章中，我們已經討論瞭如何驗證 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!(LocationType::Heap as u64),
  move |meta| load_block_index.expr(meta),   // address
  move |____| constant_from!(0),             // is 32-bit
  move |____| constant_from!(1),             // (always) enabled
    );
let store_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_cell eid type offset value

則

get (memory_at eid type) offset = Some value

• 並且，如果以下約束成立

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_cell eid type offset value)

並且以下新增約束成立

(mops_at eid type) = 1

則

(memory_at(eid+1) type) = set (memory_at eid type) offset value

這要求我們的驗證比前述情況更精確。 僅從相等約束條件中得出記憶體表條目總數等於執行中的總記憶體寫入次數並不足以完成驗證。為了證明指令的正確性，我們需要知道每個指令對應了正確數目的記憶體表條目。例如，我們需要排除攻擊者是否可能在執行序列中略去某條指令的記憶體表條目，並為另一個無關指令建立一個惡意的新記憶體表條目。

為了證明這一點，我們採用了從上到下的方式，對給定指令對應的記憶體表條目數量進行限制，這包括了三個步驟。首先，我們根據指令類型為執行序列中的指令預估了所應該建立的條目數量。我們稱從第 i 個步驟到執行結束的預期寫入次數為 instructions_mops i，並稱從第 i 條指令到執行結束在記憶體表中的對應條目數為 cum_mops (eid i)。透過分析每個指令的查找約束，我們可以證明其所建立的條目不少於預期，從而可以得出所追蹤的每一段 [i ... numRows] 所創建的條目不少於預期：

Lemma cum_mops_bound': forall n i,
  0 ≤ i ->
  i + Z.of_nat n = etable_numRow ->
  MTable.cum_mops (etable_values eid_cell i) (max_eid+1) ≥ instructions_mops' i n.

其次，如果能證明表中的條目數不多於預期，那麼它就恰好具有正確數量的條目，而這一點是顯而易見的。

Lemma cum_mops_equal' : forall n i,
    0 ≤ i ->
    i + Z.of_nat n = etable_numRow ->
    MTable.cum_mops (etable_values eid_cell i) (max_eid+1) ≤ instructions_mops' i n ->
    MTable.cum_mops (etable_values eid_cell i) (max_eid+1)  = instructions_mops' i n.

現在進行第三步。我們的正確性定理宣告：對於任意 n，cum_mops 和 instructions_mops 在表中從第 n 行到末尾的部分總是一致的：

Lemma cum_mops_equal : forall n,
    0 <= Z.of_nat n < etable_numRow ->
  MTable.cum_mops (etable_values eid_cell (Z.of_nat n)) (max_eid+1) = instructions_mops (Z.of_nat n)

透過對 n 進行歸納總結來完成驗證。表中的第一行是 zkWasm 的等式約束，表示記憶體表中條目的總數是正確的，即 cum_mops 0 = instructions_mops 0。對於接下來的行，歸納假設告訴我們：

cum_mops n = instructions_mops n

並且我們希望證明

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 i st ->
  wasm_stack st = xs ->
  (etable_values offset_cell i) > 1 ->
  nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = Some y ->
  state_rel (i+1) (update_stack (incr_iid st) (y :: xs)).

第一個定理聲明

opcode_mops_correct LocalGet i

展開定義後，表示指令在第 i 行至少建立了一個記憶體表條目（數字 1 是在 zkWasm 的 LocalGet 操作碼規格中指定的）。

第二個定理是該指令的完整正確性定理，它引用 

mops_at_correct i

作為假設，這意味著該指令準確地創建了一個記憶體表條目。

驗證工程師可以分別獨立證明這兩個定理，然後將它們與關於執行表的證明結合起來，從而證得整個系統的正確性。值得注意的是，所有針對單一指令的證明都可以在讀取/寫入約束的層面上進行，而無須了解記憶體表的具體實作。因此，項目分為三個可以獨立處理的部分。

總結

逐行驗證 zkVM 的電路與驗證其他領域的 ZK 應用並沒有本質區別，因為它們都需要對算術約束進行類似的推理。從高層來看，zkVM 的驗證需要用到許多運用於程式語言解釋器和編譯器形式化驗證的方法。這裡主要的差別在於動態大小的虛擬機器狀態。然而，透過精心建構驗證結構來匹配實作中所使用的抽象層，這些差異的影響可以被最小化，從而使得每條指令都可以像對常規解釋器那樣，基於 get-set 介面來進行獨立的模組化驗證。

免責聲明：作為區塊鏈資訊平台，本站所發布文章僅代表作者及來賓個人觀點，與 Web3Caff 立場無關。文章內的資訊僅供參考，均不構成任何投資建議及要約，並請您遵守所在國家或地區的相關法律法規。