コンテンツにスキップ

Mayhem テクノロジー

Mayhem の秘密は、連携してターゲット プログラムをテストする動的解析のポートフォリオです。動的解析は、ターゲット プログラムが実際の入力を処理するのをモニターします。Mayhem の動的解析では、結果を生成するのに使用されたテスト ケースがレポートされた動作の証拠であるため、誤検出がありません。

Mayhem はポートフォリオ解析を行います。これは、相互を補完する複数の動的解析を組み合わせることを意味します。Mayhem の解析は、先端的な学術および産業機関での 20 年以上にわたる研究の成果であり、数多くの特許取得済み技術や評価の高い査読付き学術誌で発表された技術を利用しています。

Mayhem の主要な解析には以下が含まれます。

  1. カバレッジガイド付きのインテリジェントなファジング
  2. シンボリック実行
  3. 各テスト ケースの動的実行時モニタリング
  4. セキュリティ品質指標をチェックする静的解析

このセクションでは、さまざまな解析の概要を説明し、より詳細にトピックを知りたい場合の参照リンクを示します。

ファジングとは

ファジングとは、アプリケーションにさまざまな入力を処理させ、異常な動作がないかをモニターすることによって欠陥を明らかにするプロセスです。ファジングは、さまざまな分野や組織にわたって、ソフトウェアの問題を発見する方法として一般的になっています。

ファジングはネガティブ テスト技術です。つまり、不正確な、あるいは望ましくない (ネガティブな) 動作がないかどうかをテストします。従来のテストは、プログラムが特定の望ましい動作を示しているかを個々のテスト ケースによってチェックするポジティブ テストを重視します。

ファジングは、開発者が手動でテストを実行してコードをテストする従来のテスト フレームワークとはまるで異なります。手動で作成されたテストは、開発者の意図に忠実に従ってコードをテストできる半面、開発者が考え、実装したテストだけが実行されるというデメリットもあります。ファジングは何十万、何百万という入力を生成してプログラムを実行することで、開発者が想像もしなかった、あるいは単に実装する時間がなかった機能やエッジケースをテストします。

一般的なファザーと同様に、Mayhem は 3 つのアルゴリズムで構成されます。

  1. 入力生成: ファザーはプログラムに対する新しい入力を生成します。Mayhem は一連の経験則を使用し、既知の入力から次の入力を生成します。

    Tip

    Mayhem に既存のテスト スイートを指定できます。すると、Mayhem の処理をスピードアップするのに役立ちます。

  2. 呼び出し: ユーザーは、Mayhem にプログラムの実行方法を指示する必要があります。そのために Mayhemfile を使用します。ファザーは生成された入力を使用してプログラムを呼び出します。

    Note

    最良の結果を得るには、ターゲットの各呼び出しが、互いに独立している必要があります。

  3. 通知Mayhem はプログラムがクラッシュしたかどうかをチェックして、特定の入力に問題があるかを判断します。

    Info

    Mayhem は、ファイルベースの入力の場合、1 度に 1 つの入力を検討し、UDP および TCP ネットワーク入力の場合は、独自の高度な経験則を使用します。Mayhem の経験則が、いつ単一の入力が処理されるかを特定できない場合、ユーザーがをハーネスの作成を行う必要がある可能性があります。

カバレッジガイド付きファジング

Mayhem はコード カバレッジの最大化をファジングおよび新規入力生成のゴール関数として使用します。Mayhem は、制御フロー グラフのいくつのエッジが実行されたかを計測するエッジ カバレッジ メトリクスを使用します。

形式的には、カバレッジガイド付きファザーはターゲット プログラム p に対し、入力のワーキング セット S を保持します。 シード セットと呼ばれる初期ワーキング セットは、ユーザーが指定した入力のセットまたは Mayhem が生成したデフォルトのセットです。S の各入力 x ごとに Mayhem ファザーは以下を実行します。

  1. x を使用して p を実行し、プログラムの実行されたブランチおよびステートメントに関する情報を収集します。
  2. ステップ 1 のカバレッジ情報を使用して新規入力 y を生成します。Mayhem がカバレッジガイド付きファザーと呼ばれるのは、入力 x およびカバレッジ情報の両方を使用して新規入力 y を生成するからです。
  3. y を使用して p を実行します。 y が新しい範囲をカバーする場合、Mayhem は y をワーキング セット S に追加します。
  4. カバレッジを最大化するために必要な最小限の入力のセットだけに S を減らします。 このステップでは、S のサイズはできるだけ小さく抑えられます。
  5. S から新しい入力を選択し、ステップ 1 に移動します。

ステップ (4) は、生成されるテスト ケースができるだけ小さく、できるだけすばやく実行できるようにするために重要な最適化です。minimal set を計算するため、S はよく minset とも呼ばれます。

最近の CPU では、ターゲット プログラムに対して 1 秒あたり 100 から 1000 単位のテストを実行できるのが普通です。シンボリック実行 (下で説明します) と比べると、これは非常に高速です。大きな欠点は、ファジングはランダムな、あるいはランダムに近い入力を試すように劣化する場合があり、長期的には非効率的になる可能性がある点です。一般的な目安として、最初の 10 分から 30 分の間は、シンボリック実行よりもファジングのほうが有効であり、その後はシンボリック実行のメリットが大きくなり始めます。

