記号実行とコンコリックテスト

testing 記号実行 コンコリックテスト

記号実行（Symbolic Execution）とコンコリックテスト（Concolic Testing）は、プログラムの特定の箇所を通るような入力値を生成する手法であり、ソフトウェアテストに関する研究においてよく登場する。元々なんとなく理解していたつもりだが、もう少しちゃんと調べてまとめてみる。本記事では、まずは記号実行とコンコリックテストを説明し、それぞれの長所・短所を整理する。

これらの解説をググると「コンコリックテスト」と同じような意味で「コンコリック実行」という言葉が見られる。Wikipedia では Concolic Testing のページのみが存在しているので、本記事では「コンコリックテスト」という言葉を使うことにした。意味的に考えても、Concolic Testing は、対象のプログラムの実行と、プログラムに対する symbolic なインタプリタの実行を組み合わせているだけなので、「コンコリック実行」という実行をしているわけではないないよなぁ。専門家がどのくらい「コンコリック実行」という言葉を日常的に使うのかは知らないが。

背景

記号実行とコンコリックテストは、プログラムの「特定の箇所」を通るような入力値を生成する手法である。ソフトウェアテストの文脈では「特定の箇所」を「まだ通過していない箇所」として、そこを通る入力値を生成することで、たとえばカバレッジを向上するような入力値を生成できる。

ここで注意すべきは、よさそうな入力値を生成したからといって、あるべき出力値が分からないのであればテストとして成立しないということである。プログラムのあるべきふるまいは test oracle と呼ばれ、test oracle がテスト時に必ずしも分からない問題は test oracle problem と呼ばれている。一方で、ある値を入力したときに、プログラムがエラーを起こしてクラッシュするような場合はおそらく望ましい動作ではない。たとえば、組み込みシステムがメモリリークを起こす場合や、スマホアプリがエラーで落ちる場合などである。test oracle について詳しくは Wikipedia のページ を参照のこと。

記号実行やコンコリックテストは、このような暗黙的（implicit）な test oracle に違反する入力値を発見する手法である。 新たな入力値を生成し続けることで徐々にカバレッジを高めていき、その中でエラーを起こすような入力値が見つかればラッキーという感じである。

記号実行（Symbolic Execution）

記号実行の目的が分かったところで手法を具体的に説明する。前提として、記号実行は静的解析の手法であり、プログラムを実際に実行することなく具体的な入力値を生成する。

以下のソースコードを考えてみる。

1  void bar(int x, int y) {
2    z = 2 * y;
3    if (z == x) {
4      if (x > y+10) {
5        ERROR;
6      }
7    }
8  }

ソースコードの引用元：https://www.cs.cmu.edu/~aldrich/courses/17-355-19sp/notes/notes15-concolic-testing.pdf

このプログラムでは5行目でエラーを起こすため、ここを通るような入力値を生成できると嬉しい。入力値 x, yが与えられ、2行目で変数 y の値が2倍され、3, 4行目で条件式 z == x や x > y+10 によって分岐が行われる。5行目に到達するにはこれらの条件式を真にする必要があるが、その時に必要な入力値 x, y は何か？というのが解きたい問題である。

人間がじっくり考えれば5行目に到達する入力値を求められそうだが、コンピュータで機械的に計算するにはどうすればよいか？ここで登場するのが SMT ソルバーである。SMT ソルバーはざっくり言うと、論理式が満たせるかどうか判定し、満たす場合はその具体的な値を返すものである。今回のプログラムの例では、入力変数 x, y の具体的な入力値をそれぞれ x_0, y_0 とすると、5行目に到達するには ｚ= 2 \ast y_0 \wedge z = x_0 \wedge x_0 > y_0 + 10 という条件を満たす x_0, y_0 が存在するかどうかを SMT ソルバーで解けばよい。その結果、SMT ソルバーがたとえば x_0 = 30, y_0 = 15 という値を返すため、5行目に到達する具体的な入力値として x = 30, y = 15 という値を求めることができる。

