技術概要：ZKFUZZ — ゼロ知識回路の効果的なファズテストの基盤とフレームワーク

1. 問題定義

ゼロ知識（ZK）回路は、プライバシー保護計算の基盤であり、匿名暗号通貨から検証可能な機械学習に至るまで、さまざまなアプリケーションにおいて簡潔な証明と効率的な検証を可能にします。しかし、汎用計算ロジックと有限体多項式制約の間のミスマッチにより、正しい ZK 回路の開発は極めて困難です。

脆弱性には主に 2 つのクラスが存在します。

• 制約不足（Under-constrained）回路: 制約が緩すぎ、悪意のある証明者が無効な証人（witness）に対して有効な証明を生成できてしまう（完全性（soundness）の違反）。
• 制約過多（Over-constrained）回路: 制約が厳しすぎて、誠実な証明者からの有効な証人をシステムが拒絶してしまう（完全性（completeness）の違反）。

既存の検出手法には重大な限界があります。

• 静的解析: Circomspect や ZKAP などのツールは、高い偽陽性率に悩まされ、特に中間計算や異常なプログラム終了に関連する深い意味論的な問題を捉えきれていません。
• 形式手法: SMT ソルバーに依存するツール（Picus、ConsCS など）は、現実世界の回路規模へのスケーリングに苦しみ、脆弱性の定義が不完全に依存している傾向があります。制約における非決定性のみを焦点とし、計算が中止される場合や中間値が不一致となるケースを無視しています。
• 定義の欠落: 従来の ZK バグの形式的定義は不完全です。「異常終了」（計算はクラッシュするが制約は満たされている状態）を無視したり、中間値を含む実行トレースの完全なセットを考慮できていなかったりします。

2. 手法

2.1 理論的基盤：トレース - 制約整合性テスト（TCCT）

著者は、ZK 脆弱性を 2 つの集合間の不一致として定義する言語非依存の形式的フレームワークであるTCCTを導入します。

1. トレース集合 $T(P)$: 証人計算プログラム $P$ によって生成されるすべての可能な実行トレース（入力、中間値、出力）の集合。
2. 制約充足集合 $S(C)$: 回路制約 $C$ を満たすすべてのタプル（入力、中間値、出力）の集合。

TCCT は、以下の条件を満たす場合にのみ回路が適切に制約されていると定義します。

• 制約不足の不存在: $S(C)$ の入力 - 出力ペアへの射影が、$T(P)$ の射影の部分集合であること。これにより、無効なトレースが受け入れられないことを保証します。
• 制約過多の不存在: $T(P)$ が $S(C)$ の部分集合であること。これにより、すべての有効なトレース（特定の中間値を含む）が受け入れられることを保証します。

この定式化は、計算の中止（$P$ は失敗するが $C$ は入力を受理する）や中間値の不一致によって引き起こされる脆弱性を捉えており、これらは従来の定義では見落とされていました。著者は、制約不足または制約過多の判定が NP 完全であり、完全な TCCT は co-NP 完全であることを証明しています。

2.2 システム設計：ZKFUZZ

ZKFUZZ は、プログラム変異と入力の生成を同時に行うアプローチを用いて TCCT 違反を検出する動的解析フレームワークです。入力のみを変異させる従来のファズテストとは異なり、ZKFUZZ はプログラムロジックと入力の両方を変異させます。

コアワークフロー:

