技術的概要：Veritas

問題定義

ストリpped（シンボル情報が除去された）バイナリにおけるメモリ破損脆弱性（MCV）の検出は、根本的な意味論的再構築の課題を呈する。ソースコード分析とは異なり、バイナリ分析では、コンパイルとシンボル除去により高レベル構造、オブジェクト境界、明示的な制御フローが失われたアーティファクトから、メモリオブジェクトがどのように割り当てられ、伝播し、制約され、関数間でアクセスされるかを回復しなければならない。

最近の大規模言語モデル（LLM）に基づくアプローチはコード理解を向上させたが、以下の 3 つの主要な理由により、バイナリ MCV 検出においては困難に直面している：

1. 共有状態の追跡: 脆弱性は、直接的な呼び出しチェーンの辺を持たない非連結関数間における、共有メモリ領域に関する不整合な仮定から生じることが多い。標準的な呼び出しグラフの拡張は、これらの依存関係を捉えることができない。
2. 意味論的損失: 回復された表現は断片的である。リフトされた LLVM IR は低レベルのメモリアクセスパターンを保持するが、SSA 変数やキャストといったコンパイラアーティファクトによって曖昧化される。一方、デコンパイルされた C コードは高レベル構造を提供するが、メモリ操作を一般的なオフセット式に縮小し、オブジェクトの同一性を消去する。
3. 制約検証: 静的解析では、疑わしいアクセスが実行可能なパス条件下で到達可能かどうかを決定できないことが多い。実行可能な証拠がない場合、LLM はメモリ感受性操作への攻撃者制御データの伝播の証明ではなく、構文の代理指標に依存するため、脆い推論と高い偽陽性率を招く。

既存のエージェントフレームワーク（ソースコード向けに設計され、要約や呼び出しグラフの拡張に依存するもの）は、必要な意味論的構造が構造的に部分的に欠如しているストリpped バイナリが提示する意味論的回復の問題を解決しない。

手法

Veritas は、LLM の推論を実証可能なプログラム意味論と実行可能動作に制約するように設計された、ハイブリッドで意味論的基盤を持つエージェントフレームワークである。分析は、静的基盤（回復されたプログラム事実）とランタイム基盤（具体的な実行証拠）という 2 つの基盤レイヤーと整合する 3 つの段階に整理される。

1. 意味論駆動型コンテキストスライサー（静的基盤）

スライサーは LLM を使用せず、リフトされた LLVM IR から、証拠に基づくコンパクトなソース・ツー・シンクフローを抽出する。

• 関間伝播グラフ: RetDec を用いてバイナリを LLVM IR にリフトし、呼び出し、戻り、およびグローバル依存関係を符号化した型付き関間伝播グラフ（$G_P$）を構築する。このグラフは、汚染関連の値（ポインタ、オフセット、長さ）が関数間でどのように伝播するかを追跡する。
• 証拠に基づくフロー抽出: 到達可能なすべてのソース・シンクペアを意味あるものとして扱うのではなく、スライサーは有界な関間証拠を検証する。入力ソース（例：fread）からメモリリスクシンク（例：危険な API 引数）へ汚染トークンを追跡し、定義 - 使用チェーンとメタデータを用いて各関数境界での伝播を検証する。
• フローオブジェクトの構築: 承認された証拠は、順序付けられた関数、汚染関連トークン、および「アンカーキュー」（出所クラスとエンドポイント注釈）を含むコンパクトなフローオブジェクトに変換される。これにより、下流の分析のための完全なバイナリに代わり、意味論的に完全な小規模なコンテキストが提供される。

2. 二重ビュー脆弱性検出器（制御された LLM 推論）

検出器は、意味論的損失を克服するために二重ビュー入力表現を用いて、証拠に基づくフロー上で段階的な推論を行う。

• 二重ビュー表現: ソース関数とシンク関数に対して、LLM は制御フロー推論のためのデコンパイルされた C コードと、メモリ操作およびシンク意味論を曖昧さなく解明するためのリフトされた LLVM IR の両方を受け取る。中間関数については、主にアンカーキューに導かれたデコンパイルされたコードを使用する。
• 段階的推論: LLM はフローを 1 関数ずつ分析し、伝播値、エイリアス、境界のインベントリを含む累積推論状態を維持する。この状態は、代入や制御フローの決定に基づいて更新され、フロー全体を一度に処理することによるコンテキスト制限を回避する。
• トライベースのメモ化: 冗長性を削減するため、システムは共有フロー接頭辞に対する推論状態をメモ化し、フローの一意な接尾辞に対してのみ LLM を呼び出す。
• 整合性チェック: 候補を報告する前に、検出器は最終的なパス感応検証を行い、汚染値が脆弱性関連であり、実行可能な条件下でシンクアクセスがメモリ安全性に違反することを保証する。

