AIは暗号技術と出会う 2: AIがOpenVMのZkVMで見つけたもの

これはシリーズの2番目の投稿です。 最初のCloudflareのCIRCLに関する投稿をまだ読んでいない場合は、これらの実験を実行する理由とパイプラインのセットアップ方法について、より詳しいコンテキストが含まれています。 この投稿では、AI監査ツールであるzkaオをOpenVMのzkVMに向け、悪意のあるプロバーがあらゆるペアリング等式を偽造できるゲストライブラリopenvm-pairingに重大な健全性バグを発見しました。 注意点として、これはzkVMの証明システム自体の健全性バグではなく、脆弱なライブラリを使用するコードにのみ影響します。 この投稿で取り上げたバグはCVE-2026-46669として割り当てられ、OpenVM 1.6.0で修正されました。 私たちが知る限り、OpenVMを基盤に構築しているすべてのパートナーは、その後そのバージョンにアップグレードしています。 注意：最初の投稿と同様の明確化です。AIは最終報告ではなく、候補となる発見を生成しました。私たちのチームの人間がその問題を検証し、悪用可能性を確認し、完全な影響と影響を受けるプロジェクトを理解し、開示を処理しました。 この場合、zkaオが生成した詳細なレポートと最小限のPoCのおかげで、OpenVMチームと共有する価値があると判断するために、非常に迅速な手動トリアージで十分でした。 どのようにして起こったのか 4ヶ月前、私たちはAI実験の一環としてOpenVMをスキャンしました。最初のスキャン方法は、単純なプロンプトを持つLLM、次に専門家が維持するスキルを持つLLMを使用するという、すべてをスキャンするのと同じ方法でした。 Opus 4.6とCodex 5.3で実行しました。 Opus 4.7とCodex 5.4が出た直後に、再度実行しました。 候補となる発見はすべて有効な観測であり、モデルはそれらのいくつかを自信を持って「クリティカル」または「ハイ」とラベル付けしましたが、実際には悪用可能なものは何もありませんでした。 私たちの仮説は、zkVMは単純に、300Kトークン、あるいは1Mトークンのコンテキストでも、ナイーブなLLMセットアップでは処理するには複雑すぎるということでした。 モジュール間の依存関係は、典型的なライブラリよりもはるかに密です。 暗号ライブラリは、各サブエージェントに単一の暗号プリミティブに対応するフォルダを渡すだけで、並列に監査できることがよくあります。 各サブエージェントは少数の行を読み、関連するスキルのみを適用し、発見事項をマークダウンファイルに書き込み、メインエージェントがこれらのファイルを結合します。 これらすべては、Claude CodeやCodexのような一般的なエージェントコーディングツールで、ほとんど人間の指示なしに、そのまま実行されます。 そのアプローチは、OpenVMのようなより複雑なコードベースには適用できません。 そこでは、ローエンドのフルーツ（容易に見つかるバグ）を除いて、サブエージェントの有用な出力はバグのリストではありません。 証明可能な安全なモジュールAと証明可能な安全なモジュールBがあっても、それらを組み合わせると安全ではなくなる可能性があります。 したがって、「分離」モードでバグを探しても、意味のあるバグを見つけることはできません。 代わりに、サブエージェントの出力はモジュールに関する知識であるべきです。つまり、モジュールが何を仮定し、呼び出し元に何を委譲し、どのような不変条件を静かに依存しているかです。 しかし、そのような出力をうまく表現することが難しい部分です。 短すぎると、バグが実際にある実装の詳細をスキップしてしまいます。 長すぎると、他のものと組み合わせる前にメインエージェントのコンテキストをオーバーフローさせてしまいます。 私たちがこれまでに見た限りでは、少なくとも執筆時点では、この問題は上記のエージェントコーディングツールでは効率的に解決されていません。 その仮説を念頭に置いて、これらの実験の元のルールでは、プレーンLLMがすでに実際のバグを見つけた後にのみzkaオを実行することになっていましたが、私たちはzkaオをOpenVMで実行することにしました。 私たちはzkaオのコンテキストエンジニアリングに多くの時間を費やし、脆弱性を見つけるための再利用可能なフローとして、私たち自身の専門家の作業方法をエンコードしました。そのため、この状況にまさに適したツールであるように思われました。 9時間半以上のスキャン後、多数の発見事項が返されました。 以前の実験と同様に、すべての発見事項を詳細に調べる時間がありませんでした。 クイックパスの後、1つがすぐに際立ちました。それは、ゲストライブラリの1つにおけるペアリングチェックの重大な健全性バグでした。 私たちの仮説は正しく、数ヶ月の努力が報われました！ 共有できるバグは1つだけですが、最初の投稿との一貫性を保つために、バグの概要を以下に示します。 重大度と修正の概要 # バグ | AIの重大度 | OpenVMの重大度 | 修正コミット | 発見者 ---|---|---|---|--- 1 | openvm-pairingペアリングチェックにおけるスケーリングファクターの適切なサブフィールドチェックの欠落 | クリティカル | クリティカル | a720e2c | zkao 今回は、AIの重大度とメンテナーの重大度が一致しています。 バグ1: openvm-pairingペアリングチェックにおけるスケーリングファクターの適切なサブフィールドチェックの欠落 背景 ペアリングは、Groth16、PLONK with KZG、およびBLS署名のエンジンです。 これらのプロトコルすべてにおいて、検証者は通常、1つのペアリング値を求めているわけではありません。 彼らは、ペアリングの積が1であるかどうかを尋ねています。 $$ ext{Π}_i e(P_i, Q_i) = 1. $$ この「はい」か「いいえ」の回答から、検証者はSNARK証明が有効である、KZG開示が正しい、または署名が検証されると結論付けます。 したがって、プロバーが偽のペアリング積を1に見せかけることができれば、その上に構築されたすべてはもはや健全ではなくなります。 ペアリングとは、双線形写像です。 $$ e : G_1 imes G_2 o G_T, $$ ここで、$G_1, G_2, G_T$ はアーベル群です。 この場合、$G_1$ と $G_2$ は楕円曲線群であり、$G_T$ は $ ext{F}_{p^{12}}^{*}$ の乗法部分群です。 ペアリングの最も重要な特性は双線形性です。 $$ e([a]P, [b]Q) = e(P, Q)^{ab}. $$ これがペアリングが有用な理由ですが、バグを理解するためにこの特性を実際に使用する必要はありません。 したがって、それを無視しても構いません。 ペアリング $e(P, Q)$ の計算には、2つの主要なステップがあります（Weilペアリングを除く）。 最初のステップはミラーループです。 これはミラー関数 $f_{r, Q}(P)$ を評価します。これは単純化のためにブラックボックスとして見なすことができます。 このステージは $ ext{F}_{p^{12}}^{*}$ の要素を出力します。 ペアリングの積の場合、回路はすべてのミラーループを実行し、それらの出力を掛け合わせることができます。 その結合された出力を $f$ と呼びましょう。つまり、$f = ext{Π}_i f_{r, Q_i}(P_i)$ です。 ただし、注意点があります。$f$ はまだペアリングの積ではありません。 それは、同値類 $ ext{F}_{p^{12}}^{*} / ( ext{F}_{p^{12}}^{*})^r$ の単一の代表者です。 これは、NovakovicとEagenの論文からの主要な観察の1つです。 ミラーループの出力は、 $r$ 乗の積による乗算までしか一意ではありません。 言い換えれば、$f_1$ と $f_2$ は、非ゼロの $c$ が存在して $f_1 = f_2 ext{・} c^r$ となる場合に、同じペアリングを表します。 この決定されていない因子 $c$ が、直接的な等式チェックを難しくしています。 だからこそ、2番目のステップが存在します。 最終的な指数計算は、$f$ を次のようにべき乗します。 $$ h = rac{p^{12} - 1}{r}. $$ これにより曖昧さが解消されます。なぜなら、すべての非ゼロの $c$ に対して、次のようになります。 $$ (f ext{・} c^r)^h = f^h ext{・} c^{p^{12}-1} = f^h. $$ 最後の項は、 $ ext{F}_{p^{12}}$ のすべての非ゼロ要素が $x^{p^{12}-1} = 1$ を満たすため消滅します。 この指数計算の後、結果は $G_T$、つまり $r$ 乗根の群に着地します。 したがって、実際のペアリング積チェックは次のようになります。 $$ f^h = 1. $$ 問題は、指数 $h$ が回路内で計算するには高すぎるコストがかかることです。 一方、プロバーが回路外で $c$ を計算し、ヒントとして渡すことは問題ありません。 $f = c^r$ をチェックすることは、$f^h$ の指数計算を実行することよりもはるかに安価です。 したがって、$ ext{Π}_i e(P_i, Q_i) = f^h = 1$ を証明するために、$f^h$ を直接計算する代わりに、プロバーは $f = c^r$ という安価な方程式を満たす非ゼロの $c$ を提供するだけで済みます。これは、$f^h = 1$ と正確に等価です。 これが最適化の核心的なアイデアです。 OpenVMは、NovakovicとEagenの論文のレジデュー・ウィットネス・トリックを使用してこれを実装しています。 プロバーはいくつかの追加値を提供し、回路は完全な指数計算を実行する代わりに安価な方程式をチェックします。 実際には最適化された方程式は $f = c^r$ とはわずかに異なります。 $$ f ext{・} u = c^{ ext{λ}} ext{ ∧ } u^{d^i} = 1 $$ ここで $ ext{λ} = m ext{・} r$ は、回路がFrobeniusマップを通じて $c^{ ext{λ}}$ を安価に評価できるような、曲線固有の指数であり、$u$ はスケーリングファクターと呼ばれます。 OpenVMのコードでは、このスケーリングファクターはBN254ではu、BLS12-381ではsと呼ばれます。 残りのシンボルは $d = ext{gcd}(m, h)$ と $i = v_d(h)$ です。 スケーリングファクターは、 $ ext{λ}$ が元の $r$ 乗根チェックと完全に一致しないため必要です。