← DARPA STAC
第 4.4–5 節

対象を絞った動的解析とチャレンジアプリケーション

RULER:ソフトウェア内のリソース使用の脆弱性を検出するシステム

目次

4.4 エクスプロイトを生成するための対象を絞った動的解析

我々は、静的解析と動的解析を組み合わせて、大規模な Java ソフトウェアを分析するための効率的でスケーラブルな手法を実現する Mockingbird フレームワーク [2] を開発した。このフレームワークは、既存の静的解析ツールと動的解析ツール、そしてその統合を可能にする、新たに開発した Object Mocker というコンポーネントを革新的に統合したものである。静的解析器は、大規模なソフトウェアから脆弱である可能性のある部分を抽出するのに使われる。対象を絞った動的解析は、脆弱である可能性のある部分だけを分析し、その脆弱性が実際にエクスプロイト可能かどうかを確認するのに使われる。

Mockingbird フレームワークには次のものが組み込まれている。

  • Atlas プラットフォームを用いて構築された多数の静的解析器。これらの解析器は、関連するコード、すなわち脆弱である可能性のあるコードを抽出するのに使われる。
  • AFL ファザーと、それを補う Kelinci。Kelinci は、AFL が Java プログラムを対象に動作できるようにするインターフェースとなるツールである。
  • Object Mocker。静的解析器を用いて抽出した関連するコードを、AFL ファザーを適用して動的に分析するためのハーネスを自動的に作成できる。

Mockingbird の主な新規性は、対象を絞った動的解析(TDA)である。TDA は、バイナリ入力を用いて、関連するコードだけの動的解析を行う。このフレームワークは、任意の Java のオブジェクト型をモックする機能を提供し、バイナリ入力を適切なオブジェクト型に変換するテストハーネスを生成する。AFL のようなファザーでは、ユーザーは、ファザーからのバイナリ入力を対象プログラムが期待するデータ構造に変換するテストハーネスを手作業で作成する。関連するコードだけを対象にハーネスを手作業で開発するのは、プログラムの状態を入力として考慮しなければならないため、困難で手間がかかる。プログラムの状態は、関数のパラメータと戻り値を用いてスタックメモリを介して、またはグローバル変数の読み書きを用いてヒープメモリを介して、関連する関数に伝えられる。ハーネスには、入力を関連するコードへ運ぶプログラムの成果物を模倣する、モック化されたオブジェクトが組み込まれる。Mockingbird フレームワークは、ハーネスを自動的に作成する。このフレームワークの名前は、テストのコミュニティで使われる「モックオブジェクト」という用語に由来する。

Mockingbird フレームワークでは、必要に応じて、カプセル化されたプログラムのデータを格納するオブジェクトのフィールドの値に制約を課すことができる。この拡張により、自動生成されるテストハーネスにドメイン固有の知識を体系的に組み込むことが可能になる。たとえば、プログラムが、JPEG ファイル形式の場合の 0xFFD8 のようなマジックシーケンスで始まるバイト配列だけを処理する場合、テストハーネスはプログラムの入力の先頭に既知のシーケンスを付けるだけで、プログラムの実行を意味のある方向へすばやく進められる可能性を高められる。Mockingbird フレームワークは、ドメイン知識を注入する手段として、テストハーネスに対して設定可能な入力生成の制約を指定することをサポートしている。

例:我々は、BraidIt という DARPA STAC のチャレンジアプリケーションについて、AC 脆弱性を調べる。このアプリケーションのソースコードは、次のサイトで入手できる:https://github.com/Apogee-Research/STAC。このケーススタディは、(1) Mockingbird フレームワークを用いてアルゴリズム計算量の脆弱性を効率的に発見すること、(2) Mockingbird の API を用いて、脆弱性を全体的に理解するためのプログラムの不変条件を計算するカスタムツールを作成する追加実験を示す。この追加実験により、脆弱性を引き起こす 1 つの入力だけでなく入力のクラスが明らかになり、特に、脆弱性を引き起こしうる最小の入力が明らかになる。

5. チャレンジアプリケーションの分析

分析者は、アルゴリズム計算量(AC)またはサイドチャネル(SC)の脆弱性の各種類(AC Time、AC Space、SC Time、SC Space)を見つけるために、ワークフローにおいて一定のパターンに従うことが観察された。これらのパターンを抽出し、分析者のワークフローを文書化した。大半のチャレンジの問いに対して取った手順は次のとおりである。

