【連載】なにそれ？あなたの知らないテストの言葉（第5回）：コンコリックテスト(Concolic Testing)

このマンガ連載では普段目にすることが少ない「なにそれ」という用語をピックアップして解説します。

第5回は「コンコリックテスト(Concolic Testing)」です。
コンコリックテストはホワイトボックステスト技法の一つで、プログラムの実行可能なパスを効率的に抽出し、そのパスを通るための入力を自動で見つける方法です。

シンボリック実行

コンコリックテストがどのような仕組みであるかを知るためには、基本となる考え方であるシンボリック実行を知る必要があります。
シンボリック実行でどのように実行可能パスを抽出し、入力を見つけていくのかを説明します。
以下のようなプログラムがあったとします。

def check(x, y):
    if x > 0:
        if y == x + 5:
            return “NO”
    return “YES”

シンボリック実行では入力を具体的な値ではなく、値が決まっていない未知の記号「シンボル」として扱います。ここではxという変数を未知のシンボルα、yという変数を未知のシンボルβとします。
最初の条件は `α > 0`です。シンボリック実行ではパス条件のことを制約と呼びます。

　●制約1 : α > 0

`α > 0` を制約1とします。この分岐のもう一方の条件を考えると `α ≦ 0`という制約2が分かります。

　●制約2 : α ≦ 0

制約1の後には `β == α + 5`という条件が現れます。制約1が真(True)の場合に現れるので積み重ねると制約1Aは` (α > 0) ∧ (β == α + 5) `となります。

　●制約1A : (α > 0) ∧ (β == α + 5)

続いて`β == α + 5`の条件のもう一方の条件を考えると `β ≠ α + 5`になります。これも制約1が真(True)の場合のみなので以下の制約になります。

　●制約1B : (α > 0) ∧ (β ≠ α + 5)

全てのパスを通るための制約が以下のように出そろいました。

　●制約1A : (α > 0) ∧ (β == α + 5)

　●制約1B : (α > 0) ∧ (β ≠ α + 5)

　●制約2 : α ≦ 0

これら、それぞれの制約が真(True)になる値を見つければ全ての分岐を通ることができます。
割り当てるべき値はSMTソルバ(Satisfiability Modulo Theories Solver、以下ソルバ)で解くことによって、値を生成することができます。
(※SMTソルバとSATソルバがあるが、SATソルバは命題論理を解くものである。シンボリック実行で出てくる制約は演算などを含むためSMTソルバが必要となる。)

シンボリック実行が難しくなる場合

シンボリック実行は実行パスを見つける強力な手法ですが、現実のソフトウェアに適用しようとすると以下のような問題が発生します。

パス爆発

分岐が増えると制約の数が指数的に増えてしまいます。例えば、10個の分岐があった場合、2^10 = 1024通りになってしまいます。ループを含んでも同様にパスが爆発的に増えてしまいます。

ソルバが解けない数式

ソルバが苦手としている計算もあります。例えば、三角関数や浮動小数点の計算です。また暗号関数も解けない問題です。

外部環境依存の問題

例えば、外部のライブラリを使っていた場合、内部構造が分からないため式を解くことができなくなります。同様にファイル読み込みといったファイルI/Oなど、外部環境に依存する問題も解けません。

コンコリックテスト

そこでコンコリックテストです。
コンコリックテストは具体実行（Concrete Execution）とシンボリック実行（Symbolic Execution）を組み合わせた手法です。

プログラムを実際に具体的な値で実行しながら、その時に通った分岐条件をシンボリックに記録します。その条件をソルバで解いて次に探索すべき別の入力を生成し、また実行する、というサイクルを繰り返します。これによりシンボリック実行だけでは解けない部分も、実際の実行結果で補完することで探索することができます。

以下のプログラムでコンコリックテストの流れを追います。

def check(x, y):
    if x > 0:
        if y == foo(x):
            return "NO"
    return "YES"

