Coral：構文解析とゼロ知識証明の橋渡し

この記事はSebastian Angel（Pennsylvania大学）, Sofía Celi（Brave）、Elizabeth Margolin（Pennsylvania大学）、Pratyush Mishra（Pennsylvania大学）、Martin Sander（Pennsylvania大学）、Jess Woods（Pennsylvania大学）による共同研究の紹介です。 

構文解析は、コンピューティングにおける基本的な操作の一つでありながら通常はあまり意識されることがありません。ブラウザがWebページをレンダリングするとき、ファイアウォールがトラフィックを検査するとき、あるいはコンパイラがコードを変換するとき、何らかのパーサーが静かに生のバイトストリームを構造化されたオブジェクトに変換しています。私たちはこの処理を当然のものとして受け止め、入力が一度構文解析されれば、システムの残りの部分はそれについて安全に推論できると思いがちです。また、ブラウザやコンパイラが「すぐに使える状態で」これを行い、構文解析エラーをその場で修正してくれることを期待する傾向があります。

この傾向は、日常的なコンピューティングにおいてはおかしなことではありません。ブラウザは不正な形式のHTMLを発見しても可能な限り自動で修復し、コンパイラは開発者が修正できるようにエラーの概要を伝えてくれます。しかし、プライバシーを保護する検証設定、特にゼロ知識証明システムにおいては、この前提や寛容さは問題となります。証明者は、そのバイト列が正しく構文解析できるものかどうかを証明せずに、何らかのバイトストリーム（データ）を送信し、それが有効なJSON文書、トークン、またはソースファイルであると信じるかもしれません。ベースとなるデータにアクセスできない検証者は、証明者が正直であるかどうかを判断する方法がありません。このような生のバイトと構造化データのミッシング・リンクは、提案された多くのZKアプリケーションの範囲を知らず知らずのうちに制限してきました。「入力はすでに有効なJSONオブジェクトである」または「トランスクリプトは整形式でなければならない」と仮定する証明システムは、重大な攻撃に対して脆弱です。証明者が（構文解析段階を検証せずに）不正な形式の入力を紛れ込ませることができれば、有効に見える証明で虚偽の主張を証明できる可能性があります。

ゼロ知識証明アプリケーションのミッシングリンク：Coral

過去10年間、暗号学コミュニティはゼロ知識証明という枠組みの下で、野心的なアイデアを探求してきました。TLSセッションに関する証明、デジタル認証情報の属性検証、コンパイルチェーンの確認、そして基礎となるトラフィックを明かすことなくネットワークポリシーを実施することなどです。しかし、これらすべてに共通するあまり目立たない脆弱性が存在しています。

zk-TLS のケースを考えてみましょう。ユーザーが、自分の銀行のAPIが残高を報告したことをスマートコントラクトに証明したいとします。現在のアプローチでは、通常、APIレスポンスがすでに適切な形式のJSONオブジェクト（またはHTML）であることを前提としています。もし銀行のサーバーが誤って設定されていたり、バグに遭遇して不正な形式のレスポンス（有効なJSONやHTMLではない）を出力した場合、悪意のある証明者はこの不正な形式のレスポンスを悪用して、検証者に誤った事実を正しいものであると伝えることができてしまいます。同様の問題は、JWTを扱うzk-Authorizationシステムや、データストリームが正式な文法（JSON、HTML、HTTPSなど）に準拠しているという保証なしにトラフィックを検査するzk-Middleboxにも見られます。

バイト列が構造化されたオブジェクトに正しく解析されたことを証明する方法がなければ、これらのシステムは情報を漏洩させるか、検証不可能な仮定に依存するか、あるいは攻撃に対して脆弱なままとなってしまいます。私たちは Coral を、このような問題を解決するために考案しました。Coralは、コミットされたバイトストリームが文脈自由文法に従って構造化されたオブジェクトに対応していることを、ゼロ知識で証明するシステムです。

Coralのアプローチ

Coralのアプローチは、シンプルな観察から始まります。多くの場合、計算の結果を検証することは（特に検証者に適切なヒントが与えられている場合は）計算そのものを実行するよりもはるかに簡単です。古典的な例はソート（並び替え）です。ソート済みリストを生成するには O(n log n) の時間がかかりますが、証明者がソート済みの出力と元のリストの各要素からのマッピングを提供すれば、リストが正しくソートされている（そして与えられた元のリストに対応している）ことを検証するには、1回のパスだけ、つまり O(n) で済みます。

構文解析の場合も同じ構造です。構文解析とは、入力されたバイト列が与えられた文法に適合しているかどうかを判定し、適合している場合は、その適合性を示す構文解析木を生成するプロセスです。完全な構文解析アルゴリズムを実行することは、複雑なプロセスですが、 構文解析の結果を検証すること、特に構文解析木として表されるものについてはとても簡単です。パーサーの機能自体を回路にエンコードしたり、zkVM内でエミュレートしたりするのではなく ¹、Coral は信頼できないパーサーが構文解析木を生成したと仮定し、その出力がプライベートな元のバイトストリームとパブリックな文法に関して正しいかどうかを確認することだけに焦点を当てています。

