在關(guān)于零知識證明的先進形式化驗證的系列博客中，我們已經(jīng)討論了如何驗證 ZK 指令以及對兩個 ZK 漏洞的深度剖析。正如在公開報告和代碼庫中所顯示的，通過形式化驗證每一條 zkWasm 指令，我們找到并修復(fù)了每一個漏洞，從而能夠完全驗證整個 zkWasm 電路的技術(shù)安全性和正確性。

盡管我們已展示了驗證一條 zkWasm 指令的過程，并介紹了相關(guān)的項目初步概念，但熟悉形式化驗證讀者可能更想了解 zkVM 與其他較小的 ZK 系統(tǒng)、或其他類型的字節(jié)碼 VM 在驗證上的獨特之處。在本文中，我們將深入討論在驗證 zkWasm 內(nèi)存子系統(tǒng)時所遇到的一些技術(shù)要點。內(nèi)存是 zkVM 最為獨特的部分，處理好這一點對所有其他 zkVM 的驗證都至關(guān)重要。

形式化驗證：虛擬機（VM）對 ZK 虛擬機（zkVM）

我們的最終目標(biāo)是驗證 zkWasm 的正確性，其與普通的字節(jié)碼解釋器（VM，例如以太坊節(jié)點所使用的 EVM 解釋器）的正確性定理相似。亦即，解釋器的每一執(zhí)行步驟都與基于該語言操作語義的合法步驟相對應(yīng)。如下圖所示，如果字節(jié)碼解釋器的數(shù)據(jù)結(jié)構(gòu)當(dāng)前狀態(tài)為 SL，且該狀態(tài)在 Wasm 機器的高級規(guī)范中被標(biāo)記為狀態(tài) SH，那么當(dāng)解釋器步進到狀態(tài) SL'時，必須存在一個對應(yīng)的合法高級狀態(tài) SH'，且 Wasm 規(guī)范中規(guī)定了 SH 必須步進到 SH'。

同樣地，zkVM 也有一個類似的正確性定理：zkWasm 執(zhí)行表中新的每一行都與一個基于該語言操作語義的合法步驟相對應(yīng)。如下圖所示，如果執(zhí)行表中某行數(shù)據(jù)結(jié)構(gòu)的當(dāng)前狀態(tài)是 SR，且該狀態(tài)在 Wasm 機器的高級規(guī)范中表示為狀態(tài) SH，那么執(zhí)行表的下一行狀態(tài) SR'必須對應(yīng)一個高級狀態(tài) SH'，且 Wasm 規(guī)范中規(guī)定了 SH 必須步進到 SH'。

由此可見，無論是在 VM 還是 zkVM 中，高級狀態(tài)和 Wasm 步驟的規(guī)范是一致的，因此可以借鑒先前對編程語言解釋器或編譯器的驗證經(jīng)驗。而 zkVM 驗證的特殊之處在于其構(gòu)成系統(tǒng)低級狀態(tài)的數(shù)據(jù)結(jié)構(gòu)類型。

首先，如我們在之前的博客文章中所述，zk 證明器在本質(zhì)上是對大素數(shù)取模的整數(shù)運算，而 Wasm 規(guī)范和普通解釋器處理的是 32 位或 64 位整數(shù)。zkVM 實現(xiàn)的大部分內(nèi)容都涉及到此，因此，在驗證中也需要做相應(yīng)的處理。然而，這是一個“本地局部”問題：因為需要處理算術(shù)運算，每行代碼變得更復(fù)雜，但代碼和證明的整體結(jié)構(gòu)并沒有改變。

