ゼロ知識証明の先進的な形式的検証：ZK命令をどのように検証するか

執筆：Certik

形式的検証技術が 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コードが必要です。

zkWasm回路アーキテクチャ

特定のアプリケーション（プライベートペイメントなど）向けに設計されたZKシステムで使用される専用ZK回路と比較して、zkVM回路の規模ははるかに大きいです：その制約ルールの数は前者よりも1桁から2桁多くなる可能性があり、その算術化表は数百列、数百万の数値セルを含む可能性があります。

ZK命令の検証は何を意味するのか？

ここでは、zkWasmにおけるXOR命令の正当性を検証したいと考えています。技術的には、zkWasmの実行表は合法的なWasm VM実行シーケンスに対応します。したがって、マクロ的に見ると、私たちが検証したいのは、毎回この命令を実行することで常に新しい合法的なzkVM状態が生成されることです：表の各行はVMの合法的な状態に対応し、次の行は常に対応するVM命令を実行することで生成されます。以下の図はXOR命令の正当性に関する形式的定理です。

ここで「staterel i st」は状態「st」がステップ「i」におけるスマートコントラクトの合法的なzkVM状態であることを示しています。あなたが推測したように、「staterel (i+1) …」を証明することは簡単ではありません。

ZK命令をどのように検証するか？

XOR命令の計算意味は非常にシンプルで、2つの整数のビット単位の排他的論理和（bitwise xor）を計算して整数結果を返すだけですが、関わる側面は多岐にわたります。まず、スタックメモリから2つの整数を取り出し、排他的論理和を計算し、その計算結果の新しい整数を同じスタックに戻す必要があります。さらに、この命令の実行ステップは、全体のスマートコントラクトの実行フローに組み込まれ、その実行順序とタイミングが正確でなければなりません。

したがって、XOR命令の実行効果は、データスタックから2つの数をポップし、それらのXOR結果をプッシュし、プログラムカウンタを増加させてスマートコントラクトの次の命令を指す必要があります。

ここでの正当性属性の定義は、従来のバイトコードVM（例えば、イーサリアムL1ノードのEVMインタープリタ）を検証する際に直面する状況と非常に似ています。これは、マシン状態（ここではスタックメモリと実行フロー）の高レベルの抽象定義と、各命令の期待される動作の定義（ここでは算術論理）に依存しています。

しかし、以下で見るように、ZKPとzkVMの特異性のために、その正当性の検証プロセスは通常のVMの検証とは大きく異なることがよくあります。ここでの単一の命令を検証するだけでも、zkWASM内の多くの表の正当性に依存します：数値のサイズを制限するための範囲表、バイナリビット計算の中間結果を格納するビット表、各行が固定サイズのVM状態を格納する実行表（物理CPUのレジスタやラッチ内のデータに類似）、および動的に可変サイズのVM状態（メモリ、データスタック、呼び出しスタック）を表すメモリ表とジャンプ表です。

第一步：スタックメモリ

従来のVMと同様に、命令の2つの整数パラメータがスタックから読み取れることを確認し、その排他的論理和の結果値が正しくスタックに書き戻される必要があります。スタックの形式的表現は、非常に馴染みのあるものに見えます（グローバルメモリやヒープメモリもありますが、XOR命令では使用されません）。

zkVMは動的データを表現するために複雑なスキームを使用しています。これは、ZK証明器がスタックや配列のようなデータ構造をネイティブにサポートしていないためです。代わりに、スタックにプッシュされた各数値について、メモリ表は個別の行を使用して記録し、その中のいくつかの列はその表項の有効時間を示します。もちろん、これらの表のデータは攻撃者によって制御される可能性があるため、表項が契約実行中の実際のプッシュ命令に真に対応することを保証するために、いくつかの制約を追加する必要があります。これは、プログラム実行中のプッシュ回数を慎重に計算することで実現されます。各命令を検証する際には、このカウントが常に正しいことを確認する必要があります。また、単一の命令が生成する制約をスタック操作の表検索と時間範囲チェックに関連付ける一連の補題もあります。最上位から見ると、メモリ操作のカウント制約は次のように定義されます。

第二步：算術演算

従来のVMと同様に、ビット排他的論理和の演算が正確であることを確認したいと考えています。これは簡単に見えます。結局のところ、私たちの物理コンピュータCPUはこの操作を一度に完了できます。

しかし、zkVMにとっては、これは実際には簡単ではありません。ZK証明器がネイティブにサポートする唯一の算術命令は加算と乗算です。バイナリビット演算を行うために、VMはかなり複雑なスキームを使用しており、一つの表には固定のバイトレベルの演算結果が格納され、別の表は「草稿」として機能し、64ビットの数値を8バイトに分解し、結果を再構成する方法を複数の表行に示します。

zkWasmビット表仕様の一部

従来のプログラミング言語では非常に簡単な排他的論理和演算ですが、ここではこれらの補助表の正当性を検証するために多くの補題が必要です。私たちの命令に対しては、次のようになります。

第三步：実行フロー

従来のVMと同様に、プログラムカウンタの値が正しく更新されることを確認する必要があります。XORのような順次命令の場合、各実行ステップの後にプログラムカウンタは1増加する必要があります。

zkWasmはWasmコードを実行するために設計されているため、実行全体を通じてWasmメモリの不変性が常に保持されることを確認する必要があります。

従来のプログラミング言語はブール値、8ビット整数、64ビット整数などのデータ型をネイティブにサポートしていますが、ZK回路では変数は常に大素数（≈ 2254）モジュロの整数範囲内で変化します。VMは通常64ビット数で動作するため、回路開発者はそれらが正しい数値範囲を持つことを保証するための制約システムを使用する必要があり、形式的検証エンジニアは検証プロセス全体でこれらの範囲に関する不変性を追跡する必要があります。実行フローと実行表の推論は、すべての他の補助表に関与するため、すべての表データの範囲が正しいかどうかを確認する必要があります。

メモリ操作の数の管理と同様に、zkVMは制御フローを検証するために同様の補題のセットを必要とします。具体的には、各呼び出しと戻り命令は呼び出しスタックを使用する必要があります。呼び出しスタックはデータスタックと同様の表スキームを使用して実装されます。XOR命令では呼び出しスタックを変更する必要はありませんが、命令全体を検証する際には、制御フロー操作のカウントが正しいかどうかを追跡し検証する必要があります。

この命令を検証する

すべてのステップを統合して、zkWasm XOR命令のエンドツーエンドの正当性定理を検証しましょう。以下の検証は、各形式的構造と論理推論ステップが最も厳格な機械検査を受けたインタラクティブな証明環境で行われました。

上記のように、zkVM回路の形式的検証は実行可能です。しかし、これは非常に困難な作業であり、多くの複雑な不変性を理解し追跡する必要があります。これは、検証されるソフトウェア自体の複雑性を反映しています：検証に関与する各補題は回路開発者によって正しく処理される必要があります。そのリスクが非常に高いため、形式的検証システムによる機械検査を行うことは非常に価値があります。