カバレッジ ファジングのサンプル: サンプル プログラムを見てみましょう。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
a = user_input0()
b = user_input1()
if (a < 10) {
  c = 30
}
else {
  if (b = 0xdeadbeef) {
    c = 100
  }
  else {
    c = 0
  }
}

制御フロー グラフ (CFG) の観点からプログラムを検討することがよくあります。CFG とは、単一のプログラム ステートメントをノードとし、制御の遷移が可能なノード間にエッジが存在する有向グラフです。

次の図は CFG のサンプルです。

graph-0.png

この CFG には次の 6 つのブロックがあり、異なる 6 つの場所を表しています: block-0、block-1、block-2、block-3、block-4、block-5

次のステップは、テスト対象プログラムの実行中にどのブロックに到達するかを特定することです。ブロックが実行された場合、そのブロックは「カバー済み」とみなされます。これを判断するには、各ブロックの先頭に特殊な関数を挿入します。ブロックがカバーされるたびにこの関数が実行され、呼び出しているブロックがカバー済みブロックのセットに追加されます。

インストゥルメントされたプログラムは次のとおりです。

graph-1.png

インストゥルメンテーションによって、プログラムの実行中にカバーされたブロックがわかるようになりました。たとえば、プログラムに user_input0() として値 5 を与えると、ブロック block-0、block-1、block-5 がカバーされます。

カバレッジガイド付きファザーは、新しいブロックをカバーする入力を優先します。このサンプル プログラムの場合、user_input0() に 1、2、3、4 から 9 までの入力値を与えると、常にブロック {block-0, block-1, block-5} がカバーされます。ファザーは値 {user_input0 = 0, user_input1 = 0} を入力することから開始し、これらの番号のうちいずれかをランダムに変更することができます。user_input0() に >= 10 となる値が入力されると、新しいブロックがカバーされたことがインストゥルメンテーションによって通知されます。

入力が新しいコードをカバーすると、ファザーは該当入力値をテスト スイート、つまり継続的に変化させる入力値のセットに保存します。ファザーがすでにテストしたのと同じコードを実行する入力は破棄されます。これによって、ファザーはテスト対象プログラムの新しい部分を実行する新しい入力をよりすばやく発見することができます。

シンボリック実行

シンボリック実行とは、プログラムの実行パスを論理的な式に変換する形式手法です。式は、特定のパスをたどるすべての入力値で true になります。次の C プログラムを検討してみます。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
#include <stdio.h>
#include <assert.h>

int main() {
  int input;
  input = getchar();
  printf("%d\n", input);
  if(input > 64) {
     if(input < 91)
        if((input % 2) == 0)
             printf("bug!\n");
  } else {
    printf("safe!\n");
  }
  return 0;
}

プログラムは、整数に変換したとき次の条件を満たす ASCII 文字を入力すると、"bug" と出力します。

  1. 64 より大きい
  2. 91 より小さい
  3. 偶数 (モジュロ 2 がゼロの任意の数は偶数です)

シンボリック実行は、上記の制約を捕捉し、自動的に解決して入力を生成します。

シンボリック実行は、通常の実行時のように各入力値を具体的な数値として表現するのではなく、シンボリックな変数として表現します。たとえば、プログラムに入力値 65 を指定すると、変数 input の値は具体的な数値 65 になり、各分岐が 0 または 1 に評価されます。 いっぽう、シンボリック変数は、("integer" などの型とペアにされた) 単なる変数であり、特定の値を持っていません。

シンボリック実行の仕組みは次のとおりです。

  1. 入力値を使用してプログラムを実行します。 たとえば、ASCII コードでは 65 (10 進数) に相当する入力値 A を使用して上記のプログラムを実行したとします。

  2. 入力値をシンボリック変数 x と表現して実行トレースを記録します。 入力値 "A" の場合、次の式を作成します。

    x > 64 && x < 91 && !((x %2) == 0)

    Note

    式が true になる (これを「式を満たす」と呼びます) x への任意の代入は元の入力値 "A" と同じパスを実行します。

  3. 分岐条件の 1 つを反転させ、解があるかどうかをチェックします。たとえば、シンボリック実行が、x が偶数かどうかをチェックする最後の分岐を反転させた場合 (上記の式の否定 ! を削除したものと同じ)、次のようになります。

    x > 64 && x < 91 && ((x %2) == 0)

    Note

    代入 x = 42 はこの式を満たします。これは、ASCII 文字 B に相当します。そのため、"B" を使用してプログラムを実行すると、バグがトリガーされます。

簡単に言うと、シンボリック実行は、形式論理と数式ソルバーを使用して新しい分岐を探索し、新しいプログラム パスを取る新しい入力値を見つけます。

ファジングとの比較: ファジングは形式技術ではなく、ソルバーを使用しません。たとえば、ランダム変異ファザーがこのバグを見つける確率は 10% しかありません。なぜなら、可能な ASCII 入力値 127 個のうち該当コード行に到達するのは 13 個だけだからです。