另一個主要的區(qū)別是如何處理動態(tài)大小的數(shù)據(jù)結(jié)構(gòu)。在常規(guī)的字節(jié)碼解釋器中，內(nèi)存、數(shù)據(jù)棧和調(diào)用棧都被實現(xiàn)為可變數(shù)據(jù)結(jié)構(gòu)，同樣的，Wasm 規(guī)范將內(nèi)存表示為具有 get/set 方法的數(shù)據(jù)類型。例如，Geth 的 EVM 解釋器有一個`Memory`數(shù)據(jù)類型，它被實現(xiàn)為表示物理內(nèi)存的字節(jié)數(shù)組，并通過`Set 32 `和`GetPtr`方法寫入和讀取。為了實現(xiàn)一條內(nèi)存存儲指令，Geth 調(diào)用`Set 32 `來修改物理內(nèi)存。

func opMstore(pc *uint 64, interpreter *EVMInterpreter, scope *ScopeContext) ([]byte, error) {

// pop value of the stack

mStart, val := scope.Stack.pop(), scope.Stack.pop()

scope.Memory.Set 32(mStart.Uint 64(), &val)

return nil, nil

}

在上述解釋器的正確性證明中，我們在對解釋器中的具體內(nèi)存和在規(guī)范中的抽象內(nèi)存進行賦值之后，證明其高級狀態(tài)和低級狀態(tài)相互匹配，這相對來說是比較容易的。

然而，對于 zkVM 而言，情況將變得更加復(fù)雜。

zkWasm 的內(nèi)存表和內(nèi)存抽象層

在 zkVM 中，執(zhí)行表上有用于固定大小數(shù)據(jù)的列（類似于 CPU 中的寄存器），但它不能用來處理動態(tài)大小的數(shù)據(jù)結(jié)構(gòu)，這些數(shù)據(jù)結(jié)構(gòu)要通過查找輔助表來實現(xiàn)。zkWasm 的執(zhí)行表有一個 EID 列，該列的取值為 1、 2、 3 ……，并且有內(nèi)存表和跳轉(zhuǎn)表兩個輔助表，分別用于表示內(nèi)存數(shù)據(jù)和調(diào)用棧。

以下是一個提款程序的實現(xiàn)示例：

int balance, amount;

void main () {

balance = 100;

  amount = 10;

balance -= amount; // withdraw

}

執(zhí)行表的內(nèi)容和結(jié)構(gòu)相當(dāng)簡單。它有 6 個執(zhí)行步驟（EID 1 到 6），每個步驟都有一行列出其操作碼（opcode），如果該指令是內(nèi)存讀取或?qū)懭耄瑒t還會列出其地址和數(shù)據(jù)：

內(nèi)存表中的每一行都包含地址、數(shù)據(jù)、起始 EID 和終止 EID。起始 EID 是寫入該數(shù)據(jù)到該地址的執(zhí)行步驟的 EID，終止 EID 是下一個將會寫入該地址的執(zhí)行步驟的 EID。（它還包含一個計數(shù)，我們稍后詳細(xì)討論。）對于 Wasm 內(nèi)存讀取指令電路，其使用查找約束來確保表中存在一個合適的表項，使得讀取指令的 EID 在起始到終止的范圍內(nèi)。（類似地，跳轉(zhuǎn)表的每一行對應(yīng)于調(diào)用棧的一幀，每行均標(biāo)有創(chuàng)建它的調(diào)用指令步驟的 EID。）

這個內(nèi)存系統(tǒng)與常規(guī) VM 解釋器的區(qū)別很大：內(nèi)存表不是逐步更新的可變內(nèi)存，而是包含整個執(zhí)行軌跡中所有內(nèi)存訪問的歷史記錄。為了簡化程序員的工作，zkWasm 提供了一個抽象層，通過兩個便捷入口函數(shù)來實現(xiàn)。分別是：

alloc_memory_table_lookup_write_cell

和

Alloc_memory_table_lookup_read_cell

其參數(shù)如下：

例如，zkWasm 中實現(xiàn)內(nèi)存存儲指令的代碼包含了一次對’write alloc’函數(shù)的調(diào)用：

