はじめに

ここでは,BitBlazeのうち,静的解析に特化したコンポーネントであるVineを動かしてみる.

BitBlaze

BitBlazeはDawn Songらによるバイナリ解析プラットフォームで,2008年にBitBlaze: A New Approach to Computer Security via Binary Analysis [PDF]が発表されて以来,数多くの研究に用いられてきた.BitBlazeは,動的解析コンポーネントのTEMU,静的解析コンポーネントのVine,動的シンボリック実行コンポーネントのRudderから構成される.このうち,TEMUとVineのソースコードが公開されている.

TEMU: The BitBlaze Dynamic Analysis Component

TEMUはQEMUをベースとしたエミュレータで,テイント解析(taint analysis)の機能を備えている.テイント解析とは,タグを設定したデータの伝搬を追跡することで,データ同士の依存関係を解析する技術である.TEMUはtracecapというプラグインを用いて,ゲストOS上で動作するアプリケーションのトレースログを取得することができる.

Vine: The BitBlaze Static Analysis Component

Vineは,逆アセンブリやTEMUのトレースファイルから,中間表現VineILや最弱事前条件,STP formulaなどを出力する.公開されているVineには,TEMU/tracecapのトレースファイルとしてfive.traceが同梱されている.これを例にVineの機能を見てみよう.

Vineのインストール

Vine installation and user manualの通り.OCamlで記述されているため,関連のパッケージを導入する必要がある.また,32bit環境での動作を前提としている.

1
2
3
4
sudo apt-get install g++ ocaml ocaml-findlib libgdome2-ocaml-dev camlidl \
libextlib-ocaml-dev ocaml-native-compilers \
libocamlgraph-ocaml-dev binutils-dev texlive \
texlive-latex-extra transfig hevea

trace_reader

TEMU/tracecapが出力するトレースファイルはhuman-readableではなく,閲覧はVineのtrace_readerを介して行う必要がある.five.traceでは,T1がタグの識別子となっており,T0はデータに設定されたタグが存在しないことを意味する.なお,ここではキーボードからの入力にタグが設定されている.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
../trace_utils/trace_reader -trace five.trace | grep T1 | head -n 20
42075911: movzbl (%eax),%eax R@eax[0x40014000][4] T0 M@0x40014000[0x00000035][1] T1 {1 (1001, 0) ()()()}
42077e0c: cmp $0xffffffff,%eax I@0x00000000[0xffffffff][1] T0 R@eax[0x00000035][4] T1 {1 (1001, 0) ()()()}
42077e14: movzbl (%edx),%eax R@eax[0x00000035][4] T1 {1 (1001, 0) ()()()} M@0x40014000[0x00000035][1] T1 {1 (1001, 0) ()()()}
4205abc5: mov %eax,-0xac(%ebp) R@eax[0x00000035][4] T1 {1 (1001, 0) ()()()} M@0xbffff69c[0x00000000][4] T0
4205abce: mov -0xa8(%ebp),%eax R@eax[0x00000035][4] T1 {1 (1001, 0) ()()()} M@0xbffff6a0[0x00000000][4] T0
4205abd5: cmpl $0xffffffff,-0xac(%ebp) I@0x00000000[0xffffffff][1] T0 M@0xbffff69c[0x00000035][4] T1 {1 (1001, 0) ()()()}
4205abf5: mov -0xac(%ebp),%edx R@edx[0x40014001][4] T0 M@0xbffff69c[0x00000035][4] T1 {1 (1001, 0) ()()()}
4205ac0b: cmpl $0xffffffff,-0xac(%ebp) I@0x00000000[0xffffffff][1] T0 M@0xbffff69c[0x00000035][4] T1 {1 (1001, 0) ()()()}
4205ac14: movzbl -0xac(%ebp),%eax R@eax[0x42130b80][4] T0 M@0xbffff69c[0x00000035][1] T1 {1 (1001, 0) ()()()}
4205ac24: push %eax R@eax[0x00000035][4] T1 {1 (1001, 0) ()()()} M@0xbffff604[0x4213030c][4] T0
4205ac25: mov 0x8(%ebp),%eax R@eax[0x00000035][4] T1 {1 (1001, 0) ()()()} M@0xbffff750[0x4212d980][4] T0
4207793a: mov 0xc(%ebp),%edx R@edx[0x00000035][4] T1 {1 (1001, 0) ()()()} M@0xbffff604[0x00000035][4] T1 {1 (1001, 0) ()()()}
42077945: cmp %dl,-0x1(%eax) R@dl[0x00000035][1] T1 {1 (1001, 0) ()()()} M@0x40014000[0x00000035][1] T1 {1 (1001, 0) ()()()}
42077974: movzbl %dl,%eax R@dl[0x00000035][1] T1 {1 (1001, 0) ()()()} R@eax[0x40014000][4] T0
42077960: cmp $0xffffffff,%eax I@0x00000000[0xffffffff][1] T0 R@eax[0x00000035][4] T1 {1 (1001, 0) ()()()}
4205ac39: movzbl -0x9d(%ebp),%eax R@eax[0x00000035][4] T1 {1 (1001, 0) ()()()} M@0xbffff6ab[0x00000064][1] T0
4205c550: mov $0xa,%edx I@0x00000000[0x0000000a][4] T0 R@edx[0x00000035][4] T1 {1 (1001, 0) ()()()}
4205c566: cmpl $0xffffffff,-0xac(%ebp) I@0x00000000[0xffffffff][1] T0 M@0xbffff69c[0x00000035][4] T1 {1 (1001, 0) ()()()}
4205dcd1: movzbl (%eax),%edi R@edi[0x00000000][4] T0 M@0x40014000[0x00000035][1] T1 {1 (1001, 0) ()()()}
4205dcd8: mov %edi,-0xac(%ebp) R@edi[0x00000035][4] T1 {1 (1001, 0) ()()()} M@0xbffff69c[0x00000035][4] T1 {1 (1001, 0) ()()()}