しかし、これはデータ表現の問題を生み出します。標準的な文脈自由文法（CFG）の構文解析木は、自然に任意の数の子ノードを持つノードを含みます。このような可変次数のノードは、子ノードの数が固定された均一な構造を好む回路ベースの証明システムにはうまく対応できません。Coral は、古典的なコンパイラ技術の変換を適用することでこれを克服します。構文解析木は、左子右兄弟（LCRS）二分木に変換されます。これは同じ構造をエンコードする表現ですが、各ノードが最大2つの出力エッジしか持たないことを保証します。1つは最初の子へ、もう1つは次の兄弟へのエッジです。この二分の均一なレイアウトは、元の文法の完全な意味を保持しながら、各ノードが持つ子の数が固定されているR1CS制約の構造と整合します。

R1CSに自然に適合する二分構文解析木構造により、次の課題は、証明システム内でそれを段階的に効率的に検証する方法です。Coral は、独自に設計した特化型のNPチェッカーを採用します。これは、ツリーの各ノードが文法と基礎となるバイトストリームの両方に一致していることを確認する、同じ処理を繰り返す検証ループです。このループは均一かつ再帰的であるため、Novaのような折りたたみスキームと互換性があり、数千の検証ステップを単一の簡潔な証明に集約することができます。

このNPチェッカーを実装するには、複数の種類のメモリを慎重に扱う必要があります。読み取り専用のパブリックな文法ルール、永続的なプライベート構文解析木、そして木の走査中に使用されるスタックです。Coral は、これらを区画分けされたメモリ管理の仕組みにまとめ、パブリックとプライベート、永続性と揮発性の領域に対して単一のインターフェースを提供します。この設計により、チェッカーは各ステップで必要なメモリに正確にアクセスでき、同時に全体的な構造をシンプルに保ち、折りたたみスキームとの互換性を維持します。

その結果、クリーンでモジュール化されたシステムが実現します。（ドキュメントに属する）バイト列は一度コミットされ、構文解析木に変換され、その後NPチェッカーとそのメモリ管理を介してゼロ知識で検証されます。これは控えめなスペックのマシンでもスムーズにスケールします。このシステムでは、効率性が極めて重要です。ZKで構文解析について推論しようとした従来のアプローチは、zkVMに依存してCPU全体とパーサーを高いオーバーヘッドでエミュレートするか、文法をチョムスキー標準形に書き換える必要があり、文法のサイズを膨張させ、除外ルールなどの実用的な機能を失っていました。Coral はこれら両方の落とし穴を回避し、あらゆる文脈自由文法で使用できます。

Rustで書かれた実装は、JSON APIレスポンス、TOML設定ファイル、Cソースコードのサブセットなど、現実的な入力の構文解析を証明します。証明は簡潔（20 kB未満）で、生成が高速（数秒）、検証が低コスト（70ミリ秒未満）です。重要なのは、数ギガバイトのメモリしか必要とせず、特別なハードウェアも不要なため、通常のノートパソコンでも実行可能であることです。

より広範な応用に向けて

ゼロ知識での構文解析が実現可能になったことで、新たな道が開かれます。たとえば、証明者はTLSトランスクリプトにコミットし、特定のフィールドが存在することだけでなく、トランスクリプト自体が関連する文法の下で正しく解析されたことを証明できます。ユーザーは、不正な形式の入力が検証者を欺くことができないことを知った上で、トークンやその構造を明かすことなく、認証情報の特性を証明できます。多くの場合不透明で監査が困難なコンパイルチェーンは、構文解析ステップを含めて、ソースコードからバイナリまでエンドツーエンドで証明できます。ミドルボックスでさえ、不透明なバイトストリームを信頼するのではなく、トラフィックの構文構造に関する証明に依拠できるため、プライバシーを尊重しながらポリシーを実施できます。

Coral は完全な解決策ではありません。HTML、PDF、Pythonなど、多くの実世界のフォーマットは文脈自由ではありません。実際には、一般的に使用される多くの文法が優先順位や複雑な否定述語に依存していますが、これらはまだサポートしていません。文脈依存の機能を扱えるように Coral を拡張することは、未解決の重要な課題として残っています。しかし、バイト列へのコミットメントと構造化されたオブジェクトに対する証明との間の根本的なギャップに対処することで、Coral は新世代のZKシステムの基盤を築きます。

構文解析は、暗号プロトコルの洗練性と比べると平凡に見えるかもしれませんが、実際には様々な場面で重要な土台となります。入力が正しく解析されるという保証がなければ、より高レベルの証明は砂の上に築かれているかのような不安定な基盤に築かれることになります。Coral はこのような砂の土台から成長します。証明を一つずつ積み重ねて、それを堅固なものにしていきます。Coral は、土台形成をゼロ知識の領域に持ち込むことができることを実証します。高速で、簡潔で、実用的です。構文解析を証明可能にすることで、検証可能性とプライバシーがトレードオフではなくパートナーとなり、私たちが依存する構造化されたオブジェクトが暗号証明そのものと同じ厳密さで推論できるアプリケーションを、Coral が解き放つ手助けとなることを願っています。

詳細について

CoralはIEEE S&P 2026に採択されました。もっと詳しく知りたい方はぜひご参加ください！また、私たちのコードで試してみることもできます： https://github.com/eniac/coral