ゼロ知識証明の高度な形式的検証：ZK命令の検証方法

出典：CertiK Chinese Community

zkVM（ゼロ知識仮想マシン）の上でどのように形式検証技術が適用されるかを深く理解するために、この記事では1つの命令の検証に焦点を当てます。ZKPのための高度な形式検証の一般的な概要については、同時公開の記事「ゼロ知識証明ブロックチェーンのための高度な形式検証」を参照してください。

ZK命令の検証とは何ですか？

zkVM（ゼロ知識仮想マシン）は、特定のプログラムが特定の入力で実行でき、正常に終了することの証拠として使用できる短い証明オブジェクトを作成することができます。Web 3.0では、zkVMのアプリケーションは、L1ノードがスマートコントラクトの入力状態から出力状態への遷移の短い証明を検証するだけでよく、実際のコントラクトコードの実行はオフチェーンで行うことができるため、高いスループットが可能になります。

zkVMプローバーは、まずプログラムを実行して各ステップの実行記録を生成し、次に実行記録からのデータを数値の表に変換します（「算術化」として知られるプロセス）。これらの数値は、特定の表セル間の連結方程式、固定定数、表間のデータベース検索制約、表の隣り合う行の各ペア間で満たすべき多項式（すなわち「ゲート」）を含む、それらの間の制約（すなわち回路）のセットを満たさなければならない。連鎖検証は、このように、テーブル内の正確な数値が見えないようにしながら、すべての制約を満たすテーブルが確かに存在することを確認します。

各VM命令は、その実行において多くのこれらの制約に直面します。以下は、Rustで記述されたzkWasmメモリロード命令制約の例です。

ZK 命令の形式的検証は、これらのコードに対する形式的推論によって行われます。を形式的に推論することによって行われます。

たった1つの制約にエラーが含まれていたとしても、攻撃者はこのようにエラーを提出する危険性があります。攻撃者は悪意のあるZK証明を提出する危険性があります。悪意のある証明が対応するデータテーブルは、スマートコントラクトの正当な実行に対応していません。イーサリアムのような非ZKチェーンでは、異なるEVM（イーサリアム仮想マシン）実装を実行するノードが多数存在するため、同じ場所で同時に同じエラーが発生する可能性が低いのとは異なり、zkVMチェーンではVM実装は単一です。この理由だけで、ZKチェーンは従来のWeb 3.0システムよりも脆弱です。

さらに悪いことに、非ZKチェーンとは異なり、zkVMトランザクションの計算の詳細がチェーン上に送信および保存されないため、攻撃が発生した後、攻撃の正確な詳細を発見することが非常に難しいだけでなく、攻撃自体を特定することさえも非常に困難になります。

zkVMシステムは非常に厳格な精査を必要とし、残念ながら、zkVM回路の正しさを保証することは非常に困難です。

なぜZK命令の検証は難しいのか？

VM（仮想マシン）は、Web 3.0システムアーキテクチャの中で最も複雑な部分の1つです。Web 3.0の機能を支える中心的存在であるスマートコントラクトのパワーは、基盤となるVMに由来します。例えば、EVMのgeth実装には7,500行以上のGo言語コードが必要である。同様に、これらの命令の実行を制約するZK回路も同様に大規模で複雑である。zkWasmプロジェクトのように、ZK回路の実装には6000行以上のRustコードが必要でした。

zkWasm回路アーキテクチャ

特定のアプリケーション（例えば、個人的な支払い）のために設計されたZKシステムで使用される専用のZK回路と比較すると、zkVM回路はかなり大規模です。セルを含む数百の列で構成されるかもしれない。

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

ここでzkWasmのXOR命令の正しさを検証していきたいと思います。技術的には、zkWasmの実行テーブルは正当なWasm VMの実行シーケンスに対応しています。つまり、マクロ的に検証したいのは、この命令の各実行が常に新しい合法的なzkVM状態を生成することです。テーブルの各行はVMの合法的な状態に対応し、直後の行は常に対応するVM命令を実行することで生成されなければなりません。次の図は、XOR命令の正しさに関する正式な定理を示しています。

Here."state_rel i st "は、状態 "st "がステップ "i "のスマート・コントラクトの合法的なzkVM状態であることを示します。 お察しの通り、"state_rel (i+1) ... "を証明するのは簡単ではありません。

ZKコマンドを検証するには？

XOR命令の計算セマンティクスは単純で、2つの整数のビットごとのxorを計算し、整数の結果を返すというものですが、それ以上の側面があります。まず、スタック・メモリから2つの整数を取り出し、xorを計算し、この計算の結果の新しい整数を同じスタックに戻す必要があります。さらに、この命令の実行ステップは、スマートコントラクトの実行フロー全体に統合されていなければならず、その実行順序とタイミングは正確でなければなりません。

