はじめに

選択的シンボリック実行について紹介する.

シンボリック実行

シンボリック実行とは,プログラムに含まれる変数に具体値を入力せず,その代わりとして値を代表するシンボルの操作を通じてプログラムを模擬的に実行し,結果を評価する技術である.シンボリック実行の目的は,コードカバレッジの拡大にある.シンボリック実行は全てのケースに対してforkする,あるいは,条件分岐の制約をもとにテストケースを生成するといった形態でソフトウェアテストに用いられている.
ひとまず,以前書いたシンボリック実行に入門しようとしたをご覧頂きたい.

選択的シンボリック実行

選択的シンボリック実行(selective symbolic execution)は,シンボリック実行の弱点を改善すべくS2Eにて提案,実装された.
シンボリック実行には実行パスにおける計算爆発(path explosion)の問題があった.プログラム中の全ての実行パスを通るための制約はあまりにも多い.そして,全ての実行パスというのは解析対象の実行パスだけではない.考えてもみよう,実システムでプログラムを実行した際,プログラムは自身以外の様々なものを呼び出す.呼び出されるlibcなどのライブラリ,そしてカーネルやデバイスドライバ,さらにそのファームウェアは,一体どこまで解析対象における実行パスの分岐に影響を与えるのか.
この頭が痛い問題に対応するべく編み出されたのが選択的シンボリック実行,すなわちシンボリック実行を行う範囲の限定である.S2Eはシンボリック実行を行いたい部分以外に具体値(concrete value)を用いることで,解析対象のプログラムだけにシンボリック実行を適用する(concolic testing).具体的には,S2Eは指定した変数が使用されている部分のみシンボリック実行を適用している.

S2E

動的バイナリ変換

S2Eは,QEMUをベースに開発された.QEMUはエミュレーションを実現するべく,以下のような流れで動的バイナリ変換を行う.

1.ゲストコードの逆アセンブル
2.マイクロオペレーションに変換
3.コード辞書を参照してホストコードに変換

S2Eはこのコード辞書をLLVM bitcodeに差し替えることで,x86のバイナリをLLVM bitcodeに変換する.そして,変換後のLLVM bitcodeをKLEEに渡すことで,シンボリック実行を行う.
このとき,解析対象の全部分がLLVM bitcodeに変換されるわけではない

指定した変数が使用されている部分のみシンボリック実行を適用すると書いたように,S2Eはシンボル化したデータにアクセスしているか否かによって,解析対象の実行方式を切り替えている.実行方式は以下の二通りだ.

  1. 具体値にアクセスしている場合,通常通り実行
  2. シンボルにアクセスしている場合,LLVM bitcodeに変換してKLEE上で実行

これは,解析対象を多数のコードブロックに分割するというQEMUのバイナリ変換方式に極めて依存している.

S2E opcodes

S2Eは独自の拡張命令S2E opcodesを用いてシンボリック実行のための機能をinstrumentする.S2E opcodesは以下のような機能を提供する.

  • S2SYM: データのシンボル化
  • S2ENA: 複数パスの実行を有効化
  • S2DIS: 複数パスの実行を無効化
  • S2OUT: デバッグ情報の出力

この中身はs2e-x86.hs2e.hに記述されている.例としてS2SYMの実装を見てみよう.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
#define S2E_INSTRUCTION_COMPLEX(val1, val2) \
".byte 0x0F, 0x3F\n" \
".byte 0x00, 0x" #val1 ", 0x" #val2 ", 0x00\n" \
".byte 0x00, 0x00, 0x00, 0x00\n"
#define S2E_INSTRUCTION_SIMPLE(val) \
S2E_INSTRUCTION_COMPLEX(val, 00)
~ 略 ~
static inline void s2e_make_symbolic(void *buf, int size, const char *name)
{
__s2e_touch_string(name);
__s2e_touch_buffer(buf, size);
__asm__ __volatile__(
S2E_INSTRUCTION_SIMPLE(03)
: : "a" (buf), "d" (size), "c" (name) : "memory"
);
}

例えば,解析対象のソースコード上でs2e_make_symbolic()の引数にシンボル化したい変数を渡すことで,この関数を利用することができる.

Windowsデバイスドライバに対する選択的シンボリック実行

Analyzing Windows Drivers: Step-by-Step Tutorialという公式チュートリアルでは,プラグインを用いてWindowsデバイスドライバにアノテーションを付加する方法が紹介されている.

1
2
3
4
5
6
7
8
9
10
11
12
13
function annotation_example(state, plg)
-- Write custom Lua code here (e.g., to inject symbolic values)
end
pluginsConfig.Annotation =
{
init1 = {
active=true,
module="pcntpci5_sys_1",
address=0x169c9,
instructionAnnotation="annotation_example"
}
}

チュートリアルの例ではpcntpci5.sysというドライバが0x169c9というアドレスを呼び出す際にannotation_example()が実行される.BSoDもフックできるので,NotMyFaultドライバで遊ぼう.

オーバーヘッド

いつだって問題となるのは実行速度だ.論文によると,S2Eは具体値による実行時(concrete mode)にQEMUの6倍,シンボリック実行時にQEMUの78倍のオーバーヘッドが生ずるとされている.注意したいのは,実機の78倍ではなくQEMUの78倍である点だ.

おわりに

S2Eについて紹介した.
このエントリはソフトウェアテストあどべんとかれんだー2014の3日目として書かれた.

参考文献

より詳しくは以下の論文を参照されたい.これも全てVitaly Chipounovって奴の仕業なんだ.