3. 自動脆弱性検証器（ランタイム基盤）

検証器は、検出器の仮説を実行可能なチェックに変換し、候補を確認または反証する。

• アーティファクト準備: Radare2 を使用して、デコンパイラビューとランタイムデバッグの間のギャップを埋め、検出器の仮説を RVAs（相対仮想アドレス）やシンボルといった実行可能座標にマッピングする。
• マルチエージェント協調: 3 つのエージェントが検証を調整する：
  • ストラテジスト: 検証を計画し、計装ターゲット、ブレークポイント、およびトリガーモード（ファイル、ネットワーク、CLI）を選択する。
  • 検証者: プランを実行し、概念実証（PoC）を生成して、デバッガ（Radare2）またはメモリチェッカ（Valgrind）下でバイナリを実行し、クラッシュや無効なアクセスを観察する。
  • エクスプローラー: 初期証拠が不十分な場合、代替状態または関連関数をプローブして、支持証拠を見つける。
• 確認: 具体的なランタイム証拠（例：セグメンテーションフォルト、Valgrind エラー、または特定のメモリ状態）が報告されたシンク、アクセスパターン、および根本原因を裏付ける場合にのみ、脆弱性が確認される。

主要な貢献

1. Veritas フレームワーク: 静的プログラム分析とランタイム検証を統合し、ストリpped バイナリにおけるメモリ破損を検出する、意味論的基盤を持つエージェントフレームワーク。
2. 3 段階アーキテクチャ:
   • LLM を使用せずにリフトされた IR から証拠に基づくフローを抽出するスライサー。
   • 意味論的曖昧さを解決するために選択的 IR サポートを用いてフロー上で推論を行う二重ビュー検出器。
   • デバッガから可視なアーティファクトと具体的な実行を用いて仮説を確認する検証器。
3. 詳細なベンチマーク: 基盤バイナリ検出を評価するために構築された、トレースレベルのグラウンドトゥルースを備えた 20 の実世界バイナリメモリ破損事例のキュレーションデータセット。
4. 性能: 評価により、Veritas はベンチマークで90% のリコールを達成し、静的アナライザ（0% のリコール）、ファジング（10% のリコール）、エージェントベースライン（25–35% のリコール）を大幅に上回ることが示された。623 の候補に対する包括的検証において偽陽性はゼロであり、より大規模なサンプリング監査では偽陽性が 2 つのみであった。
5. 実世界での発見: Veritas は、Apple の Universal Scene Description ライブラリ（libusd_ms.dylib）における、以前は知られていなかったゼロデイの境界外読み取りを発見し、これが確認されて CVE が割り当てられた。

結果と意義

本論文は、LLM ベースの脆弱性発見の有効性は、モデルの内在的な能力のみならず、推論に必要な意味論的構造を回復する周辺インフラの能力に依存すると主張している。

• 設計原則としての意味論的基盤: 結果は、運用上の設計原則としての意味論的基盤を支持する。LLM の推論を明示的なメモリ関連事実（静的基盤）に制約し、実行可能な動作に対する結論を検証（ランタイム基盤）することで、Veritas は制約のないモデルの推測の脆さを回避する。
• ベースラインに対する優位性: 従来のツールは、関間における意味論的基盤の欠如により失敗する。エージェントベースラインは、メモリオブジェクトのライフサイクルの明示的なモデルが欠如し、誘導されない探索や構文パターンに依存するため失敗する。Veritas は、確定的分析を用いて伝播を事前計算し、LLM を用いて複雑な意味論を解釈し、その後厳格なランタイム確認を行うことで、このギャップを埋める。
• コストと精度のトレードオフ: ランタイム検証は、PoC 生成とデバッグを必要とするため主要なコストボトルネックであるが、このフレームワークは、ストリpped バイナリ分析において高い精度を達成するには実行可能な証拠が必要であることを示している。システムは、スループットよりも検出の信頼性を優先しており、セキュリティ上重要なバイナリ分析にとって必要なトレードオフである。

本論文は、実用的なバイナリ脆弱性検出においては、推論が回復されたプログラム意味論と実行可能な証拠の両方にアンカーされなければならないと結論付けており、Veritas はそのモジュール式でハイブリッドなアーキテクチャを通じてこの原則を実装している。