技術要約：インタープロシージャル制御フローパスの実現可能性分析に向けた記号実行の強化

問題定義

静的解析はソフトウェアのセキュリティと信頼性におけるスケーラブルな手法であるが、しばしば高い偽陽性（誤検知）率に悩まされる。これらの偽陽性は、インタープロシージャル制御フローグラフ（ICFG）における制御フローパスが、セマンティクス上の制約（例：変数の値の矛盾）により実行時には理論上は可能であっても実際には実行不可能である場合に発生する。プログラムのICFGにおける特定のパスが実行可能かどうかを判定することは、**パス実現可能性分析（path feasibility analysis）**として知られている。

**記号実行（symbolic execution）**は、記号値を用いてパスを探索し、SMTソルバを利用することでパスの実現可能性を検証する強力な手法であるが、この特定の問題に適用する場合、主に2つの課題に直面する：

1. リソース需要とパス爆発： 標準的な記号実行は、到達可能なすべてのパスを探索しようとするため、特にループや複雑な分岐が存在する場合、指数関数的な状態増大を招く。
2. 自動化のギャップ： 既存のエンジンは、未知の値を持つ変数（例：未初期化メモリ、外部関数の戻り値、ポインタ引数）を扱うために手動の設定を必要とすることが多く、これが静的解析ツールとの完全な自動統合を妨げている。

手法

著者らは、定義された一連のICFGPパスの実現可能性を検証するために特別に設計された、**指向的記号実行（directed symbolic execution）**手法を提案する。すべての到達可能なパスを探索する従来の記号実行とは異なり、このアプローチは実行をターゲットパスへと厳密に誘導し、無関係な分岐の探索を排除する。

この手法は、以下の4つのコア技術コンポーネントに基づいている。

1. 指向的実行とプルーニング（枝刈り）

アルゴリズムは、許可された基本ブロックの集合（$S_{allowed}$）と、必須のマイルストーンの集合（$S_{req}$）を入力として受け取る。実行中：

• プルーニング： 分岐点において、$S_{allowed}$ に属さない後続の基本ブロックはすべてプルーニングされ、エンジンが無関係なコード領域を探索することを防ぐ。
• 検証： パスは、ターゲットブロック（$B_{target}$）に到達し、かつ $S_{req}$ 内のすべてのブロックを訪問し、かつ $S_{allowed}$ 内に留まり続けた場合にのみ、実現可能であるとみなされる。

2. 自動化された記号化戦略

ユーザーの介入なしに完全な自動解析を可能にするため、著者らは、標準的な実行では未知または具体的（concrete）となる値を記号化するための戦略を導入している。

• エントリポイントのパラメータ： パス解析を開始する関数のすべてのパラメータを記号化する。
• 未初期化変数とメモリ： 未初期化のローカル変数および動的に割り当てられたメモリ（例：mallocによるもの）は、未定義動作や具体的な初期化を引き起こすのではなく、制約のない値を持つ記号オブジェクトとして扱われる。
• 外部関数：
  • 戻り値： 内部の実体が存在しない外部関数の戻り値を記号化する。
  • ポインタ引数： 外部コールの非定数ポインタ引数が参照するメモリ位置を再記号化し、副作用を考慮する。
  • 特殊なグローバル変数： errno（外部コール後に記号化される）および environ（文字列比較中の非停止を防ぐため、固定長の固定された記号変数のセットとしてモデル化される）に対して特別な処理を行う。
• 関数ポインタと仮想関数： 仮想テーブルと関数シグネチャを分析することで、関数ポインタや仮想コールの潜在的なターゲットを解決し、すべての有効な候補に対して記号状態をフォーク（分岐）させる。

3. 柔軟なメモリモデル

本論文では、固定サイズの配列割り当てに依存しない、記号ポインタをサポートするメモリモデルを導入している。

• 遅延割り当て（Lazy Allocation）： 記号ポインタがデリファレンス（参照）されるまで、メモリオブジェクトは作成されない。
• エイリアシングの処理： 記号ポインタがデリファレンスされる際、エンジンはエイリアシングのシナリオを検討する。エンジンは、ポインタが既存のメモリオブジェクト（一致または異なるオフセットを持つ）を参照する場合と、完全に新しいメモリ位置を参照する場合の両方を探索するために、記号状態をフォークさせる。これにより、サイズを事前定義することなく、連結リストや木構造などの複雑なデータ構造の解析が可能になる。

4. ループ境界戦略