1. 変異: システムは、元の計算プログラム ($P$) の変異体 ($P'$) を生成します。変異には、アサーションの削除、代入の変換（演算子や値の置換など）、弱い代入の修正が含まれます。
2. 実行: 元のプログラム ($P$) と変異体 ($P'$) の両方を、サンプリングされた入力 ($x$) に対して実行します。
3. 検証:
   • 制約過多の検出: $P(x)$ が有効なトレースを生成するが $C$ に失敗する場合、回路は制約過多です。
   • 制約不足の検出: $P'(x)$ が異なる出力 ($y' \neq y$) を持つトレースを生成し、それでも $C$ を満たす場合、回路は制約不足です（変異体のロジックは意味論的に異なるため、出力は受理されるべきではないからです）。
4. ガイド付き探索: 大規模な素数体と無限の変異可能性という広大な探索空間をナビゲートするため、ZKFUZZ は遺伝的アルゴリズムを採用します。
   • 適合度関数: 新規の最小和適合度関数は、与えられたトレースにおけるすべての制約の制約エラーの合計を計算します。変異体は、サンプリングされた入力全体にわたる最小エラー合計によってスコア付けされます。これは従来の最大値のみの手法とは異なり、同時変異に適しています。
   • ターゲットセレクター: システムは静的解析を用いて、変異と入力生成を以下の高リスクパターンへと誘導します。
     • ゼロ除算: 分子と分母の両方がゼロとなる入力を生成する。
     • ハッシュチェック: 入力をハッシュ等値制約を満たすように強制する。
     • 偏った分布: 境界ケース（0、1、および体法 $q$ に近い値）への入力生成をバイアスする。
     • ホワイトリスト: 誤りやすいコードに集中するため、既知の安全なテンプレート（例：IsZero、Num2Bits）をスキップする。

3. 主要な貢献

1. TCCT フレームワーク: 従来の定義を包含し、異常終了や中間値の不一致に起因する ZK バグの全領域を捉える、統一された言語非依存の形式的モデル。
2. ZKFUZZ システム: TCCT 違反を検出するためにプログラムと入力を同時に変異させる新規ファズテストフレームワーク。最小和適合度関数とガイド付き探索ヒューリスティックを活用。
3. 実証的検証: 452 の現実世界の Circom 回路を用いた評価により、最先端のツールを上回る性能を実証。
4. Noir プロトタイプ: 異なる ZK DSL である Noir 向けの実装プロトタイプ。フレームワークの言語非依存性を示す。

4. 結果

著者は、Circomspect、ZKAP、Picus、ConsCS という 4 つの最先端ツールと比較し、452 の現実世界の Circom 回路に対して ZKFUZZ を評価しました。

• バグ検出: ZKFUZZ は85 の固有のバグを特定し、そのうち59 は以前は未知のゼロデイ脆弱性でした。このうち 39 は開発者によって確認され、14 は修正されました。
• 比較: ZKFUZZ は、さまざまな回路サイズにおいて、既存のツールよりも30% から 300% 多くのバグを発見しました。
• 精度: ZKFUZZ は**100% の精度（偽陽性ゼロ）**を達成しました。一方、Circomspect や ZKAP などの静的解析ツールは高い偽陽性率（精度は 0.06 から 0.75 の範囲）を有していました。
• 速度: ターゲットセレクターを備えた ZKFUZZ++ は、100 秒以内に 90% 以上のバグを特定し、形式手法や静的解析ツールを大幅に凌駕しました。
• 影響: 発見されたバグには、zk-regex や passport-zk-circuits などのプロジェクトにおける重要な制約不足の脆弱性が含まれており、攻撃者が証明を偽造したり資金を抜き取ったりする可能性がありました。

5. 意義と主張

本論文は、ZK 回路のセキュリティにおいて、従来の脆弱性定義の根本的な不完全性に対処することで、ZKFUZZ が重要な進歩を遂げたと主張しています。バグをトレース - 制約の不一致（TCCT）として形式化することで、著者は、制約の非決定性のみを焦点とするツールでは以前は検出不可能だった大規模な脆弱性クラス（評価において現実世界のバグの約 50%）を露呈させました。

偽陽性なしにバグを検出できるこのシステムの能力は、偽陽性の高い静的解析ツールからのアラートを無視しがちな開発者にとって、実用的なツールとなります。さらに、Noir 回路におけるバグの検出に成功したことは、TCCT フレームワークと ZKFUZZ アーキテクチャが Circom に限定されず、標準化された制約形式にコンパイルされる他の ZK 言語にも一般化可能であることを示唆しています。

著者は、彼らの研究が計算と制約のミスマッチ（完全性と完全性）に起因する脆弱性に焦点を当てており、基盤となる証明システム内のバグ、純粋なロジックエラー（未使用の入力など）、またはプロトコルレベルのゼロ知識漏洩は明示的に除外されていることを強調しています。