形式検証テクノロジが zkVM (ゼロ知識仮想マシン) にどのように適用されるかを深く理解するために、この記事では単一命令の検証に焦点を当てます。 ZKP（ゼロ知識証明）の高度形式検証の全体状況については、同時公開した記事「ゼロ知識証明ブロックチェーンの高度形式検証」を参照してください。
zkVM (ゼロ知識仮想マシン) は、特定のプログラムが特定の入力で実行され、正常に終了できることを証明する短い証明オブジェクトを作成できます。 Web3.0 分野では、L1 ノードはスマート コントラクトの入力状態から出力状態への遷移の短い証明のみを検証するだけでよく、実際のコントラクト コードの実行はオフチェーンで完了できるため、zkVM のアプリケーションにより高スループットが可能になります。
zkVM 証明者は、まずプログラムを実行して各ステップの実行記録を生成し、次に実行記録データを数値表のセットに変換します (このプロセスを「算術化」と呼びます)。これらの数値は、特定のテーブル セル間の接続方程式、固定定数、テーブル間のデータベース検索制約、および隣接するテーブル行の各ペア間で満たされる必要がある多項式などの制約のセット (回路など) を満たす必要があります。方程式 (別名「ゲート」)。オンチェーン検証では、テーブル内の特定の数値が表示されないことを保証しながら、すべての制約を満たすテーブルが実際に存在することを確認できます。
各 VM 命令の実行は、このような多くの制約に直面します。ここでは、VM 命令のこの一連の制約を「ZK 命令」と呼びます。以下は、Rust で書かれた zkWasm メモリ ロード命令制約の例です。
#ZK 命令の形式検証は、これらのコードに対して形式推論を実行することによって行われ、最初に形式言語に変換されます。
#単一の制約にエラーが含まれている場合でも、攻撃者が悪意のある ZK 証明を送信する可能性があります。悪意のある証拠に対応するデータテーブルは、スマートコントラクトの法的な運用に対応していません。イーサリアムなどの非 ZK チェーンでは、異なる EVM (イーサリアム仮想マシン) 実装を実行する多数のノードがあり、同じバグが同時に同じ場所で発生する可能性は低くなります。zkVM チェーンには単一の VM 実装しかありません。 。この観点だけから見ても、ZK チェーンは従来の Web3.0 システムよりも脆弱です。
さらに悪いことに、非 ZK チェーンとは異なり、zkVM トランザクションの計算の詳細が送信されず、チェーン上に保存されないため、攻撃が発生した後、トランザクションの特定の詳細を発見することが非常に困難になるだけでなく、攻撃だけでなく、攻撃自体を特定することさえ困難になる場合があります。
zkVM システムは非常に厳密な検査を必要としますが、残念ながら、zkVM 回路の正確性を保証することは困難です。
VM (仮想マシン) は、Web3.0 システム アーキテクチャの最も複雑な部分の 1 つです。スマート コントラクトの強力な機能は、Web3.0 機能をサポートする中核であり、その力は柔軟かつ複雑な基盤となる VM から得られます。一般的なコンピューティングおよびストレージ タスクを完了するには、これらの VM が多数の命令をサポートできなければなりません。と州。たとえば、EVM の geth 実装には 7,500 行を超える Go 言語コードが必要です。同様に、これらの命令の実行を制約する ZK 回路も同様に大きくて複雑です。 zkWasm プロジェクトと同様、ZK 回路の実装には 6000 行を超える Rust コードが必要です。
zkWasm 回路アーキテクチャ
プライベート決済などの特定のアプリケーション向けに設計された ZK システムとの比較zkVM 回路で使用される専用の ZK 回路では、zkVM 回路の規模ははるかに大きくなります。制約ルールの数は前者よりも 1 ～ 2 桁多くなり、演算テーブルには数百の列が含まれる可能性があります。何千ものデジタルセル。
ここでは、zkWasm の XOR 命令が正しいことを確認したいと思います。技術的に言えば、zkWasm の実行テーブルは、正当な Wasm VM 実行シーケンスに対応します。したがって、マクロの観点から確認したいのは、この命令が実行されるたびに、新しい正当な zkVM 状態が常に生成されるということです。テーブル内の各行は VM の正当な状態に対応し、次の行は常に生成されます。これは、対応する VM 命令を実行することによって生成されます。以下の図は、XOR 命令の正しさに関する形式定理を示しています。
ここで、「state_rel i st」は、状態「st」がステップ「i」のスマート コントラクトの正当な zkVM 状態であることを示します。ご想像のとおり、「state_rel (i 1) ...」を証明するのは簡単ではありません。
XOR 命令の計算セマンティクスは非常に単純ですが、ビット単位の排他的 OR (ビット単位でメモリから 2 つの整数を取得し、XOR 計算を実行し、計算された新しい整数を同じスタックに格納します) を計算することです。 。さらに、この命令の実行ステップはスマート コントラクト実行プロセス全体に統合される必要があり、その実行の順序とタイミングは正しくなければなりません。
したがって、XOR 命令の実行結果は、データ スタックから 2 つの数値をポップし、それらの XOR 結果をプッシュし、同時にプログラム カウンターをインクリメントすることになります。スマートコントラクトの次の指示をポイントします。
ここでの正当性属性の定義が、従来のバイトコード VM (イーサリアム L1 ノードの EVM インタープリタなど) を検証するときと一般に同じであることを理解するのは難しくありません。直面する状況は非常によく似ています。これは、マシン状態の高レベルの抽象定義 (ここではスタック メモリと実行フロー) と、各命令の予期される動作の定義 (ここでは算術ロジック) に依存します。
ただし、以下で説明するように、ZKP と zkVM の特殊な性質により、その正しさの検証プロセスは通常の VM の検証プロセスとは大きく異なることがよくあります。ここでの 1 つの命令が zkWASM 内の多くのテーブルの正しさに依存していることを確認します。その中には、値のサイズを制限するために使用される範囲テーブル、バイナリ ビット計算の中間結果に使用されるビット テーブル、データを格納する実行テーブルなどがあります。行ごとの一定サイズの VM 状態 (物理 CPU のレジスタおよびラッチ内のデータと同様)、および動的に可変サイズの VM 状態を表すメモリ (メモリ、データ スタック、およびコール スタック) テーブルとジャンプ テーブル。
従来の VM と同様に、命令の 2 つの整数パラメーターがスタックから読み取れること、およびそれらの XOR 結果の値が次のとおりであることを確認する必要があります。バックスタックが正しく書き込まれました。スタックの正式な表現もかなり見慣れたものです (グローバル メモリとヒープ メモリもありますが、XOR 命令はそれらを使用しません)。
ZK 証明者はスタックや配列などのデータ構造をネイティブにサポートしていないため、zkVM は複雑なスキームを使用して動的データを表現します。逆に、スタックにプッシュされた値ごとに、メモリ テーブルに個別の行が記録され、列の一部はエントリの有効時間を示すために使用されます。もちろん、これらのテーブル内のデータは攻撃者によって制御される可能性があるため、テーブル エントリがコントラクト実行時の実際のスタック命令に実際に対応していることを確認するには、いくつかの制約を課す必要があります。これは、プログラム実行中のスタック プッシュの数を慎重に計算することで実現されます。各命令を検証するときは、このカウントが常に正しいことを確認する必要があります。さらに、単一の命令によって生成される制約を、スタック操作を実装するテーブル検索と時間範囲チェックに関連付ける一連の補題があります。最上位レベルから、メモリ操作のカウント制約は次のように定義されます。
従来の VM と同様に、ビット単位の XOR 演算が正しいことを確認する必要があります。私たちの物理的なコンピュータの CPU は一度にこれを実行できるため、これは簡単に思えます。
しかし、zkVM の場合、これは実際には単純ではありません。 ZK 証明者がネイティブにサポートする算術命令は加算と乗算のみです。バイナリ ビット演算を実行するために、VM はかなり複雑なスキームを使用します。このスキームでは、1 つのテーブルが固定バイト レベルの演算結果を格納し、もう 1 つのテーブルが複数のテーブル行で演算を実行する方法を示す「スクラッチ パッド」として機能します。 64 ビットの数値は 8 バイトに分解され、再組み立てされて結果が得られます。
zkWasm ビットテーブル仕様の一部
従来のプログラミング言語での非常に単純な XOR 操作はこちらこれらの補助テーブルの正確さを検証するには、多くの補題が必要です。ディレクティブには次のようになります:
従来の VM と同様に、プログラム カウンターの値が正しく更新されていることを確認する必要があります。 XOR などの逐次命令の場合、各ステップの後にプログラム カウンタを 1 つずつ増やす必要があります。
zkWasm は Wasm コードを実行するように設計されているため、Wasm メモリの不変の性質が実行中維持されることを確認することも重要です。
従来のプログラミング言語では、ブール値、8 ビット整数、64 ビット整数などのデータ型がネイティブにサポートされていますが、ZK 回路では、変数は常に整数の剰余の範囲内にあります。素数 (≈ 2254)。 VM は通常 64 ビットで実行されるため、回路開発者は制約システムを使用して数値範囲が正しいことを確認する必要があり、形式検証エンジニアは検証プロセス全体を通じてこれらの範囲に関する不変プロパティを追跡する必要があります。実行フローと実行テーブルに関する推論には他のすべての補助テーブルが関係するため、すべてのテーブル データの範囲が正しいことを確認する必要があります。
メモリ操作数管理の場合と同様に、zkVM では制御フローを検証するために同様の補題のセットが必要です。具体的には、各呼び出し命令と戻り命令では呼び出しスタックの使用が必要です。呼び出しスタックは、データ スタックと同様のテーブル スキームを使用して実装されます。 XOR 命令の場合、コール スタックを変更する必要はありませんが、命令全体を検証する場合は、制御フローの操作数が正しいかどうかを追跡して検証する必要があります。
この命令を検証する
すべての手順をまとめて、zkWasm XOR 命令のエンドツーエンドの正当性定理を検証してみましょう。以下の検証は対話型証明環境で完了します。この環境では、形式的な構築と論理的推論のすべてのステップが最も厳密な機械チェックを受けます。
#上記のように、zkVM 回路の正式な検証は実行可能です。しかし、これは多くの複雑な不変プロパティを理解して追跡する必要がある難しい作業です。これは、検証されるソフトウェアの複雑さを反映しています。検証に含まれるすべての補題は、回路開発者によって正しく処理される必要があります。大きなリスクが伴うことを考えると、人間による慎重なレビューのみに依存するのではなく、正式な検証システムによって機械チェックを受けることは価値があるでしょう。
以上がゼロ知識証明の高度な形式的検証: ZK 命令を検証する方法の詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。
![[Web フロントエンド] Node.js クイック スタート](https://img.php.cn/upload/course/000/000/067/662b5d34ba7c0227.png)