foo(x)は外部から呼んでいて分からないとします。
また未知のシンボルに置き換えて考えます。xはα、yはβ、foo(x)は未知の関数F(α)とします。

1回目の実行

まずは適当な入力で実行します。(x=0, y=0)とします。
実行結果は x > 0 が偽(False)となるため、if文の中は実行されず “YES” を返します。

シンボリック実行の側では α ≦ 0 を通ったこととなります。
α ≦ 0 を通ったので、次は条件を反転し α > 0 を通りたいです。よってソルバで α > 0 が真(True)となる入力を生成します。(x=1, y=0)を得たとします。

2回目の実行

(x=1, y=0)を入力として実行します。x > 0は通過することができます。
実行することによってfoo(1)から何が返ってくるかを観測することができます。仮に7が返ってきたとします。
その場合、y==foo(x) の比較は 0と7の比較となるため偽(False)となり、最終結果は”YES”となります。

シンボリック実行の側では β ≠ F(α) という条件を通ったことになります。よって制約は (α > 0) ∧ (β ≠ F(α))を通ったことになります。
次はβ ≠ F(α)を反転して、(α > 0) ∧ (β == F(α))を満たす具体的な入力を作りたいです。
ここで具体実行によってF(1) = 7になることは観測済みです。
そこでF(1)を観測値である7に置き換えるのです。これがコンコリックテストの肝です。
これによりxが1の時、yが7ならば(α > 0) ∧ (β == F(α))を満たすことが分かるのです。

3回目の実行

(x=1, y=7)を入力として実行します。x > 0を通過し、次の y == foo(x)についても、foo(1) = 7のため 7 == 7 で真(True)となります。よって最終結果は”NO”となります。

シンボリック実行側でも無事 (α > 0) ∧ (β == F(α)) を通ったこととなります。

＊＊＊

コンコリックテストは、このように解けない部分は具体実行によって得た観測値を使い、ソルバが解けない問題を回避して進めていく方法です。

どうやってバグを発見するのか

コンコリックテストは実行パスを効率的に探索する方法です。これだけで期待結果と比較するものではありません。アサーションを用意して比較することも可能ですが、特定のメソッドでない限り難しいです。

よってよく行われる方法はクラッシュ監視です。つまりその実行パスを通った時に例外などでクラッシュしないかの監視をすることが多いです。他にもメモリリークなど、特定のプログラムに依存しない一般的に起きたら困ることの発生の有無を確認します。

実際の事例

実際にコンコリックテストがどのように使われているかについて、MicrosoftのSAGEの事例を取り上げます。

https://queue.acm.org/detail.cfm?id=2094081

この記事では、コンコリックテストはWhitebox Fuzzingと記載されています。
Microsoftでは、特にファイルパーサーのバグによるバッファオーバーフローなどのセキュリティバグが深刻でした。そこでファジング（ブラックボックステスト技法。ランダムな入力を与えてバッファオーバーフローが発生しないか確認する）でテストを行っていました。これにより数千ものセキュリティバグは発見されましたが、効率が悪く網羅性に欠けていました。

そこで自社製のSAGEというコンコリックテストツールを用いることにしました。
Windows7の開発中、セキュリティ関連のバグについて、ファイルを入力として用いたテストでは、発見されたバグの1 / 3をSAGEが発見したと報告されています。事例の記事執筆時点(2012年)では、平均100台以上のマシンで24時間365日コンコリックテストが動き、数百ものアプリケーションを自動でコンコリックテストが実行されているそうです。

派生開発の回帰テストへの応用の研究事例

国内でもコンコリックテストの研究事例があります。ソフトウェア・シンポジウム2015では「Concolic Testingを活用した実装ベースの回帰テスト」が報告されました。この研究では、従来の仕様ベース回帰テスト（リグレッションテスト）では膨大な工数が必要になるという課題に対して、実装ベースで制御パスを網羅する入力を自動生成し、期待結果も前バージョンから自動取得する方式を提案しています。これにより、人手によるテストケース設計を不要にし、回帰テストの自動化を実現できることが示されています。