zkCraft: 技術的サマリー（日本語）

本論文は、ゼロ知識証明（ZK）回路のバグ発見とデバッグを目的とした新しいフレームワーク**「zkCraft」**を提案するものです。ZK 回路はプライバシー保護やスケーラビリティの基盤ですが、証跡（witness）の計算と回路制約の整合性が厳密に取れていない場合、深刻なセキュリティ脆弱性（制約不足や過剰制約）が発生しやすくなります。zkCraft は、決定論的な LLM 駆動のムテーション（変異）と、証明を伴う探索（proof-bearing search）を組み合わせることで、従来のソルバー依存アプローチの限界を克服し、効率的かつ正確な脆弱性検出を実現します。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細をまとめます。

---

1. 問題定義と背景

ゼロ知識回路（例：Circom）の開発において、以下の 2 種類の主要な論理的欠陥が存在します。

• 制約不足（Under-constrained）: 有効な証跡（witness）が存在しない実行トレースが、回路制約を満たしてしまう状態。これにより、不正な入力が正当な証明として承認されるリスクがあります。
• 過剰制約（Over-constrained）: 有効な証跡が存在するにもかかわらず、回路制約がそれを拒絶してしまう状態。

既存のアプローチには以下の課題がありました。

• 静的解析・パターンベース: 構文エラーは検出できるが、証跡生成時や特定の入力でのみ現れる意味論的な不一致を見逃しやすい。
• 形式検証/SMT: 強力な保証を提供するが、大規模な回路にはスケーラビリティが不足しており、プログラム編集と入力割り当ての組み合わせ探索空間が膨大になる。
• 従来のファジング: 多くの高コストなソルバー呼び出しに依存するか、無指向的な変異により低価値な候補を多数生成してしまう。
• LLM 活用: 高品質なテストパターンを生成できるが、証明を伴う探索と分離されており、検証コストが高く、偽陽性（False Positive）が多い傾向がある。

2. 手法：zkCraft のアーキテクチャ

zkCraft は、代数的局所化、簡潔な違反証明、そして決定論的なプロンプト誘導型ムテーションテンプレートを密接に結合した ZK ネイティブなパイプラインです。

2.1 ステージ 1: スパース署名抽出と候補プールの選定

• 各制約行（R1CS 行）に対して、証跡変数と定数/公的変数の非ゼロ係数インデックスのサポート（supp）を分析します。
• 行ごとに診断スコア（κw, κc）を計算し、ハッシュに基づいたコンパクトな「指紋（fingerprint）」を生成します。
• スコアに基づき、脆弱性発見の可能性が高い上位 32 行程度を「候補プール（Rcand）」として選定します。これにより探索空間を大幅に削減します。

2.2 ステージ 2: Row-Vortex 承諾と Violation IOP（ZK ネイティブエンジン）

これが zkCraft の中核となる技術革新です。

• Row-Vortex 多項式: 候補行の選択（δ）と置換定数（c）を、2 変数多項式 $R(X, Y)$ としてエンコードします。これにより、多数の SMT/SAT クエリを単一の代数的存在証明に集約します。
• Violation IOP (Interactive Oracle Proof): 証明者（Prover）は、編集された制約を満たしつつ、元の公開出力と異なる出力を生み出す証跡（witness）の存在を、Violation IOPを用いて証明します。
  • 具体的には、Sum-Check プロトコルを用いて、編集された残差と出力の差分（$\Delta_{out}$）がゼロでないことを代数的に証明します。
  • この証明 $\pi$ は、脆弱性の存在を認証するだけでなく、具体的なカウンターエグザンプル（反例）を復元可能な形式で含みます。
• Row-Vortex 承諾: 効率的な多項式承諾（例：HyperPlonk+ や BaseFold）を用いて、行選択と置換パラメータをコンパクトに束縛します。

2.3 ステージ 3: 決定論的有限体合成と LLM オーラクル