ただし記号実行にはよく知られた課題がいくつかある。その一つとして、プログラム中の命令が SMT ソルバーの論理式として表現できないとき、適切な入力値を求められないことが挙げられる。たとえば、一般的な SMT ソルバーは値を足したり掛けたりする線形な演算をサポートしているものの、余りの計算や浮動小数点数の計算など非線形な演算はサポートしていない。そのため、目標とする箇所に至るまでにこれらの非線形な演算が含まれている場合、記号実行は役に立たない。

具体的には、以下のソースコードの場合は記号実行が上手く機能しない。

1  void bar(int x, int y) {
2    z = y * y % 50;
3    if (z == x) {
4      if (x > y+10) {
5        ERROR;
6      }
7    }
8  }

ほとんど先ほどのプログラムを同じであるが、2行目に非線形な演算（余りの計算）が含まれている。そのため、5行目に到達するための制約を SMT ソルバーで解ける論理式として表現できず、記号実行によって入力値を求めることができない。

プログラムでは表現できるが SMT ソルバーの制約としては表現できない。それなら、SMT ソルバーの制約として表現できない部分を、実際にプログラムを実行した結果で置き換えられないか？こんな発想から生まれたのがコンコリックテストである。

プログラムを読み込んで SMT ソルバーに与える論理式を作る処理はある種のインタプリタであるといえる。具体的には、プログラムの命令列を first-order logic の式として解釈するようなものである。プログラムと SMT が表現できる意味空間にミスマッチがあるため、記号実行が有効に働かない場合があるという状況である。

コンコリックテスト（Concolic Testing）

コンコリックテストは記号実行と動的解析を組み合わせた手法であり、プログラムを実際に実行しそのログを記録する必要がある。コンコリックテストの流れは以下である。（Wikipedia のページ より抜粋）

  1. 適当な入力値のもとでプログラムを実行し、その実行ログを記録する。
  2. 実行された経路に対して記号実行を行い、制約を論理式として構築する。論理式はプログラムの各命令と分岐条件を制約として表現したものである。
  3. 新たな分岐を通る入力値を求めるため、前手順で構築した論理式のうち分岐条件に対応するものを1つ選び、それを否定形で置換する。
  4. 構築した論理式を SMT ソルバーによって解き、新たな入力値を得る。この入力値が手順 1. とは異なる分岐を通過するものとなっている。新たな入力値が得られなければアルゴリズムを停止する。
  5. 新たな入力値のもとで手順1.へ戻る。

要するに、実際にプログラムを実行してみると入力値に対してどの経路が実行されるかを知ることができ、その情報からまだ通っていない分岐を通るような入力値を作り出す手法と言えそう。

コンコリックテストの具体的な実行過程を例を用いて説明する。
ここで記号実行が有効でないソースコードを再掲する。

1  void bar(int x, int y) {
2    z = y * y % 50;
3    if (z == x) {
4      if (x > y+10) {
5        ERROR;
6      }
7    }
8  }

まず、このプログラムにランダムな入力値を与えて実行し、どこを通るか観測する。たとえば、x = 22, y = 7 という入力値を生成して実行する。このとき、3行目の時点で z = 49, x = 22 となり条件式 z == x が偽になるため、エラーを起こす5行目には到達しない。ここで実際に通った経路に対して記号実行を行う。3行目が偽になるので z = y_0 \ast y_0 \% 50 \wedge z \neq x_0 という論理式が真になっているはずである。新たな分岐を通る入力値を生成するには、最後の条件式 z \neq x の否定が真になるような制約式を考えればよい。つまり、 z = y_0 \ast y_0 \% 50 \wedge z = x_0 を満たす入力値を求めたい。しかし、非線形な演算（%）が含まれているのでこのままでは SMT ソルバーで解けない。ここで、入力値が y = 7 のとき３行目の時点で z = 49 となっていたことを利用すると、代わりに z = 49 \wedge z = x_0 を満たす x_0 を求めればよいことが分かる。この解として x_0 = 49 が求まり、x = 49, y = 7 という5行目のエラーを引き起こす入力値を求めることができる。