VineIL

Vineが生成するVineILは静的単一代入形式の中間表現であり,CFGの情報が損なわれることはない.中間表現の生成をinstruction liftingという.なお,VineILはValgrindの中間表現を扱うライブラリVEXをもとに生成される.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
~/vine/examples$ ../trace_utils/appreplay -trace five.trace -ir-out five.ir
~/vine/examples$ cat five.ir | awk 'NR==1000,NR==1020'
R_CC_OP_16:reg32_t = 0xd:reg32_t;
T_32t9_1114:reg32_t = cast(T_8t3_1108:reg8_t)U:reg32_t;
R_CC_DEP1_17:reg32_t = T_32t9_1114:reg32_t;
R_CC_DEP2_18:reg32_t = 0:reg32_t;
R_CC_NDEP_19:reg32_t = 0:reg32_t;
/*eflags thunk: logic*/
R_CF_10:reg1_t = false;
T_7_1115:reg8_t = cast(T_32t9_1114:reg32_t)L:reg8_t;
R_PF_11:reg1_t =
!cast(
((T_7_1115:reg8_t >> 7:reg32_t ^ T_7_1115:reg8_t >> 6:reg32_t)
^ (T_7_1115:reg8_t >> 5:reg32_t ^ T_7_1115:reg8_t >> 4:reg32_t))
^
((T_7_1115:reg8_t >> 3:reg32_t ^ T_7_1115:reg8_t >> 2:reg32_t)
^ (T_7_1115:reg8_t >> 1:reg32_t ^ T_7_1115:reg8_t))
)L:reg1_t;
R_AF_12:reg1_t = false;
R_ZF_13:reg1_t = T_32t9_1114:reg32_t == 0:reg32_t;
R_SF_14:reg1_t = 1:reg32_t == (1:reg32_t & T_32t9_1114:reg32_t >> 7:reg32_t);
R_OF_15:reg1_t = false;

出力している行の番号は適当.

最弱事前条件

最弱事前条件(weakest precondition)はDijkstraによる述語変換意味論の基礎を成す概念である.Sを条件,式をRとした際,最弱事前条件WP(S, R)は,Rを実行する前にS’が成り立っていればSの実行後にSが成り立つ最も弱い条件S’を表す.単純な例だと,以下のように表現される.

1
2
3
WP(S, x=e) = S[e/x]
WP(new == org, new = new+taint)
= new+taint == org