ループにおけるパス爆発を軽減するため、本手法は**ループ境界戦略（loop-bounding strategy）**を採用している。

• 最大反復回数（$C_{max}$）が定義される。
• 記号状態がループ内に $C_{max}$ 回以上進入した場合、エンジンは利用可能な脱出エッジを介して強制的にループを脱出させる。
• 重要な点として、ループ実行中に書き込まれたメモリ位置は、強制脱出前に記号化される。これにより、たとえ正確な反復回数が切り詰められたとしても、ループの副作用に依存するパスをエンジンが依然として探索できることが保証される。これは、完全性とスケーラビリティの間のトレードオフを導入するものであり、ターゲットとなる欠陥箇所の到達可能性を優先するものである。

主な貢献

本論文は、以下の貢献を主張している。

1. 指定された集合内の任意のICFGPパスの実現可能性を判定するための、指向的記号実行アルゴリズム。
2. 未知の値を持つ変数、外部関数の戻り値、およびポインタ引数のための、完全自動化された記号化戦略。
3. 固定サイズの制約なしに記号ポインタの推論とエイリアシングをサポートするメモリモデル。
4. 記号実行を終了させることなく、反復回数を制限するループ境界アルゴリズム。
5. 実世界のソフトウェアおよびJulietテストスイートを用いた実証的評価。

実験結果

本手法は KLEE 記号実行エンジン（v3.1）の拡張として実装され、以下のデータセットを用いて評価された。

1. 実世界のパス検証（GNU Coreutils）

• データセット： 22から1,218の基本ブロックに及ぶ、GNU Coreutilsから抽出された234個の一意なICFGPパス。
• 結果： 本ツールは 95.3% の再現率（recall） を達成し、234パス中223パスの検証に成功した。
• 考察： 49個のパスにおいてループ境界戦略が必要となった。研究では、深さ優先探索（DFS）が時間制限内にターゲット状態に到達できなかった複雑なループのシナリオにおいて、幅優先探索（BFS）戦略が時として必要になることが指摘された。

2. MLH静的解析器との統合

• セットアップ： 本手法をMLH静的解析ツールに統合し、Juliet Test Suite（CWE-401: メモリリーク）を用いてテストした。
• 結果： 統合により、手法は（真陽性を破棄することなく）適合率（precision）を56%から100%に向上させつつ、100%の再現率を維持した。本手法は、すべての偽陽性を排除することに成功した。

3. KLEEFとの比較

• セットアップ： 本手法を、Juliet Test Suite（CWE-415およびCWE-416）における Infer と Clang Static Analyzer (CSA) のレポートを用いて、KLEEF（特化したKLEE派生版）と比較した。
• 結果：
  • Infer： KLEEFはF1スコアを1.0から0.0に低下させた（60件のレポートでクラッシュし、すべての真陽性を実現不可能と分類した）。提案手法はF1スコア1.0を維持した。
  • CSA： KLEEFはF1スコアを0.766から0.058に低下させた。提案手法はF1スコア0.767を維持した（一部の偽陽性をフィルタリングすることで適合率をわずかに向上させつつ、再現率100%を維持した）。
• 分析： 著者らは、KLEEFの失敗の原因を、特定の外部関数呼び出しや記号ポインタ演算を処理できないことにあり、それが早期終了を招いたためであるとしている。

重要性と主張

本論文は、本研究を、静的解析のスケーラビリティと記号実行の精度の間の溝を埋めるための実用的な解決策として位置づけている。著者らは、記号実行を指向させ、記号化を自動化することにより、本手法が静的解析器が報告する実現不可能なパスを効果的にフィルタリングできると主張している。

その重要性は、以下の点にある：

• 記号変数の手動設定なしに、検証プロセスを自動化できること。
• 他のツールが失敗したり固定サイズの近似を必要としたりすることが多い、複雑なメモリモデル（ポインタ、動的割り当て）を扱うことができること。
• 静的解析の指標を改善すること：具体的には、本手法は、真の脆弱性の検出（再現率の維持）を犠牲にすることなく、偽陽性を排除（適合率の向上）できることを示している。

著者らは、ループ境界戦略による完全性とスケーラビリティの間のトレードオフを認めているが、静的解析のレポートを検証するという特定の目的においては、ターゲットとなる箇所の到達可能性を優先することは許容可能な妥協であると主張している。今後の課題として、効率をさらに向上させるための解析の並列化および専門化された状態選択戦略の開発が提案されている。