5.1 AC Time

  1. ダッシュボード(Entry points)を用いて、アプリのエントリポイントを見つける。
  2. 簡潔なグラフを得るための PCG ツールボックスの助けを借りながら、データフロー/テイント解析のツールボックスを用いて、アプリのエントリポイントと対応するリクエストハンドラの対応を見つける。
  3. データフロー/テイント解析のツールボックスを用いて、攻撃者が利用できる、ユーザー入力で制御されるリクエストを見つける。
  4. ループカタログ、Loop Hierarchy の Smart View、データフロー/テイント解析のツールボックスを用いて、ユーザー入力で制御されるリクエストから到達可能な、ユーザー入力で制御されるループを見つける。
  5. 型とコールサイトのカタログとループカタログを用いて、再帰的なデータ構造を膨張させうる、ユーザー入力で制御されるループを見つける。
  6. ループカタログ、Loop Hierarchy の Smart View、データフロー/テイント解析のツールボックスを用いて、ドメイン知識、ネストの深さ、再帰、終了条件の複雑さ、Java のサブシステムとの相互作用に基づいて、ループの監査の優先順位を付ける。
  7. 動的解析によって、AC Time の存在を検証する。

5.2 AC Space

  1. 型/コールサイトのカタログと Subsystem Interaction View を用いて、チャレンジの問いに基づいて、関心のある特定の操作または型を見つける。
  2. ダッシュボード(Entry points)を用いて、アプリのエントリポイントを見つける。
  3. データフロー/テイント解析のツールボックスを用いて、「関心のある操作または型は、エントリポイントから到達可能か(すなわち、ユーザー入力で制御されるか)」に答える。
  4. ループカタログを用いて、「これらの関心のある操作または型は、ユーザーが制御するループまたは注目すべき分岐に支配されているか」に答える。
  5. データフロー/テイント解析を用いて、「関心のある操作または型によって何が消費されているか」に答える。
  6. データフロー/テイント解析を用いて、「消費されているものはユーザーが制御しているか。それらは膨張させられるか、またはループ内で発生するか」に答える。
  7. IPCG とコールグラフを用いて、消費されることになるユーザーが制御するオブジェクトへ至る、手続き間の関係と呼び出し構造を理解する。
  8. 動的解析を用いて、空間の膨張を動的に引き起こして予算を超えられるかどうかを検証する。

5.3 SC Time

  1. 秘密情報に対応するオブジェクトを見つける。
  2. ダッシュボードを用いて、アプリのエントリポイントを見つける。
  3. PCG の助けを借りながら、データフロー/テイント解析を用いて、エントリポイントと対応するリクエストハンドラの対応を見つける。
  4. PCG の助けを借りながら、データフロー/テイント解析を用いて、リクエストと可能なレスポンスの対応を見つける。
  5. リクエストからレスポンスへの各対応について、PCG の助けを借りながら、ループ/分岐カタログと型とコールサイトのビューを用いて、ユーザーが制御するループ/再帰、負荷の高い操作、または処理されない例外の送出があるかどうかを見つける。
  6. 秘密情報の露見への影響/関係に基づいて、リクエスト/レスポンスの対応の監査の優先順位を付ける。
  7. 動的解析を用いて、秘密情報を明らかにするような時間の差が観測できるかどうかを確認する。

5.4 SC Space

  1. データフロー/テイント解析を用いて、秘密情報に対応するオブジェクトを見つける。
  2. ダッシュボードを用いて、アプリのエントリポイントを見つける。
  3. PCG とあわせてデータフロー/テイント解析を用いて、リクエストとリクエストハンドラの対応を見つける。
  4. 型とコールサイトのカタログとあわせて Subsystem Interaction View を用いて、アプリの出力箇所を見つける。
  5. データフロー/テイント解析を用いて、出力箇所がユーザー入力で制御され、秘密情報と関係があるかどうかを判断する。
  6. 攻撃者が、これらの出力で制御されるオブジェクトを膨張させる入力を与えられる方法として、どのようなものがありうるかを調べる。
  7. IPCG とシステム依存グラフのビューとあわせてループカタログを用いて、ユーザー入力で制御される出力箇所が、ループと差を生む条件に支配されているかどうかを判断する。
  8. 動的解析を用いて、秘密情報を明らかにするような空間の差が観測できるかどうかを確認する。