let memory_table_lookup_heap_write1 = allocator

    .alloc_memory_table_lookup_write_cell_with_value(

"store write res 1",

constraint_builder,

eid,

move |____| constant_from!(LocationType::Heap as u 64),

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`函數(shù)負(fù)責(zé)處理表之間的查找約束以及將當(dāng)前`eid`與內(nèi)存表條目相關(guān)聯(lián)的算術(shù)約束。由此，程序員可以將這些表看作普通內(nèi)存，并且在代碼執(zhí)行之后 `store_value_in_heap1`的值已被賦給了 `load_block_index` 地址。

類似地，內(nèi)存讀取指令使用`read_alloc`函數(shù)實現(xiàn)。在上面的示例執(zhí)行序列中，每條加載指令有一個讀取約束，每條存儲指令有一個寫入約束，每個約束都由內(nèi)存表中的一個條目所滿足。

mtable_lookup_write(row 1.eid, row 1.store_addr, row 1.store_value)

                       ? (row 1.eid= 1 ∧ row 1.store_addr=balance ∧ row 1.store_value= 100 ∧ ...)

mtable_lookup_write(row 2.eid, row 2.store_addr, row 2.store_value)

                      ? (row 2.eid= 2 ∧ row 2.store_addr=amount ∧ row 2.store_value= 10 ∧ ...)

mtable_lookup_read(row 3.eid, row 3.load_addr, row 3.load_value)

                      ? ( 2<row 3.eid≤ 6 ∧ row 3.load_addr=amount ∧ row 3.load_value= 100 ∧ ...)

mtable_lookup_read(row 4.eid, row 4.load_addr, row 4.load_value)

                      ? ( 1<row 4.eid≤ 6 ∧ row 4.load_addr=balance ∧ row 4.load_value= 10 ∧ ...)

mtable_lookup_write(row 6.eid, row 6.store_addr, row 6.store_value)

                      ? (row 6.eid= 6 ∧ row 6.store_addr=balance ∧ row 6.store_value= 90 ∧ ...)

形式化驗證的結(jié)構(gòu)應(yīng)與被驗證軟件中所使用的抽象相對應(yīng)，使得證明可以遵循與代碼相同的邏輯。對于 zkWasm，這意味著我們需要將內(nèi)存表電路和“alloc read/write cell”函數(shù)作為一個模塊來進行驗證，其接口則像可變內(nèi)存。給定這樣的接口后，每條指令電路的驗證可以以類似于常規(guī)解釋器的方式進行，而額外的 ZK 復(fù)雜性則被封裝在內(nèi)存子系統(tǒng)模塊中。

在驗證中，我們具體實現(xiàn)了“內(nèi)存表其實可以被看作是一個可變數(shù)據(jù)結(jié)構(gòu)”這個想法。亦即，編寫函數(shù) `memory_at type`，其完整掃描內(nèi)存表、并構(gòu)建相應(yīng)的地址數(shù)據(jù)映射。（這里變量 `type` 的取值范圍為三種不同類型的 Wasm 內(nèi)存數(shù)據(jù)：堆、數(shù)據(jù)棧和全局變量。）而后，我們證明由 alloc 函數(shù)所生成的內(nèi)存約束等價于使用 set 和 get 函數(shù)對相應(yīng)地址數(shù)據(jù)映射所進行的數(shù)據(jù)變更。我們可以證明：

• 對于每一 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

    在此之后，每條指令的驗證可以建立在對地址數(shù)據(jù)映射的 get 和 set 操作之上，這與非 ZK 字節(jié)碼解釋器相類似。

    zkWasm 的內(nèi)存寫入計數(shù)機制

    不過，上述的簡化描述并未揭示內(nèi)存表和跳轉(zhuǎn)表的全部內(nèi)容。在 zkVM 的框架下，這些表可能會受到攻擊者的操控，攻擊者可以輕易地通過插入一行數(shù)據(jù)來操縱內(nèi)存加載指令，返回任意數(shù)值。

    以提款程序為例，攻擊者有機會在提款操作前，通過偽造一個$ 110 的內(nèi)存寫入操作，將虛假數(shù)據(jù)注入到賬戶余額中。這一過程可以通過在內(nèi)存表中添加一行數(shù)據(jù)，并修改內(nèi)存表和執(zhí)行表中現(xiàn)有單元格的數(shù)值來實現(xiàn)。這將導(dǎo)致其可以進行“免費”的提款操作，因為賬戶余額在操作后將仍然保持在$ 100 。

    為確保內(nèi)存表（和跳轉(zhuǎn)表）僅包含由實際執(zhí)行的內(nèi)存寫入（和調(diào)用及返回）指令生成的有效條目，zkWasm 采用了一種特殊的計數(shù)機制來監(jiān)控條目數(shù)量。具體來說，內(nèi)存表設(shè)有一個專門的列，用以持續(xù)追蹤內(nèi)存寫入條目的總數(shù)。同時，執(zhí)行表中也包含了一個計數(shù)器，用于統(tǒng)計每個指令預(yù)期進行的內(nèi)存寫入操作的次數(shù)。通過設(shè)置一個相等約束，從而確保這兩個計數(shù)是一致的。這種方法的邏輯十分直觀：每當(dāng)內(nèi)存進行寫入操作，就會被計數(shù)一次，而內(nèi)存表中相應(yīng)地也應(yīng)有一條記錄。因此，攻擊者無法在內(nèi)存表中插入任何額外的條目。

    上面的邏輯陳述有點模糊，在機械化證明的過程中，需要使其更加精確。首先，我們需要修正前述內(nèi)存寫入引理的陳述。我們定義函數(shù)`mops_at eid type`，對具有給定`eid`和`type`的內(nèi)存表條目計數(shù)（大多數(shù)指令將在一個 eid 處創(chuàng)建 0 或 1 個條目）。該定理的完整陳述有一個額外的前提條件，指出沒有虛假的內(nèi)存表條目：

    如果以下約束成立

     (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

    這要求我們的驗證比前述情況更精確。 僅僅從相等約束條件中得出內(nèi)存表條目總數(shù)等于執(zhí)行中的總內(nèi)存寫入次數(shù)并不足以完成驗證。為了證明指令的正確性，我們需要知道每條指令對應(yīng)了正確數(shù)目的內(nèi)存表條目。例如，我們需要排除攻擊者是否可能在執(zhí)行序列中略去某條指令的內(nèi)存表條目，并為另一條無關(guān)指令創(chuàng)建一個惡意的新內(nèi)存表條目。

    為了證明這一點，我們采用了由上至下的方式，對給定指令對應(yīng)的內(nèi)存表條目數(shù)量進行限制，這包括了三個步驟。首先，我們根據(jù)指令類型為執(zhí)行序列中的指令預(yù)估了所應(yīng)該創(chuàng)建的條目數(shù)量。我們稱從第 i 個步驟到執(zhí)行結(jié)束的預(yù)期寫入次數(shù)為`instructions_mops i`，并稱從第 i 條指令到執(zhí)行結(jié)束在內(nèi)存表中的相應(yīng)條目數(shù)為`cum_mops (eid i)`。通過分析每條指令的查找約束，我們可以證明其所創(chuàng)建的條目不少于預(yù)期，從而可以得出所跟蹤的每一段 [i... numRows] 所創(chuàng)建的條目不少于預(yù)期：

    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.

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

    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.

    現(xià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 進行歸納總結(jié)來完成驗證。表中的第一行是 zkWasm 的等式約束，表明內(nèi)存表中條目的總數(shù)是正確的，即 cum_mops 0 = instructions_mops 0 。對于接下來的行，歸納假設(shè)告訴我們：

    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)

    此前，我們已經(jīng)證明了每條指令將創(chuàng)造不少于預(yù)期數(shù)量的條目，例如

    mops_at n ≥ instruction_mops n.

    所以可以得出

    cum_mops (n  1) ≤ instructions_mops (n  1)

    這里我們需要應(yīng)用上述第二個引理。

    （用類似的引理對跳轉(zhuǎn)表進行驗證，可證得每條調(diào)用指令都能準(zhǔn)確地產(chǎn)生一個跳轉(zhuǎn)表條目，這個證明技術(shù)因此普遍適用。然而，我們?nèi)孕枰M一步的驗證工作來證明返回指令的正確性。返回的 eid 與創(chuàng)建調(diào)用幀的調(diào)用指令的 eid 是不同的，因此我們還需要一個附加的不變性質(zhì)，用來聲明 eid 數(shù)值在執(zhí)行序列中是單向遞增的。）

    如此詳細(xì)地說明證明過程，是形式化驗證的典型特征，也是驗證特定代碼片段通常比編寫它需要更長時間的原因。然而這樣做是否值得？在這里的情況下是值得的，因為我們在證明的過程中的確發(fā)現(xiàn)了一個跳轉(zhuǎn)表計數(shù)機制的關(guān)鍵錯誤。之前的文章中已經(jīng)詳細(xì)描述了這個錯誤——總結(jié)來說，舊版本的代碼同時計入了調(diào)用和返回指令，而攻擊者可以通過在執(zhí)行序列中添加額外的返回指令，來為偽造的跳轉(zhuǎn)表條目騰出空間。盡管不正確的計數(shù)機制可以滿足對每條調(diào)用和返回指令都計數(shù)的直覺，但當(dāng)我們試圖將這種直覺細(xì)化為更精確的定理陳述時，問題就會凸顯出來。

    使證明過程模塊化

    從上面的討論中，我們可以看到在關(guān)于每條指令電路的證明和關(guān)于執(zhí)行表的計數(shù)列的證明之間存在著一種循環(huán)依賴關(guān)系。要證明指令電路的正確性，我們需要對其中的內(nèi)存寫入進行推理；即需要知道在特定 EID 處內(nèi)存表條目的數(shù)量、以及需要證明執(zhí)行表中的內(nèi)存寫入操作計數(shù)是正確的；而這又需要證明每條指令至少執(zhí)行了最少數(shù)量的內(nèi)存寫入操作。

    此外，還有一個需要考慮的因素，zkWasm 項目相當(dāng)龐大，因此驗證工作需要模塊化，以便多位驗證工程師分工處理。因此，對計數(shù)機制的證明解構(gòu)時需要特別注意其復(fù)雜性。例如，對于 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 行至少創(chuàng)建了一個內(nèi)存表條目（數(shù)字 1 是在 zkWasm 的 LocalGet 操作碼規(guī)范中指定的）。

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

    mops_at_correct i 

    作為假設(shè)，這意味著該指令準(zhǔn)確地創(chuàng)建了一個內(nèi)存表條目。

    驗證工程師可以分別獨立地證明這兩個定理，然后將它們與關(guān)于執(zhí)行表的證明結(jié)合起來，從而證得整個系統(tǒng)的正確性。值得注意的是，所有針對單個指令的證明都可以在讀取/寫入約束的層面上進行，而無須了解內(nèi)存表的具體實現(xiàn)。因此，項目分為三個可以獨立處理的部分。

    總結(jié)

    逐行驗證 zkVM 的電路與驗證其他領(lǐng)域的 ZK 應(yīng)用并沒有本質(zhì)區(qū)別，因為它們都需要對算術(shù)約束進行類似的推理。從高層來看，對 zkVM 的驗證需要用到許多運用于編程語言解釋器和編譯器形式化驗證的方法。這里主要的區(qū)別在于動態(tài)大小的虛擬機狀態(tài)。然而，通過精心構(gòu)建驗證結(jié)構(gòu)來匹配實現(xiàn)中所使用的抽象層，這些差異的影響可以被最小化，從而使得每條指令都可以像對常規(guī)解釋器那樣，基于 get-set 接口來進行獨立的模塊化驗證。

AD：

鄭重聲明：本文版權(quán)歸原作者所有，轉(zhuǎn)載文章僅為傳播更多信息之目的，如作者信息標(biāo)記有誤，請第一時間聯(lián)系我們修改或刪除，多謝。