This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
zk-SNARKsシステムのメモリ検証方法：zkWasmはどのように形式的認証を実現するか
ゼロ知識証明の形式的検証:プルーフ・オブ・メモリー法
零知識証明システムの形式的認証を行う際、メモリサブシステムの処理は重要な課題です。従来の仮想マシンとは異なり、zkVMは実行テーブルと補助テーブルを使用してメモリ状態を表現し、特別な検証方法が必要です。
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-89a848cad134821a8c7c009ed6f54cda.webp)
zkWasmのメモリシステムは、実行テーブルとメモリテーブルで構成されています。実行テーブルは命令の実行プロセスを記録し、メモリテーブルはすべてのメモリアクセスの履歴を保存します。開発を簡素化するために、zkWasmは抽象レイヤーを提供し、alloc_memory_table_lookup_write_cellおよびalloc_memory_table_lookup_read_cellの2つの関数を使用してメモリを操作します。
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-26846de67e6cea4a40783150d002084c.webp)
検証プロセスでは、メモリテーブルを可変データ構造として扱い、memory_at関数を使用してアドレスデータマッピングを構築します。これにより、alloc関数によって生成された制約がマッピングに対するsetおよびget操作と等価であることが証明でき、命令の検証を非ZKインタプリタに似た形式に簡素化することができます。
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-53c7e3a45209f44c30093acd18dc7b81.webp)
攻撃者がメモリテーブルを操作するのを防ぐために、zkWasmは有効エントリの数を追跡するカウントメカニズムを採用しています。実行テーブルとメモリテーブルはそれぞれカウンターを維持し、制約によって両者の整合性が確保されます。これにより、検証時により正確さが求められ、各命令が正しい数のメモリテーブルエントリに対応していることを証明する必要があります。
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-eef0b5eb2efc84aa949b89d178ed671c.webp)
検証プロセスは、トップダウン方式を採用しており、3つのステップが含まれています:
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-86aa6d91b889ad492d104a5d367d29d1.webp)
この詳細な検証方法は、ジャンプテーブルカウントメカニズムの重要な問題など、潜在的なエラーを発見するのに役立ちます。
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-74cef0d2bae93477cb01dbc8d0970398.webp)
モジュール化検証を実現するために、システムを三つの独立した部分に分割します: 命令回路検証、実行テーブル検証、およびメモリテーブルの実装。この構造により、複数のエンジニアが並行して作業でき、検証効率が向上します。
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-0cb97d2b1359ba8ec999b5fa183c39cb.webp)
全体的に見ると、zkVMの検証は動的な状態を処理する際に違いがありますが、実装内の抽象レイヤーを一致させることにより、従来のインタプリタ検証と類似のモジュール化アプローチを採用することができます。このアプローチは、違いによる影響を最小限に抑え、各命令がget-setインターフェースに基づいて独立して検証できるようにします。
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-a73101c3b88a3ca28063d5fc6e0cada2.webp)
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-ebb57b18c469bc9dc200680d62c34aef.webp)
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-e1796b9e7d7f1395278a58ebe5549f71.webp)
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-156c067f1b5934b57b76122e023bbca9.webp)
! [ゼロ知識証明の高度な形式的検証:ゼロ知識記憶をどう証明するか] ](https://img-cdn.gateio.im/webp-social/moments-7920d37f984caa9326fc2cc4b48eec03.webp)