• LLM オーラクル（オプション）: 大規模言語モデル（LLM）を「ゼロショット・パターンオーラクル」として利用します。
  • Mutation-Oracle: 右辺式をエッジケース（0, $q-1$, 小定数など）にバイアスした変異テンプレートを生成します。
  • Pattern-Oracle: 発見されたカウンターエグザンプルから、入力サンプリングをバイアスする Rust 関数を生成します。
  • 重要点: LLM はソルバーではなく、探索を誘導するテンプレート生成器として機能します。すべての提案は ZK 証明によって検証されるため、LLM の誤りによる偽陽性は防がれます。
• 証明からのカウンターエグザンプル復元: 検証者が証明 $\pi$ を受け入れると、コミットメントのオープン値から具体的な置換定数 $c$ と証跡 $w'$ を復元し、具体的なバグを含むプログラム $P'$ と入力 $x'$ を合成します。これにより、追加の TCCT（Trace-Constraint Consistency Test）実行なしでバグを確認できます。

3. 主要な貢献

1. ZK ネイティブ検索フレームワーク: 小さな脆弱性誘発編集の探索を、単一の代数的存在ステートメント（Row-Vortex 多項式）にマッピングし、Violation IOP で認証する新しいアプローチを提案しました。
2. 決定論的 LLM 統合: LLM を証明生成から分離された「テンプレートオーラクル」として設計し、探索の質を向上させつつ、LLM の非決定性や誤りを証明ベースの検証で排除しました。
3. 実用的な実装技術: 行ごとのコンパクトな指紋抽出、候補プールの選定ヒューリスティック、証明埋め込みエンコードからの具体的な置換復元（有限体合成）を実装しました。
4. 証明付きカウンターエグザンプル: 脆弱性の発見と、開発者が検証可能な具体的な反例（実行トレース）の提供を同時に行う「Proof-as-Counterexample」を実現しました。

4. 評価結果

452 件の実世界の Circom テストスイート（小〜超大規模）を用いた評価結果は以下の通りです。

• 検出精度: zkCraft はすべての回路サイズにおいて、既存のツール（Circomspect, ZKAP, Picus, ZKFUZZ など）を上回る真陽性（TP）数を達成しました。
• 偽陽性（FP）: zkCraft は偽陽性を 0に抑え、精度（Precision）が 100% でした。一方、既存のファジングツールや静的解析ツールは 10〜50% 程度の偽陽性率を示しました。
• 発見速度: 2 時間の時間制限内で、zkCraft は既存手法よりもはるかに早くバグを発見しました（90% 以上のバグを 100 秒以内に発見）。
• ソルバー呼び出しの削減: 従来の SMT/SAT ベースのアプローチに比べ、ソルバーとの対話を大幅に削減し、ZK 証明による検証に置き換えることでコストを低減しました。
• 未発見バグの発見: 既知のベンチマークに加え、開発者によってパッチされた新規の脆弱性（所有権偽造、暗号計算バグなど）を多数発見しました。

5. 意義と将来展望

• 形式検証と自動デバッグの架け橋: zkCraft は、形式検証の厳密さとファジングの拡張性を融合させ、大規模な ZK 回路開発における堅牢性を向上させるスケーラブルな道筋を示しました。
• 実用的なセキュリティ保証: 証明付きのカウンターエグザンプルは、開発者のデバッグプロセスを大幅に効率化し、脆弱性の根本原因分析を加速します。
• 将来の展開: より高度な記号的簡略化の統合、他のドメイン固有言語（Noir など）や zkVM への対応、および大規模回路向けのハードウェアアクセラレーション（GPU/FPGA）への拡張が今後の課題として挙げられています。

結論として、zkCraft は、ゼロ知識回路のセキュリティを高めるための、実用的で検証可能かつ効率的な次世代ファジングフレームワークとして、ZK 分野のセキュリティ研究と実装に重要な進展をもたらしました。