別の例として、上記のカバレッジガイド付きファジングセクションのサンプルを検討してみましょう。 すべての整数が 32 ビットの場合、ランダムな入力値が if 条件 b == 0xdeadbeef を満たす確率は 2\^{-32} しかありません。

シンボリック実行のサンプル: このセクションでは、上記のカバレッジガイド付き ファジングのサンプルを使用して、シンボリック実行がどのようにパス式を構築するか を説明します。

まず、block-0 の末尾でシンボリック実行は次の値をトラックできるよう、user_input0() の結果を A に置き換え、user_input1() の結果を B に置き換えます。

graph-2.png

States:
  State-0:
    Location: After block-0
    Variables: {a = A, b = B}
    PathFormula = {}

ブロックがあり、ブロックのシンボリック実行の終わりにシンボリック ステートがあるため、それがブロックに付加されています。このシンボリック実行では、シンボリック実行エンジンが user_input0() に対して A を返し、user_input0() に対して B を返しました。実際のプログラムでは、input_file.txt というファイルからバイト列を読み取る場合、ファイルの各バイトを個別のシンボリック値とし、input_file.txt_0x1、input_file.txt_0x2 等と命名する可能性があります。

block-0 を出ると、条件分岐に遭遇します。1 つのパスは a < 10 によってガードされ、もう 1 つのパスは a >= 10 によってガードされています。シンボリック ステートをコピーまたは「フォーク」して、まったく同じ 2 つのコピーを作成し、パス式に条件を追加します。その後、後続のブロック block-1 および block-2 を実行します。

graph-3.png

States:
  State-0:
    Location: After block-1
    Variables: {a = A, b = B, C = 30}
    PathFormula = {A < 10}
  State-1:
    Location: After block-2
    Variables: {a = A, b = B}
    PathFormula = {A >= 10}

ステートをフォークし、パス式を追加する方法をすでに知っているので、block-2 の後にステートをフォークし、block-3 および block-4 をシンボリックに実行します。

graph-4.png

States:
  State-0:
    Location: After block-1
    Variables: {a = A, b = B, C = 30}
    PathFormula = {A < 10}
  State-1:
    Location: After block-3
    Variables: {a = A, b = B, C = 0}
    PathFormula = {A >= 10 AND B != 0xdeadbeef}
  State-2:
    Location: After block-4
    Variables: {a = A, b = B, C = 100}
    PathFormula = {A >= 10 AND B == 0xdeadbeef}

最後に、関数の終わりまですべてのシンボリック ステートを実行していきます。

graph-0.png

States:
  State-0:
    Location: After block-5
    Variables: {a = A, b = B, C = 30}
    PathFormula = {A < 10}
  State-1:
    Location: After block-5
    Variables: {a = A, b = B, C = 0}
    PathFormula = {A >= 10 AND B != 0xdeadbeef}
  State-2:
    Location: After block-5
    Variables: {a = A, b = B, C = 100}
    PathFormula = {A >= 10 AND B == 0xdeadbeef}

3 つのステートと、3 つの異なるパス式のセットが残りました。

  • A < 10
  • A >= 10 AND B != 0xdeadbeef
  • A >= 10 AND B == 0xdeadbeef

これら 3 つのパス式は、このプログラムのすべてのパスを網羅するためにどのような入力値が必要かをもれなく記述しています。

その後、式を解いて、式が true となる特定の変数値を見つけます。Mayhem は SMT (Satisfiability Modulo Theory) ソルバーを使用します。これは、マシンレベルの数値表現に関する推論を行うことができます。式が与えられると、SMT は次のいずれかを返します。

  • SAT および各変数のサンプル値。式の構築において、各値はプログラムへの入力です。
  • 式を満たす答えが存在しないことを表す UNSAT。たとえば、式 A and NOT A は unsatisfiable です。
  • 未完了。 SMT は少なくとも NP 困難であり、タイムアウト時間内に終了しない可能性があります。

サンプル実行では、次の 3 つのサンプル SAT 解があります。

  • A < 10 -> {A = 5}
  • A >= 10 AND B != 0xdeadbeef -> {A = 20, B = 0}
  • A >= 10 AND B == 0xdeadbeef -> {A = 15, B = 0xdeadbeef}

このサンプルでは、シンボリック実行はランダム ファジングよりも少ないステップで B = 0xdeadbeef を発見することができました。

ファジングとシンボリック実行を組み合わせる

Mayhem はベストオブブリードのカバレッジガイド付きファジングと高度なシンボリック実行を組み合わせて、より多くのコードを実行し、より高速にバグを見つける入力値をすばやく発見します。これを実現するため、Mayhem はファザーとシンボリック エグゼキューター間で入力値を共有します。

シンボリック エグゼキューターがファザーから入力を受け取ると、特定のポイントまでは入力値によって記述されるのと同じパスをたどり、その後、シンボリック実行を使用してフォークを行い、ファザーでは推論が困難だったエッジを網羅する新しい入力値を発見します。同様に、ファザーはシンボリック実行から入力値を受け取ってすばやく変更し、プログラムをテストして到達が容易な新しいブロックを探索します。