論文「Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery」の技術的サマリー

この論文は、大規模な C/C++ コードベースにおける脆弱性発見の課題を解決するため、静的解析（Static Analysis: SA）、大規模言語モデル（LLM）、そして**記号実行（Symbolic Execution: SE）**を統合した新しい自動化パイプライン「Sailor」を提案しています。

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

---

1. 背景と問題定義

大規模な C/C++ プロジェクトにおける自動脆弱性発見には、以下の既存技術の限界が存在します。

• 静的解析（SA）: 数百万行のコードを高速にスキャンできますが、誤検知（False Positive）が多く、具体的な実行経路や状態の検証ができません。
• ファジング（Fuzzing）: 具体的な入力値でプログラムを実行しますが、深いライブラリ内部や、正確に構成されたプログラム状態を必要とする経路への到達が困難です。
• LLM による検出: 文脈を理解できますが、形式的な正しさの保証がなく、実行ベースの検証がないため、存在しない脆弱性を報告したり、真の脆弱性を見逃したりするリスクがあります。
• 記号実行（SE）: 入力値を記号値として扱い、制約ソルバーを用いて形式的に脆弱性を証明できます。しかし、大規模コードベースに直接適用するには**「ハネス（Harness）の作成」**がボトルネックとなっています。
  • ハネスとは、記号実行エンジンが対象関数に到達し、必要な状態をセットアップするためのドライバプログラムです。
  • 従来のハネス作成は、コードベースと SE エンジンの両方に精通した専門家による手作業が必要であり、スケーラビリティを阻害する主要な要因でした。

Sailor の目的: 静的解析で脆弱性の候補を特定し、LLM がその文脈に基づいてハネスを自動生成・改良し、記号実行と具体実行（Concrete Execution）で検証する、完全自動化されたパイプラインの構築です。

---

2. 提案手法：Sailor のアーキテクチャ

Sailor は、以下の 3 つのフェーズで構成されるエンドツーエンドのパイプラインです。

フェーズ 1: 静的解析に基づくターゲット生成 (Static Analysis Informed Target Generation)

• 目的: 大規模コードベースから脆弱性の候補を特定し、LLM がハネスを生成するための「脆弱性仕様（Vulnerability Specification）」を生成する。
• プロセス:
  1. 事実生成: CodeQL を使用し、34 種類のメモリ安全性クエリ（標準クエリ＋カスタムクエリ）を実行。
  2. 事実の補強: 対象関数周辺の呼び出し、ポインタ変数、長さ変数、ビルドコンテキスト（include パス等）を抽出。
  3. 仕様生成: 候補場所、脆弱性説明、エントリポイント、アサーションテンプレート（CWE 別）を JSON 形式でまとめる。
  • 特徴: 手作業なしで 619 件もの候補（例：Binutils における未チェックの memcpy）を特定し、LLM への入力として渡します。

フェーズ 2: LLM によるオーケストレーションされた記号実行 (LLM-Orchestrated Symbolic Execution)

• 目的: 生成された仕様に基づき、LLM が記号実行用のハネス（ドライバ、スタブ、アサーション）を反復的に合成・改良する。
• プロセス:
  1. ソース探索: LLM がプロジェクトのソースコードを読み込み、型定義や関数シグネチャを把握。
  2. ハネス合成:
     • ドライバ: 記号入力（klee_make_symbolic）のセットアップ、ガード条件の回避（klee_assume）、メモリ割り当てを生成。
     • スタブ: 対象経路外の関数をスタブ化（戻り値を記号値にする等）、ループを単一パスに変換し、経路爆発を抑制。
     • アサーション: 脆弱性条件（例：バッファオーバーフロー）を検知するための制約を追加。
  3. 反復改良ループ:
     • 生成されたコードをコンパイルし、KLEE（SE エンジン）で実行。
     • コンパイルエラーや KLEE のフィードバック（到達不可、バグ未発生など）を LLM に返却。
     • LLM はフィードバックに基づいてドライバやスタブを修正し、バグがトリガーされるか、または偽陽性として排除されるまでループを継続（最大 60 回）。

フェーズ 3: 具体検証 (Concrete Validation)

• 目的: LLM が生成したハネスと記号実行の結果が、修正されていない元のプロジェクトソースで再現可能かを確認し、誤検知を排除する。
• プロセス:
  1. KLEE が生成した具体入力（.ktest ファイル）を用いて、修正されていないプロジェクトを AddressSanitizer (ASan) 付きでコンパイル。
  2. 生成されたドライバを ASan 付きバイナリにリンクして実行。
  3. ASan がメモリ安全性違反（ヒープバッファオーバーフロー等）を報告した場合のみ、「確認済み（Confirmed）」として認定。

---

3. 主要な貢献

1. 完全自動化された脆弱性発見技術: 静的解析でターゲットを特定し、LLM がハネスを合成・改良し、具体実行で検証する、手作業を不要としたパイプラインの提案。
2. Sailor の実装: CodeQL、LLM、KLEE、AddressSanitizer を統合したエンドツーエンドの実装。プロジェクト固有の設定（ビルドスクリプト以外）は不要。
3. 大規模評価と再現性: 10 のオープンソース C/C++ プロジェクト（合計 680 万行）での評価。発見された 379 件の脆弱性すべてに、パス制約、クラッシュ入力、ASan スタックトレース、および必要に応じてファジング用シードを提供。

---

4. 評価結果

10 のプロジェクト（libpng, binutils, FFmpeg, OpenSSL, SQLite など、合計 680 万行）で評価を行いました。

• 発見数: 379 件の固有の既知ではないメモリ安全性脆弱性（421 件の確認済みクラッシュ）を発見。
• ベースラインとの比較:
  • 最も強力なベースライン（全コードベースアクセスと無制限の対話を許可したエージェント型 LLM、B5）は、わずか12 件の脆弱性しか発見できませんでした。
  • Sailor は、他のすべてのベースライン（手動ハネス付き SE、LLM 単独検出など）を大きく上回る性能を示しました（30 倍以上）。
• アブレーション研究（各コンポーネントの重要性）:
  • 静的解析なし: 確認済み脆弱性は 31 件に減少（12.2 倍の低下）。LLM 単独では候補の絞り込みが不可能。
  • 反復改良なし: 確認済み脆弱性は0 件に。LLM の一回きりの生成ではハネスの精度が不足し、コンパイルエラーや経路到達失敗が多発。
  • 記号実行なし: どの手法でも 12 件を超える脆弱性は発見不可能。LLM 単独や静的解析単独では誤検知率が高すぎる。
  • 具体検証: 924 件の SE 検出結果のうち、ASan による具体検証で 379 件に絞り込まれ、誤検知を排除。

---

5. 意義と結論

• スケーラビリティの突破: 手作業でのハネス作成というボトルネックを解消し、数百万行規模のコードベースに対しても記号実行を適用可能にしました。
• 技術の相乗効果: 静的解析の「スケーラビリティ」、LLM の「コード推論能力」、記号実行の「経路精度」、具体実行の「真実性（Ground Truth）」を組み合わせることで、単独では達成できない高い精度と発見能力を実現しました。
• 実用性: 発見された 379 件の脆弱性の多くは OSS-Fuzz などの既存ファジングツールでは再現困難な、複雑な状態依存のバグでした。これにより、深層のライブラリ内部にある脆弱性の発見が可能になりました。

この研究は、LLM を単なるコード生成ツールとしてではなく、静的解析と動的検証を橋渡しする「オーケストレーター」として活用する新しいパラダイムを示しており、大規模ソフトウェアのセキュリティ強化に重要な貢献を果たすものです。