Vineにおける最弱事前条件の出力は,以下のようになる.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
~/vine/examples$ ../trace_utils/appreplay -trace five.trace -wp-out five.wp
~/vine/examples$ grep let five.wp | head -n 20
let post_1681:reg1_t = true in
let R_EAX_1682:reg32_t = 0x40014000:reg32_t in
let idx_1683:reg32_t = 0x40014000:reg32_t in
let val_1684:reg8_t = INPUT_1001_0000_61:reg8_t in
let temp_1685:reg8_t = val_1684:reg8_t & 0xff:reg8_t in
let temp_1686:reg8_t = temp_1685:reg8_t >> 0:reg8_t in
let towrite_1688:reg8_t = cast(temp_1686:reg8_t)L:reg8_t in
let mem_arr_1687:reg8_t[4294967296] =
let mem_arr_57[0x40014000:reg32_t]:reg8_t = towrite_1688:reg8_t in
mem_arr_57:reg8_t[4294967296]
in
let R_EAX_1689:reg32_t = 0x40014000:reg32_t in
let R_GDT_1690:reg32_t = 0xc02dbd80:reg32_t in
let R_LDT_1691:reg32_t = 0xc02dcc58:reg32_t in
let R_DFLAG_1692:reg32_t = 1:reg32_t in
let T_32t0_1693:reg32_t = R_EAX_1689:reg32_t in
let T_8t2_1694:reg8_t = mem_arr_1687[0x40014000:reg32_t]:reg8_t in
let T_32t1_1695:reg32_t = cast(T_8t2_1694:reg8_t)U:reg32_t in
let R_EAX_1696:reg32_t = T_32t1_1695:reg32_t in
let temp_1697:reg32_t = R_EAX_1696:reg32_t & 0xffff00ff:reg32_t in
let temp_1698:reg32_t = cast(0:reg8_t)U:reg32_t in
let temp_1699:reg32_t = temp_1698:reg32_t << 8:reg8_t in

このような手法でソースコードの存在しないバイナリから最弱事前条件を抽出し,仕様書を復元する試みがあるらしい.ゾッとする.

STP formula

Vineは,TEMUのトレースファイルからSTP formulaを出力する.STP formulaとはSMTソルバであるSTP用のフォーマットである.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
~/vine/examples$ ../trace_utils/appreplay -trace five.trace -stp-out five.stp
~/vine/examples$ head -n 20 five.stp
% free variables:
mem_arr_57 : ARRAY BITVECTOR(64) OF BITVECTOR(8);
INPUT_1001_0000_61 : BITVECTOR(8);
% end free variables.
ASSERT( 0bin1 =
(LET post_1681 =
0bin1
IN
(LET R_EAX_1682 =
0hex40014000
IN
(LET idx_1683 =
0hex40014000
IN
(LET val_1684 =
INPUT_1001_0000_61
IN
(LET temp_1685 =

SMTソルバは充足可能性問題を解く.では,ここで与えられる命題とは何か.それは,任意の初期値がトレースファイルの結果と一致するというものだ.STPは命題が充足可能か解こうとし,充足不能であった場合は反例を出力する.

1
2
3
~/vine/examples$ cat >>five.stp
QUERY(FALSE);
COUNTEREXAMPLE;

ここで出力される反例は,実行経路に影響を与えた入力値となるようだ.five.traceでは,0x35(ASCIIで5)という入力値が分岐に影響を与えている.

1
2
3
~/vine/examples$ ../stp/stp five.stp
Invalid.
ASSERT( INPUT_1001_0_61 = 0hex35 );

これはトレースファイルに対する静的なシンボリック実行だと言える.シンボリック実行とは,記号によって表現したプログラムの変数を操作することで,実行経路に影響する制約を抽出する静的解析の手法である.シンボリック実行は到達定義の解析などモデルベーステストの領域で発展してきたが,マルウェアの挙動解析に役立てられないだろうか.

BAP

BAPはDavid BrumleyらによるVineの再実装である.彼らはCMUに所属しており,PPPのメンバーでもある.彼らは脆弱性解析の自動化をmotivationとしてBitBlazeを扱ってきた.BAPはVineをより発展させたプロジェクトであり,逆アセンブリやTEMUのトレースファイルから中間表現BILを生成するほか,CFGのみならずCDG(control dependence graphs)やDDG(data dependence graphs)の出力をサポートしているようだ.

おわりに

TEMUのトレースファイルについて,ざっくりVineによる静的解析を行った.とりあえず動かしてみただけなので,コードを噛み砕く必要がある.気になるのはやはり中間表現のフォーマットだ.一度,QEMU,Valgrind,DynamoRIO,LLVM,Vine,BAPなどの中間表現について,対応を整理したほうが良いかもしれない.