ゼロ知識証明の高度な形式的検証に関するこのブログ シリーズでは、 ZK 命令を検証する方法について説明し、 2 つの ZK 脆弱性について詳しく説明しました。すべての zkWasm 命令を正式に検証することで、公開レポートやコード ベースに示されているようにすべての脆弱性を発見して修正し、zkWasm 回路全体の技術的安全性と正確性を完全に検証できるようになりました。
zkWasm 命令を検証するプロセスを示し、関連プロジェクトの予備的な概念を紹介しましたが、形式的な検証に慣れている読者は、他の小規模な ZK システムや他のタイプのバイトコード VM による zkVM の検証を理解することに興味があるかもしれません。の上。この記事では、zkWasm メモリ サブシステムを検証する際に発生する技術的なポイントのいくつかについて詳しく説明します。メモリは zkVM の最もユニークな部分であり、これを処理することは他のすべての zkVM 検証にとって重要です。
正式な検証: 仮想マシン (VM) と ZK 仮想マシン (zkVM)
私たちの最終的な目標は、zkWasm の正確性を検証することです。これは、通常のバイトコード インタープリター (VM、イーサリアム ノードで使用される EVM インタープリターなど) の正確性定理と同様です。つまり、インタプリタの各実行ステップは、言語の操作セマンティクスに基づいた法的ステップに対応します。以下の図に示すように、バイトコード インタプリタのデータ構造の現在の状態が SL で、この状態が Wasm マシンの高レベル仕様で状態 SH としてマークされている場合、インタプリタが状態 SL にステップすると、対応する法的な高レベル状態 SH である必要があり、Wasm 仕様では SH が SH にステップする必要があると規定されています。
同様に、zkVM にも同様の正当性定理があります。つまり、zkWasm 実行テーブルの新しい行はそれぞれ、言語の操作セマンティクスに基づいた正当なステップに対応します。以下の図に示すように、実行テーブル内のデータ構造の行の現在の状態が SR であり、この状態が Wasm マシンの上位仕様で状態 SH として表現される場合、実行テーブルの次の行は高レベル状態 SH に対応する必要があり、Wasm 仕様では SH が SH にステップする必要があると規定されています。
つまり、高レベルの状態と Wasm ステップの仕様は VM であっても zkVM であっても一貫しているため、プログラミング言語インタープリターまたはコンパイラーを使用した以前の検証経験を活用できます。 zkVM 検証を特別なものにしているのは、システムの低レベルの状態を構成するデータ構造のタイプです。
まず、以前のブログ投稿で述べたように、zk 証明器は本質的に大きな素数を法とする整数演算ですが、Wasm 仕様と通常のインタプリタは 32 ビットまたは 64 ビットの整数を扱います。ほとんどの zkVM 実装にはこれが含まれるため、検証中に対応する処理も行う必要があります。ただし、これは「ローカル」問題です。処理する必要がある算術演算のため、コードの各行はより複雑になりますが、コードと証明の全体的な構造は変わりません。
もう 1 つの大きな違いは、動的にサイズ変更されたデータ構造がどのように処理されるかです。通常のバイトコード インタプリタでは、メモリ、データ スタック、およびコール スタックはすべて変更可能なデータ構造として実装されます。同様に、Wasm 仕様では get/set メソッドを使用してメモリをデータ型として表します。たとえば、Geth の EVM インタプリタには「Memory」データ型があり、物理メモリを表すバイト配列として実装され、「Set 32」および「GetPtr」メソッドを通じて書き込みおよび読み取りが行われます。メモリ ストア命令を実装するために、Geth は `Set 32` を呼び出して物理メモリを変更します。
func opMstore(pc *uint 64, インタプリタ *EVMInterpreter, スコープ *ScopeContext) ([]byte, error) {
// スタックの値をポップします
mStart、val :=scope.Stack.pop()、scope.Stack.pop()
スコープ.Memory.Set 32(mStart.Uint 64(), val)
nil、nil を返す
}
上記のインタプリタの正しさの証明では、インタプリタ内の具象メモリと仕様内の抽象メモリに値を代入した上で、その高レベルの状態と低レベルの状態が一致することを証明しました。これは比較的簡単です。
ただし、zkVM の場合、状況はさらに複雑になります。
zkWasm のメモリ テーブルとメモリ抽象化層
zkVM では、実行テーブル上に固定サイズのデータ用の列 (CPU のレジスタと同様) がありますが、これを使用して、補助テーブルをルックアップすることによって実装される動的サイズのデータ構造を処理することはできません。 zkWasm の実行テーブルには、値が 1、2、3... である EID 列があり、メモリ データとコール スタックをそれぞれ表すために使用される 2 つの補助テーブル、メモリ テーブルとジャンプ テーブルがあります。
以下は、引き出しプログラムの実装方法の例です。
int 残高、金額;
void main() {
残高 = 100;
金額 = 10;
残高 -= 金額; // 出金;
}
実行テーブルの内容と構造は非常に単純です。これには 6 つの実行ステップ (EID 1 ～ 6) があり、各ステップにはオペコードをリストする行があり、命令がメモリの読み取りまたは書き込みの場合はそのアドレスとデータをリストします。
メモリ テーブルの各行には、アドレス、データ、開始 EID、および終了 EID が含まれます。開始 EID は、このデータをこのアドレスに書き込む実行ステップの EID であり、終了 EID は、このアドレスに書き込む次の実行ステップの EID です。 (後で詳しく説明するカウントも含まれています。) Wasm メモリ読み取り命令回路の場合、ルックアップ制約を使用して、読み取り命令の EID がテーブル内に適切なエントリがあることを確認します。最初から最後までの範囲内。 (同様に、ジャンプ テーブルの各行は呼び出しスタックのフレームに対応し、各行にはそれを作成した呼び出し命令ステップの EID がラベル付けされます。)
このメモリ システムは通常の VM インタープリタとは大きく異なります。段階的に更新される可変メモリの代わりに、メモリ テーブルには実行トレース全体にわたるすべてのメモリ アクセスの履歴が含まれます。プログラマの作業を簡素化するために、zkWasm は 2 つの便利なエントリ関数を通じて実装された抽象化層を提供します。彼らです：
alloc_memory_table_lookup_write_cell
そして
Alloc_memory_table_lookup_read_cell
そのパラメータは次のとおりです。
たとえば、zkWasm でメモリ ストレージ命令を実装するコードには、「write alloc」関数への呼び出しが含まれています。
letmemory_table_lookup_heap_write1 = アロケータ
.alloc_memory_table_lookup_write_cell_with_value(
書き込み応答 1 を保存,
制約ビルダー、
イード、
move |____| constant_from!(LocationType::Heap as u 64),
移動 |meta|
move |____| 定数_from!( 0)、 // は 32 ビットです
move |____| 定数から!( 1), // (常に) 有効
);
ヒープ内のストア値1 = メモリテーブルルックアップヒープライト1.値セル;
`alloc` 関数は、テーブル間のルックアップ制約と、現在の `eid` をメモリ テーブル エントリに関連付ける算術制約を処理します。このことから、プログラマはこれらのテーブルを通常のメモリとして扱うことができ、コードの実行後に「store_value_in_heap1」の値が「load_block_index」アドレスに割り当てられます。
同様に、メモリ読み取り命令は「read_alloc」関数を使用して実装されます。上記の実行シーケンスの例では、各ロード命令には読み取り制約があり、各ストア命令には書き込み制約があり、各制約はメモリ テーブル内のエントリによって満たされます。
mtable_lookup_write(行 1.eid、行 1.store_addr、行 1.store_value)
⇐ (行 1.eid= 1 ∧ 行 1.store_addr=balance ∧ 行 1.store_value= 100 ∧ ...)
mtable_lookup_write(行 2.eid、行 2.store_addr、行 2.store_value)
⇐ (行 2.eid= 2 ∧ 行 2.store_addr=amount ∧ 行 2.store_value= 10 ∧ ...)
mtable_lookup_read(行 3.eid、行 3.load_addr、行 3.load_value)
⇐ ( 2<行 3.eid≤ 6 ∧ 行 3.load_addr=量 ∧ 行 3.load_value= 100 ∧ ...)
mtable_lookup_read(行 4.eid、行 4.load_addr、行 4.load_value)
⇐ ( 1<行 4.eid≤ 6 ∧ 行 4.load_addr=balance ∧ 行 4.load_value= 10 ∧ ...)
mtable_lookup_write(行 6.eid、行 6.store_addr、行 6.store_value)
⇐ (行 6.eid= 6 ∧ 行 6.store_addr=balance ∧ 行 6.store_value= 90 ∧ ...)
形式的検証の構造は、証明がコードと同じロジックに従うことができるように、検証されるソフトウェアで使用される抽象化に対応する必要があります。 zkWasm の場合、これはメモリ テーブル回路と、変数メモリのようにインターフェイスするモジュールとしての「読み出し/書き込みセルの割り当て」機能を検証する必要があることを意味します。このようなインターフェイスがあれば、各命令回路の検証は通常のインタプリタと同様の方法で実行でき、追加の ZK の複雑さはメモリ サブシステム モジュールにカプセル化されます。
検証では、「メモリテーブルは実際には可変のデータ構造とみなすことができる」というアイデアを実装しました。つまり、メモリ テーブルを完全にスキャンし、対応するアドレス データ マッピングを構築する関数 `memory_at type` を作成します。 (ここでの変数 `type` の値の範囲は、ヒープ、データ スタック、グローバル変数の 3 つの異なるタイプの Wasm メモリ データです。) 次に、alloc 関数によって生成されたメモリ制約が set および get を使用するのと同等であることを証明します。対応するアドレス データ マッピングによって行われるデータ変更。次のことを証明できます。
各 eid について、次の制約が当てはまる場合
Memory_table_lookup_read_cell eid タイプのオフセット値
しかし
get (memory_at eid type) offset = 何らかの値
そして、次の制約が成立する場合、
Memory_table_lookup_write_cell eid タイプのオフセット値
しかし
Memory_at (eid+ 1) タイプ = set (memory_at eid タイプ) オフセット値
この後、各命令の検証は、非 ZK バイトコード インタプリタと同様に、アドレス データ マップ上の get および set 操作に基づいて行うことができます。
zkWasm のメモリ書き込みカウント メカニズム
ただし、上記の簡略化した説明では、メモリ テーブルとジャンプ テーブルの内容がすべて明らかになっているわけではありません。 zkVM フレームワークでは、これらのテーブルは攻撃者によって操作される可能性があり、攻撃者はデータ行を挿入することでメモリ ロード命令を簡単に操作して任意の値を返すことができます。
出金プログラムを例に挙げると、攻撃者は出金操作の前に 110 ドルのメモリ書き込み操作を偽造することで、口座残高に偽のデータを注入する機会を得ます。このプロセスは、メモリ テーブルにデータ行を追加し、メモリ テーブルと実行テーブルの既存のセルの値を変更することで実現できます。操作後もアカウント残高は 100 ドルのままなので、これにより「無料」の出金が可能になります。
実際に実行されるメモリ書き込み (および呼び出しと復帰) 命令によって生成された有効なエントリのみがメモリ テーブル (およびジャンプ テーブル) に含まれるようにするために、zkWasm は特別なカウント メカニズムを採用してエントリ数を監視します。具体的には、メモリ テーブルには、メモリに書き込まれたエントリの総数を追跡する専用の列があります。同時に、実行テーブルには、各命令で予想されるメモリ書き込み操作の数をカウントするカウンターも含まれています。等価制約を設定して、2 つのカウントが一貫していることを確認します。このメソッドのロジックは非常に直感的です。メモリ内で書き込み操作が実行されるたびに、それが 1 回カウントされ、対応するレコードがメモリ テーブルに存在する必要があります。したがって、攻撃者はメモリ テーブルに追加のエントリを挿入できません。
上記の論理ステートメントは少し曖昧であり、機械化された証明のプロセスでは、より正確にする必要があります。まず、上記のメモリ書き込み補題のステートメントを修正する必要があります。関数 `mops_at eid type` を定義して、指定された `eid` と `type` を持つメモリ テーブル エントリをカウントします (ほとんどの命令は、eid に 0 または 1 つのエントリを作成します)。定理の完全な記述には、偽のメモリ テーブル エントリがないことを示す追加の前提条件があります。
以下の制約が成立する場合
(memory_table_lookup_write_cell eidタイプのオフセット値)
そして、次のような新しい制約が確立されます
(mops_at eid タイプ) = 1
しかし
(memory_at(eid+1) タイプ) = (memory_at eid タイプ) オフセット値を設定
これには、前のケースよりも正確な検証が必要です。 メモリ テーブル エントリの総数が実行時のメモリ書き込みの総数に等しいという等価性制約から単に導出するだけでは、検証を完了するには十分ではありません。命令の正しさを証明するには、各命令が正しい数のメモリ テーブル エントリに対応していることを知る必要があります。たとえば、攻撃者が実行シーケンス内の命令のメモリ テーブル エントリを省略し、別の無関係な命令に対して悪意のある新しいメモリ テーブル エントリを作成する可能性があるかどうかを除外する必要があります。
これを証明するために、トップダウンのアプローチを使用して、特定の命令に対応するメモリ テーブル エントリの数を制限します。これには 3 つのステップが含まれます。まず、命令の種類に基づいて、実行シーケンス内の命令に対して作成する必要があるエントリの数を見積もります。 i 番目のステップから実行の終了までに予想される書き込み数を「instructions_mops i」と呼び、i 番目の命令から実行の終了までに対応するメモリ テーブル内のエントリの数を「cum_mops (eid i)」と呼びます。各命令の検索制約を分析することで、予想よりも少ないエントリが作成されないことを証明でき、追跡された各セグメント [i... numRows] が予想よりも少ないエントリを作成しないと結論付けることができます。
補題cum_mops_bound: forall ni,
0 ≤ i ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≥ infection_mops i n。
次に、テーブルに予想よりも多くのエントリが含まれていないことが証明できれば、テーブルには正確な数のエントリが含まれていることになります。これは明らかです。
補題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) ≤ infection_mops in ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) =命令_mops i n。
次にステップ 3 に進みます。私たちの正当性定理は、任意の n に対して、cum_mops とmessages_mops は行 n からテーブルの最後まで常に一貫していると述べています。
補題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) =命令_mops (Z.of_nat n)
検証は n を要約することによって行われます。テーブルの最初の行は zkWasm の等価制約で、メモリ テーブル内のエントリの総数が正しいこと、つまりcum_mops 0 =messages_mops 0 を示します。次の行については、帰納的仮説により次のことがわかります。
Cum_mops n = 命令モップ n
そして私たちはそれを証明したいと考えています
Cum_mops (n+ 1) = 命令_mops (n+ 1)
ここに注目してください
Cum_mops n = mop_at n + Cum_mops (n+ 1)
そして
命令モップス n = 命令モップス n + 命令モップス (n+ 1)
したがって、私たちは得ることができます
mops_at n +cum_mops (n+ 1) = 命令モップ n + 命令モップ (n+ 1)
以前に、各命令が予想される数以上のエントリを作成することを示しました。
mops_at n ≧instruction_mops n。
それで結論づけられるのは
Cum_mops (n+ 1) ≤ infection_mops (n+ 1)
ここで、上記の 2 番目の補題を適用する必要があります。
(同様の補題を使用してジャンプ テーブルを検証すると、各呼び出し命令がジャンプ テーブル エントリを正確に生成できることが証明できるため、この証明手法は一般に適用可能です。ただし、戻り値の正確性を証明するには、さらに検証作業が必要です。返される eid は、呼び出しフレームを作成した呼び出し命令の eid とは異なるため、実行シーケンス中に eid 値が一方向にインクリメントされることを宣言する追加の不変プロパティも必要です。)
証明プロセスをこれほど詳細に説明することは、形式的検証の典型であり、特定のコード部分の検証に、コードを記述するよりも時間がかかることがよくある理由です。しかし、それだけの価値はあるでしょうか？この場合、証明中にジャンプ テーブルのカウント メカニズムに重大なバグが見つかったので、これは価値がありました。このバグについては、以前の記事で詳しく説明しました。要約すると、古いバージョンのコードは呼び出し命令と戻り命令の両方を担当しており、攻撃者は追加の戻り命令を実行シーケンスに追加して余地を作ることで偽のジャンプを作成する可能性があります。 。間違ったカウントメカニズムによって、すべての呼び出し命令と戻り命令がカウントされるという直感を満たすことができますが、この直感をより正確な定理ステートメントに改良しようとすると問題が発生します。
証明プロセスをモジュール化する
上記の議論から、各命令の回路に関する証明と実行テーブルのカウント列に関する証明の間には循環依存関係があることがわかります。命令回路が正しいことを証明するには、その中のメモリ書き込みについて推論する必要があります。つまり、特定の EID でのメモリ テーブル エントリの数を知る必要があり、メモリ書き込み操作のカウントを証明する必要があります。実行テーブルが正しく、各命令が少なくとも最小数のメモリ書き込みを実行することを証明する必要もあります。
さらに、zkWasm プロジェクトは非常に大規模であるため、複数の検証エンジニアが作業を分担できるように検証作業をモジュール化する必要があります。したがって、カウントメカニズムの証明を分解するときは、その複雑さに特別な注意を払う必要があります。たとえば、LocalGet 命令の場合、次の 2 つの定理があります。
定理 opcode_mops_correct_local_get : forall i,
0 <= i ->
etable_values eid_cell i > 0 ->
opcode_mops_correct LocalGet i.
定理 LocalGetOp_correct : forall i st y xs,
0 <= i ->
etable_values 有効セル 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 つのメモリ テーブル エントリを作成することを意味します (番号 1 は、zkWasm の LocalGet オペコード仕様で指定されます)。
2 番目の定理は、命令の完全な正しさの定理であり、次のようになります。
mops_at_correct i
仮説として、これは、命令によってメモリ テーブル エントリが 1 つだけ作成されることを意味します。
検証エンジニアは、これら 2 つの定理を独立して証明し、実行テーブルに関する証明と組み合わせて、システム全体の正しさを証明できます。個々の命令のすべての証明は、メモリ テーブルの特定の実装を知らなくても、読み取り/書き込み制約のレベルで実行できることは注目に値します。したがって、プロジェクトは独立して処理できる 3 つの部分に分割されます。
要約する
zkVM の回路を 1 行ずつ検証することは、他のドメインの ZK アプリケーションを検証することと基本的に異なりません。どちらも算術制約について同様の推論を必要とするからです。大まかに言えば、zkVM の検証には、プログラミング言語インタープリターやコンパイラーに使用されるのと同じ形式的な検証方法の多くが必要です。ここでの主な違いは、仮想マシンの状態が動的にサイズ変更されることです。ただし、実装で使用される抽象化レイヤーに一致するように検証構造を慎重に構築することで、これらの違いの影響を最小限に抑えることができます。これにより、通常のインタプリタの化学検証と同様に、各命令を get-set インターフェイスに基づいて独立したモジュールにすることができます。