したがって、XOR命令の実行の効果は、データスタックから2つの数値をポップし、そのXOR結果を押し込むことであるべきです。スマート・コントラクトの次の命令を指すようにプログラム・カウンターを増加させながら、XOR結果を押し込むことです。

ここでの正しさのプロパティの定義が、一般的に、イーサネットのEVMインタープリタなどの従来のバイトコードVMの検証で使用しているものと似ていることは、難しいことではありません。イーサネットL1ノードのEVMインタプリタ）のような従来のバイトコードVMを検証する際に直面するものと非常によく似ています。これは、マシン状態（ここでは、スタック・メモリと実行フロー）の高レベルの抽象的な定義と、各命令の期待される動作（ここでは、算術論理）の定義に依存しています。

しかし、後述するように、ZKPとzkVMの特殊な性質のために、それらの正しさを検証するプロセスは、通常のVMとは大きく異なることがよくあります。その中には、値のサイズを制限するための範囲テーブル、バイナリビット計算の中間結果を格納するビットテーブル、各行に一定サイズのVM状態を格納する実行テーブル（物理的なCPUのレジスタやラッチのデータに似ています）、そして動的に可変サイズのVM状態（メモリ、データ）を表すテーブルがあります。可変サイズのVM状態（メモリ、データスタック、コールスタック）、およびメモリテーブルとジャンプテーブルを表します。

ステップ 1: スタック メモリ

従来の VM と同様に、命令の 2 つの整数パラメーターがスタックから読み取れること、およびそれらの iso 結果値がスタックに正しく書き戻されることを確認する必要があります。スタックの形式的な表現も、かなり見慣れたものです（グローバル・メモリやヒープ・メモリと一緒ですが、XOR命令はそれらを使いません）。

zkVM は動的データを表現するために複雑なスキームを使用します。これは、ZKプロヴァーがスタックや配列のようなデータ構造をネイティブにサポートしていないためです。その代わりに、スタックに押された値ごとに、メモリ・テーブルが別の行に記録され、そのテーブル・エントリがいつ有効であるかを示すために特定の列が使用されます。もちろん、これらのテーブルのデータは攻撃者にコントロールされる可能性があるので、テーブル・エントリがコントラクト実行中の実際のスタック押下命令に本当に対応していることを保証するために、いくつかの制約も課さなければならない。これは、プログラム実行中のスタック数を注意深くカウントすることで達成される。各命令を検証する際には、このカウントが常に正しいことを保証する必要がある。さらに、1つの命令によって生成される制約を、スタック操作を実装するテーブル・ルックアップと時間水平チェッ クに関連付ける一連のレンマがあります。トップレベルでは、メモリ操作のカウント制約は次のように定義されます。

従来のVMと同様に、ビットごとの同型の算術演算が正しいことを確認したいと思います。結局のところ、私たちの物理的なコンピューターの CPU は、この演算を一度に行うことができます。

しかし、zkVMでは、実際にはそれほど単純ではありません。ZKプローバーがネイティブでサポートするバイナリ算術命令は、加算と乗算だけです。バイナリー・ビットワイズ演算を実行するために、VMはかなり複雑なスキームを使用します。1つのテーブルが固定バイトレベルの演算結果を保持し、もう1つのテーブルが「スケッチブック」として機能し、テーブルの複数の行で64ビット数を8バイトに分解し、結果を再結合する方法を示します。

zkWasmビットテーブル仕様の一部

従来のプログラミング言語では非常に単純な変則演算ですが、ここではこれらの補助テーブルの正しさを検証するために多くのレンマが必要です。

ステップ3: 実行ストリーム

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

zkWasmはWasmコードを実行するように設計されているため、Wasmメモリの不変性が実行中常に維持されるようにすることも重要です。

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

メモリ操作数の管理の場合と似ています。zkVMは、制御フローを検証するために同様のプリミティブセットを必要とします。具体的には、各コールとリターン命令は、コールスタックの使用を必要とします。コール・スタックは、データ・スタックと同様のテーブル・スキームを使用して実装される。XOR命令の場合、コールスタックを変更する必要はありません。しかし、命令全体を検証する場合、制御フロー操作カウントが正しいことをトレースして検証する必要があります。

この命令を検証する

zkWasm XOR命令のend-to-endの正しさの定理を検証するために、すべてのステップをまとめましょう。以下の検証は、各形式的構成と論理的推論ステップが最も厳密なマシンチェックを受ける対話型証明環境で行われます。

上で見たように、zkVM回路の形式的検証は実現可能です。回路のフォーマル検証は可能です。しかし、多くの複雑な不変特性を理解し、トレースする必要がある難しい作業です。これは、検証されるソフトウェア自体の複雑さを反映しています。検証に関わるすべてのレンマは、回路開発者によって正しく処理される必要があります。このような高いリスクを考えると、慎重な手作業によるレビューだけに頼るのではなく、形式検証システムによって機械的にチェックされることは価値があります。