疑問点メモ：一般に、どのようなケースでコンコリックテストが有効に働くのか理解できていない。この例では入力変数として x と y の2つが存在していて、分岐条件 z == x の左辺 z は入力変数 y のみから決定され、右辺 x は入力変数 x のみから決定される。このように分岐条件が入力変数ごとに独立に決定される場合でコンコリックテストが有効に働くことは理解した。一方で、2行目が z = y * x % 50 であった場合は分岐条件 z == x の左辺 z は入力変数 x, y の両方によって決定される。そのため、実行時の zの値が具体的に分かったとしても z == x を真にする x の値を求めることは難しい（x の値を動かすと z の値が非線形に動いてしまうため）。入力変数が n 個存在する状況で、m コを具体的な値で固定したとき、残りの n-m コの取るべき値を線形的な制約から決定できるときにコンコリックテストが有効って感じ？

記号実行とコンコリックテストの比較

まず分かりやすい大きな違いは、記号実行は静的解析であり、コンコリックテストは動的解析の手法であることである。そのため、コンコリックテストの方が実行にコストがかかるし、そもそも実行ログを記録できない場合は使えない。

一方で、コンコリックテストの方が記号実行よりカバーできるプログラムの範囲が広い。具体的には、記号実行では対応できないが、コンコリックテストでは対応できる可能性のあるケースとして、以下のようものがある。
これは自分の理解に基づいたものであり、間違っているかもしれないので要注意。

  • 非線形な演算や外部ライブラリの実行など、記号実行における制約式としてそもそも表現できないようなケース。コンコリックテストでは、記号実行できない演算をその具体的な実行結果で置換できる可能性があり、分岐条件を反転するような入力値を求めることができる可能性がある。
  • 記号実行において SMT ソルバーの計算があまりに重いため具体的な入力値が1つも求められないようなケース。プログラムの複雑さによっては SMT ソルバーの計算が効率的に解けない状況が生まれるのは自然である。コンコリックテストでは、それらの実行の結果を具体的な値で置換することで、SMT ソルバーで解けるようになる可能性がある。

所感

  • コンコリックテストは、記号実行で構築する論理式のうち SMT ソルバーで扱えない要素を、実際のプログラムの実行結果で置き換えることで、対応できる範囲を拡張するものであると理解した。論理式のうち SMT ソルバーが解釈できない部分はプログラム側で実行してあげて、SMT ソルバーが解釈できる形に置換して渡してあげるのがコンコリックテストの本質といえそう。解析対象のプログラムの意味を正確に再現できる最強のソルバーが存在する世界であればコンコリックテストは不要になるのかと思った。
  • ググっていろいろ調べたが、記号実行で解けるプログラムの例を出してコンコリックテストの説明をしているものが多い。手法を説明するときは、その手法でしか解けないものを running example として例示してほしい。
  • 本記事の途中でも書いたが、コンコリックテストが一般にどういう状況で有効に働くのか理解できていない。記号実行できない演算の出力を決定するために一部の入力変数の値を固定することで、残りの入力変数に対する制約を得て、それが SMT ソルバーで解ける場合はラッキー、という状況のはず。もし記号実行できない演算の出力がすべての入力値に依存するのであればコンコリックテストでも解けない、という理解であってるか？

たとえば、もっともシンプルな例として以下を考える。

1  void bar(int x) {
2    z = foo(x);
3    if (z == 10) {
4      ERROR;
5    }
6  }

記号実行できない演算 foo(x) があり、その出力が唯一の入力変数 x によって決定される。たとえば入力値として x = 3 を与えたとき z = 7 になったとして、意味のある制約式を SMT ソルバーに渡すことはできないはず。どんなときに foo(x) の出力が 10 になるのかを求めるのが本質的に難しいのだから。
一方で、以下のケースでは演算 foo() の結果は入力変数 x に依存しないので、コンコリックテストで意味のある入力値を見つけられる。foo() の具体的な値を入力変数 x に設定してやればよい。

1  void bar(int x) {
2    z = foo();
3    if (z == x) {
4      ERROR;
5    }
6  }

この違いをちゃんと説明した文献とかないかなぁ。

参考文献

Symbolic execution - Wikipedia

Concolic testing - Wikipedia

https://www.cs.cmu.edu/~aldrich/courses/17-355-19sp/notes/notes15-concolic-testing.pdf

[1610.00502] A Survey of Symbolic Execution Techniques