はじめに

 今年のセキュリティ・キャンプでは,うっかり「なぜマルウェア解析は自動化できないのか」という題の講義を行ってしまったが,それだけセキュリティの世界には自動化の波が来ている.本稿では,脆弱性分析の自動化をめざして開発されているangr, AFL, Drillerをざっくり紹介する.

angr

 angrはUCSBの研究チームにしてCTFチームShellphishを中心に開発されているバイナリ解析フレームワーク.論文[PDF]はIEEE S&P 2016に採択されている.手法の新規性というよりは実装力でゴリ押しするタイプ.評価には,アメリカ国防高等研究計画局が5,500万ドル(約56億円)の資金を投じてまで開催した脆弱性分析・修正の自動化コンペ,DARPA Cyber Grand Challenge (CGC) のデータセットが用いられている.CGCの決勝戦に進出したチームには75万ドル(約7,600万円),優勝したチームは200万ドル(約2億円)が与えられる.angr開発の目的のひとつが,CGCでの勝利にあることは疑いようもない——最終的な戦績は,CMUのツールMAYHEMに優勝を譲って3位だったが.
 さて,angrはシンボリック実行やプログラムスライシングを通して,プログラムの特定位置に到達するための入力値を抽出することができる.次のコードで雰囲気をつかめるだろうか:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
#!/usr/bin/env python
#-*- coding:utf-8 -*-
import sys
import angr
import simuvex
# 解析対象を指定
p = angr.Project(sys.argv[1])
# 制御フローグラフの生成
cfg = p.analyses.CFG()
print [x for x in cfg.functions.iteritems()]
# シンボルを取得
target_addr = p.loader.main_bin.get_symbol("main").addr
# パス分析クラスのインスタンス
pg = p.factory.path_group()
# シンボルへのパスを分析
pg.explore(find = target_addr)
# avoidを避け,findに到達する入力値を探索してくれる
a = p.surveyors.Explorer(find = FIND_ADDR, avoid = AVOID_ADDR).run()
# フック
p.hook_symbol('strlen', simuvex.SimProcedures['stubs']['ReturnUnconstrained'])
# 実行結果のダンプ
a.found[0].state.posix.dumps(1)

 解析対象の規模が大きい場合,エントリポイントを起点とした解析に時間を要するあるいは失敗することがあるが,プログラムの途中から解析を始めることも可能だ.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
p = angr.Project(sys.argv[1])
# 解析の起点となるアドレス
state = p.factory.blank_state(addr = START_ADDR)
# その地点までプログラムを実行したときのスタックの状態
state.regs.ebp = BASE_ADDR
state.regs.esp = STACK_ADDR
# 入力値の設定
for i in range(INPUT_LENGTH):
s = state.se.BVS('Var[{}]'.format(i), 32, explicit_name = True)
state.memory.store(INPUT_ADDR + i * 4, s)
path = p.factory.path(state)
a = p.surveyors.Explorer(start = path, find= FIND_ADDR, avoid= AVOID_ADDR)
a.found[0].state.posix.dumps(1)

 シンボリック実行はSSA形式の中間表現を前提とするが,angrはValgrindのVEX IRを用いている.バックエンドのSMTソルバはZ3だが,claripyという自前のラッパが噛ませてある.
 これ以上の説明は公式ドキュメントに譲ろう.

AFL

 AFL (American Fuzzy Lop) はGoogleのエンジニアlcamtufを中心に開発されているファジングツール.遺伝的アルゴリズムによって正常な入力を次々と変異させていき,自動的にプログラムのバグを検出する.AFLにはbashやtcpdump, OpenSSHといったさまざまなソフトウェアのバグを検出した実績があり,いまや脆弱性分析の研究になくてはならない存在だ.一般的なファジングはプログラムの浅い箇所にしか到達できない.AFLは,大量の正常な入力をトリミングしてシードとするコーパス蒸留 (corpus distillation) と,遺伝的アルゴリズムを用いてシードを変異させるGAFuzzingのいいとこ取りを図ったものだ.その実行フローは次のようになる:

  1. ユーザーから与えられた初期テストケースをキューに入れる
  2. キューから次の入力テストケースをひとつ取り出し,
  3. プログラムの振る舞いに影響を与えない最小サイズにトリミングする
  4. バランスのよい探索となるよう,さまざまな変異戦略を用いて入力を繰り返し変異させる
  5. 新たな状態遷移が計測されたら,出力をキューに入れる
  6. 2に戻る

 ここでAFLはカバレッジ計測のため,解析対象のプログラムに計測用のコードを埋め込む.これには,解析対象のソースコードが手元にある場合gccやclangの独自フロントエンドが,解析対象のソースコードが手元にない場合QEMUが用いられる.
 ファジング機能の中核は,afl-fuzz.cmain()から呼び出されるfuzz_one()にある.実装されている変異戦略は次の通り:

  • SIMPLE BITFLIP
  • ARITHMETIC INC/DEC
  • INTERESTING VALUES
  • DICTIONARY STUFF
  • RANDOM HAVOC
  • SPLICING

 CGCで優勝したCMUのMAYHEMは,このAFLにシンボリック実行機能を追加していたようだ.MAYHEMといえば同名のシンボリック実行エンジンの論文[PDF]がIEEE S&P 2012で発表されているが,当時からの変更点がどれほどなのかはわからない.
 また,AFLの拡張に,解析対象のパスを枝刈りすることで高速化を図ったAFLFastがある.これもCGC決勝進出チームによるもので,論文[PDF]はACM CCS 2016に採択されている.600行程度のパッチでトップカンファレンス.ちょっと妬ましい.

Driller

 Drillerはangrの開発陣によるAFLの拡張.論文[PDF]はNDSS 2016に採択されている.AFLのREADMEには次のようにある:

Other, more sophisticated research has focused on techniques such as program flow analysis (“concolic execution”), symbolic execution, or static analysis. All these methods are extremely promising in experimental settings, but tend to suffer from reliability and performance problems in practical uses - and currently do not offer a viable alternative to “dumb” fuzzing techniques.

 シンボリック(コンコリック)実行は実用的ではないと切って捨てている.DrillerはangrとAFLを組み合わせることで,この批判を克服し,ファジングとシンボリック実行のいいとこ取りを図ったものだ:

 たとえば,次のコードの解析には,ファジングよりシンボリック実行が適している:

1
2
3
4
5
6
7
int main(void)
{
int x;
read(0, &x, sizeof(x));
if(x == 0x123ABCD)
vulnerable();
}

 なぜなら,ファジングによって0x123ABCDという値を生成するには大量の試行を必要とするからだ.一方で,次のコードの解析には,シンボリック実行よりファジングが適している:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
int check(char *x, int depth)
{
if(depth >= 100){
return 0;
}else{
int count = (*x == 'B') ? 1 : 0;
count += check(x+1, depth+1);
return count;
}
}
int main(void)
{
char x[100];
read(0, x, 100);
if(check(x, 0) == 25)
vulnerable();
}

 なぜなら,単純なシンボリック実行ではパス爆発を解決できないからだ.
 Drillerは両手法の長所と短所を踏まえた上で,それらを堅実に組み合わせている.やはりハッシュ関数の充足はDrillerをもってしても難しいようだが,現行MAYHEMもAFLとシンボリック実行を併用しているようだし,このアプローチが現在の着地点なのだろう.

おわりに

 CGCとそれにともなう研究によって,脆弱性分析の自動化手法は大きな進歩を遂げつつあることが伝わっただろうか.学会のOSS重視傾向も相まって,さまざまなツールを手元で試せるようになってきている.大変ありがたいことだ.

 本稿は情報セキュリティ系論文紹介 Advent Calendar 2015の11日目である.

TL;DR:

 テイント解析(taint analysis)やプログラムスライシング(program slicing),記号的実行(symbolic execution)やファジング(fuzzing)といったバイナリ解析技術を総動員して,マルウェアが通信するC&CサーバのフィンガープリントをC&Cサーバと通信せずとも生成する手法–AUTOPROBE[1]を紹介する.

背景

 マルウェアによるサイバー犯罪はC&Cサーバやコンフィグファイルの配布元,二次検体の配布元など様々な悪性サーバ(malicious server)からなるインフラによって支えられている.攻撃者はこれらの悪性サーバを頻繁に閉鎖・移転させて対策から逃れようとする.とりわけ攻撃者の命令を送信してマルウェアの動作を決定するC&Cサーバはその後の攻撃の起点となるため早期発見が望ましい.したがって不審なサーバがC&Cサーバかどうか判定するフィンガープリントが必要となる.
 しかしながら従来のフィンガープリント生成手法にはC&Cサーバとの長期的な通信を前提としている[2],サーバとして動作するマルウェアを前提としている[3]といった問題点があった.

問題定義

 あるマルウェアのファミリFに属する検体Pを入力として受け取り,Fが用いるC&Cサーバのフィンガープリントφを出力することがAUTOPROBEの目的である.C&Cサーバ側のコードは参照できず,マルウェアの検体はシンボル情報やソースコードを含んでいなくともよい.またマルウェアは複数のリクエストをC&Cサーバに送信するものとする.

提案手法

 あるサーバにマルウェアと同様のリクエストを送って,マルウェアがコマンドとして解釈できるレスポンスが返ってきたら,そのサーバは疑いようもなくC&Cサーバである–AUTOPROBEの鍵となる発想は至極単純だ.
 AUTOPROBEは検体の命令・API・システムコールの実行を–おそらくQEMUによって–トレースし,リクエストを生成する処理とレスポンスをハンドルする処理をそれぞれマルウェアから抽出する.つづいて前者によって不審なサーバに対するリクエストを生成し,後者によってレスポンスをハンドルする.レスポンスハンドリングの可否をもってフィンガープリントとするから,その処理の抽出さえできれば不審なサーバがC&Cサーバかどうか判定するまで実際のC&Cサーバと通信する必要はない–でもどうやって?

リクエスト生成

 マルウェアの多くは時間や擬似乱数,OS情報などの環境依存の値によって動作を変更する.たとえばWin32/LoadMoney.AFはレジストリキーの有無によって送信するリクエストを変更する.

 不審なサーバがC&Cサーバかどうか判定するためには攻撃者の期待するリクエストをより多く送信しより多くレスポンスを得たい.そこでAUTOPROBEは以下のアルゴリズムにしたがって複数の実行トレースを得る.これは条件分岐の度に直前のシステムコールを参照する,ある種の深さ優先探索として実装される.

 さらにAUTOPROBEはトレースをスライスし,システムコールの結果に依存する値を環境依存の値として決定論的な値・定数と区別する.ここで環境依存の値を書き換えれば攻撃者の期待するリクエストを送信できるようになる.また環境依存の値に影響するシステムコールの戻り値に時間,IPアドレス,擬似乱数,OS情報など200種類のラベルを設定しているとのことだ.

レスポンスハンドリング

 生成したリクエストをC&Cサーバに送信してレスポンスを得たら,AUTOPROBEはレスポンスの各バイトを記号値として扱い,実行トレースから検体の分岐制約を充足する解およびスライスθ1を得る.ここで探索の終了条件はclosesocketexitprocessに到達した場合,データを受信してから50個の条件分岐にわたってそのデータを参照するものが存在しない場合である.つづいてレスポンスとして正しく解釈できない値を検体に与え,実行トレースから分岐制約を充足する解およびスライスθ2を得る.ここでηは以下の式によって得られる実行経路の類似度である.

 bnとfnはそれぞれ各スライスに含まれるユニークなコードブロックとシステムコールの数を示す.AUTOPROBEはηが閾値10を下回ればレスポンスを正しく解釈していない実行経路とみなしてスライスを破棄し,上回れば別々のハンドラであるとしてそれぞれの分岐制約をフィンガープリントとして保持する.たとえばこんなふうに.

 C&Cサーバからレスポンスを得られなければ,AUTOPROBEは記号的実行とファジング,フラグレジスタの書き換えによる強制実行(forced execution)を併用してレスポンスに依存する実行経路を探索する.

 このファジングでは検体にランダム値を与えるが,検体が用いるアルゴリズムがHTTPなど既知のものであればエラーメッセージのハンドラを起点に探索する.
 AUTOPROBEはこのように探索したレスポンスのハンドラをフィンガープリントとするが,期待されるレスポンスが得られずさきほどのアルゴリズムによって探索した場合は以下のようにC&Cサーバの尤もらしさを算出する.

評価

 論文ではふたつのデータセットを用いてAUTOPROBEの性能を評価している.ひとつはSality, ZeroAccess, Ramnit, Bamital, Taidoorを含む37ファミリ10亜種計370検体.もうひとつはネットワーク通信の特徴量に基づいてフィンガープリントを生成する既存研究–CYBERPROBE[2]で用いられた19ファミリ. “which have been kindly provided to us by the authors of CYBERPROBE”って書いてるけどAUTOPROBEと同じメンバーじゃねえか.
 検体の実行時間は5分.

リクエスト生成

 まずはリクエストの生成から.可能であればC&Cサーバとの接続をともなうがAlexaトップ10,000サイトは除外している.ここでAUTOPROBEはC&Cサーバに接続せずとも検体のバイナリを分析してCYBERPROBEと同様の結果を得ている.

 AUTOPROBEはふたつのデータセットに含まれる56ファミリのトレースから105のリクエストを生成した.生成にかかった時間は平均13.2分.リクエストはすべてHTTPであったとのこと.

レスポンスハンドリング

 生成したリクエストのうち76件がC&Cサーバからのレスポンスを引き出した.さらにAUTOPROBEはHTTP 200レスポンスコードを含む同数のランダムなレスポンスを生成し,検体に与えた.これはレスポンスハンドリングの可否によって検体の異なる挙動を確認したいためだ.結果として76件のテストケース中71件(93%)で検体は異なる挙動を示した–期待される受信データを得たマルウェアは一般に10以上のシステムコールと50以上のコードブロックを実行する.残りの5件はC&Cサーバではなかった.つまりAUTOPROBEはマルウェアの通信先がC&Cサーバかどうか正しく判定できている.

ケーススタディ

 たとえばBamitalのリクエストはファイル名・GetVersionExによって得たOS情報・DGA (domain generation algorithm) によって生成したホスト名を含んでいた.AUTOPROBEはこれらの値が依存するシステムコールを得ている.

 C&Cサーバと接続せずともHTTP/1.1 200 OKを与えればBamitalのハンドラは分析できるとのこと.
 また標的型攻撃に用いられるTaidoorのリクエストはGetAdaptersInfoによって得たMACアドレスに依存する値を含んでいた.これによってTaidoorのC&Cサーバは感染端末のみで動作するレスポンスを送信していたようだ.
 ドライブバイダウンロード検体であるSalityのC&Cサーバはspm/s_tasks.php, logos_s.gif, 231013_d.exeというファイルをレスポンスに含んでいた.AUTOPROBEはこれらのファイルの存在するサーバをSalityのC&Cサーバとみなす.などなど.

限定的な探索

 Malware Domain Listに含まれる9,500アドレスの近傍/24サブネット・2.6Mアドレスのスキャン結果.

 VirusTotal, Malware Domain List, そしてURLQueryに発見されていないC&Cサーバを特定できている.

インターネット全体の探索

 ここではBGPからインターネット全体をスキャンし,7,100万ものHTTPサーバを発見している.

 このうちマルウェア3ファミリのC&Cサーバをどれだけ発見できるかCYBERPROBEと比較した結果.

 CYBERPROBEが40件のC&Cサーバを特定しているのにたいしてAUTOPROBEは54件のC&Cサーバを特定している.
 高度化するマルウェアが通信内容を難読化・秘匿する傾向にあることを鑑みると,CYBERPROBEのようにネットワーク通信の特徴量を用いる手法よりもAUTOPROBEのようにバイナリ解析を応用した手法こそ吟味されるべきだろう.

感想

 AUTOPROBEは折しも私が昨年度のインターンシップでほとんど同じようなテーマに取り組んでいたとき発表された.テイント解析のソースを受信データではなくシステムコールの結果に設定することで,リクエストのセマンティクスを復元しようとするAUTOPROBEの発想は野心的であり,さまざまなバイナリ解析技術を結集して未知のC&Cサーバを発見する手際は鮮やかというほかない.
 私は来年書くことになる卒業論文のテーマとして,インターネット接続のない閉環境におけるマルウェアの分析に本手法を応用できないか検討している.Ryzhykら[4]はデバイスドライバと環境(デバイスおよびOS)との相互作用を有限オートマトンを用いて表現し,デバイスドライバを半自動的に合成する手法を提案している.問題領域は異なるがこうした手法も検討したい.

用語解説

  • テイント解析
    • 任意のデータに設定したタグをルールにしたがって伝搬させることで,データ間の依存関係を分析する手法
  • プログラムスライシング
    • 任意のデータに依存する処理部分をプログラムから抽出する手法
  • 記号的実行
    • プログラムの分岐条件を充足論理問題とし,制約を充足する解を得る手法
  • ファジング
    • 開発者が意図しない入力を自動生成してプログラムに与えることで脆弱性を顕在化させる手法

参考文献

TL;DR:

 ソフトウェアの多くは外部からの入力に依存する実行パス(trigger-based code)をもつ.
 これを記号的実行(symbolic execution, シンボリック実行)などの解析手法から隠蔽する手法として,コラッツの問題を用いた線型難読化(linear obfuscation)がある[1].
 本稿ではしかし,線型難読化されたコードはコンパイラ最適化によってある程度除去できることを示す.

コラッツの問題

 コラッツの問題は数論の未解決問題のひとつである.
 任意の1でない自然数nに対して,nが偶数ならば2で割り,nが奇数ならば3倍して1を足す.この操作を繰り返していくと,どのような自然数nから出発しても,有限回の操作のうちに必ず1に到達する.
 この定理は経験則的に正しいと考えられているが,いまだ証明はなされていない.

線型難読化

 たとえば次のプログラムtr.cは外部からの入力に依存する実行パスをもつ.

1
2
3
4
5
6
7
8
9
10
11
// tr.c
#include <stdio.h>
int main(int argc, char *argv[])
{
int x=argc;
if(x==2)
printf("triggered!\n");
return 0;
}

 LLVM bitcodeレベルでのtr.cの制御フローグラフは次のようになる.

1
2
3
# clang -emit-llvm -c -g tr.c
# opt tr.bc -dot-cfg > /dev/null
# dot -Tpng cfg.main.dot > tr.png

 この単純なプログラムにたいして,コラッツの問題にもとづくループを挿入する.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
// tr2.c
#include <stdio.h>
int main(int argc, char *argv[])
{
int x = argc;
int y = x + 1000;
while(y > 1)
{
if(y % 2 == 1)
y = 3 * y + 1;
else
y = y / 2;
if((x - y > 0)&&(x + y < 4))
{
printf("triggered!\n");
break;
}
}
return 0;
}

 変数yは必ず1に到達する,いわば偽の変数である.
 難読化されたtr2.cの制御フローグラフは次のようになる.

 ループが挿入されたことによって実行パスが複雑化していることが見て取れる.

記号的実行

 では,線型難読化がどれほど記号的実行にたいして効力をもつか見てみよう.
 今回はLLVM bitcodeを扱う記号的実行ツールKLEEを用いる.
 まず次のコードを解析対象のソースに追記する必要がある.これは,変数xにたいして記号的実行を適用するという意味である.

1
2
3
4
5
6
7
@@ -3,6 +3,7 @@
int main(int argc, char *argv[])
{
int x=argc;
+ klee_make_symbolic(&x, sizeof(x), "x");
if(x==2)
printf("triggered!\n");

 次に,LLVM bitcodeを生成する.

1
2
3
4
5
6
# clang -emit-llvm -c -g tr.c
tr.c:6:5: warning: implicit declaration of function 'klee_make_symbolic' is
invalid in C99 [-Wimplicit-function-declaration]
klee_make_symbolic(&x, sizeof(x), "x");
^
1 warning generated.

 警告が出るが,気にしてはいけない.この関数呼び出しがKLEEにトラップされることになるのだ.
 ソースコードのないマルウェアなどを分析するにあたっては,IDAなどのデコンパイラでソースを出力し,型情報やシグナルハンドラなどの記述を整えたのち上記のようなコードを挿入するか,あるいはS2EやPANDAといった動的解析環境を頼ることになるだろう.
 それはさておき,KLEEを動かしてみよう.少し前までKLEEをビルドして動かすのはとても面倒だったが,いまではDocker Imageが提供されている.

1
2
# sudo docker pull klee/klee
# sudo docker run --rm -ti klee/klee

 線型難読化をおこなう前のtr.cについて記号的実行をおこなった結果を示す.

1
2
3
4
5
6
7
8
9
10
11
12
13
klee@4d625535c122:~$ time klee tr.bc
KLEE: output directory is "/home/klee/klee-out-1"
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING ONCE: calling external: printf(39707328)
triggered!
KLEE: done: total instructions = 17
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
real 0m0.032s
user 0m0.009s
sys 0m0.012s

 パスは2つしか存在しないため,32msecで解析が終わっている.
 ならば,線型難読化を施した後のtr2.cについてはどうか.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
klee@4d625535c122:~$ time klee tr2.bc
KLEE: output directory is "/home/klee/klee-out-2"
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING ONCE: calling external: printf(49859696)
triggered!
triggered!
triggered!
triggered!
triggered!
...
KLEE: done: total instructions = 285809
KLEE: done: completed paths = 158
KLEE: done: generated tests = 158
real 6m11.933s
user 3m56.240s
sys 2m14.245s

 さきほどに比べ,実行パスは158に増加し,解析に11622.9倍(!)もの時間がかかっている.
 今回の単純なプログラムでさえこのようになるならば,複数の入出力に依存する実行パスに線型難読化が施されたらどうなることか.

コンパイラ最適化

 難読化とはえてしてコンパイラ最適化の逆写像である.
 KLEEがLLVMにもとづいているということもあって,LLVMの最適化が線型難読化を除去できるかどうか興味をもった.検証してみよう.

1
# opt -O3 tr2.bc -o tr3.bc

 -O3をもって最適化した後の制御フローグラフは次のようになる.

 最初のtr.cほどではないが,いくらか単純になっていることがわかる.printf()puts()に変換されている.
 では,実行パスは減少しているだろうか.記号的実行をおこなった結果は次の通り.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
klee@4d625535c122:~$ time klee tr3.bc
KLEE: output directory is "/home/klee/klee-out-4"
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING ONCE: calling external: puts(32090720)
triggered!
triggered!
triggered!
triggered!
triggered!
triggered!
triggered!
triggered!
triggered!
KLEE: done: total instructions = 3383
KLEE: done: completed paths = 10
KLEE: done: generated tests = 10
real 0m2.845s
user 0m2.490s
sys 0m0.357s

 実行パスは10とさきほどのtr2.cよりも減少している.実行時間はtr.cの88.9倍であった.

おわりに

 線型難読化は脅威ではないことがわかった–少なくとも提唱者の思惑ほどには.
 塵も積もれば山となるように,線型難読化を多数の箇所に施せばその効力は増すだろう.しかしそれはクラスタリングなどの手法で対処される可能性を高めるだけである.もちろん,どれほどの範囲で難読化を適用すれば効果的かという閾値を探ることに価値はある.
 LLVMの-O3最適化は複数の最適化パスを組み合わせ,再帰的に適用することによっておこなわれる.どのパスが線型難読化の除去にもっとも寄与しているか調べてみるとおもしろいかもしれない(やる気がない).

参考文献

はじめに

2015.08.11~15にわたって開催されたセキュリティ・キャンプ全国大会 2015に解析トラックの講師として参加した.講義では「仮想化技術を用いてマルウェア解析」と題して,QEMUをベースに開発が行われているDECAFという解析プラットフォームを用いて演習を行った.

講義資料

講義内容

演習では実際のマルウェアに用いられている解析妨害機能を備えたサンプルプログラムを扱った.素のDECAFには解析妨害機能への対策が施されていない.そこで,受講者にはDECAFのプラグインを拡張し,対策手法を実装して頂いた.
演習で用いたプログラムはGitHub上で公開している.

  • 解析妨害機能を備えたサンプルプログラム
  • DECAFプラグインのひな形

ひな形にある通り,IsDebuggerPresent()をフックするDECAFプラグインは以下のように書ける.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
static DECAF_Handle isdebuggerpresent_handle = DECAF_NULL_HANDLE;
typedef struct {
uint32_t call_stack[1]; //paramters and return address
DECAF_Handle hook_handle;
} IsDebuggerPresent_hook_context_t;
/*
* BOOL IsDebuggerPresent(VOID);
*/
static void IsDebuggerPresent_ret(void *param)
{
IsDebuggerPresent_hook_context_t *ctx = (IsDebuggerPresent_hook_context_t *)param;
hookapi_remove_hook(ctx->hook_handle);
DECAF_printf("EIP = %08x, EAX = %d\n", cpu_single_env->eip, cpu_single_env->regs[R_EAX]);
free(ctx);
}
static void IsDebuggerPresent_call(void *opaque)
{
DECAF_printf("IsDebuggerPresent ");
IsDebuggerPresent_hook_context_t *ctx = (IsDebuggerPresent_hook_context_t*)malloc(sizeof(IsDebuggerPresent_hook_context_t));
if(!ctx) return;
DECAF_read_mem(NULL, cpu_single_env->regs[R_ESP], 4, ctx->call_stack);
ctx->hook_handle = hookapi_hook_return(ctx->call_stack[0], IsDebuggerPresent_ret, ctx, sizeof(*ctx));
}
static void geteip_loadmainmodule_callback(VMI_Callback_Params* params)
{
if(strcmp(params->cp.name,targetname) == 0)
{
DECAF_printf("Process %s you spcecified starts \n", params->cp.name);
target_cr3 = params->cp.cr3;
isdebuggerpresent_handle = hookapi_hook_function_byname("kernel32.dll", "IsDebuggerPresent", 1, target_cr3, IsDebuggerPresent_call, NULL, 0);
}
}

現在のプロセスがデバッガのコンテキストで実行されていない場合,IsDebuggerPresent()は0を返す.ここで,IsDebuggerPresent()の戻り値を0にするには,モジュール(この場合はkernel32.dll)から戻る段階でeaxを書き換えてやればよい.

1
2
3
4
5
6
7
8
static void IsDebuggerPresent_ret(void *param)
{
IsDebuggerPresent_hook_context_t *ctx = (IsDebuggerPresent_hook_context_t *)param;
hookapi_remove_hook(ctx->hook_handle);
cpu_single_env->regs[R_EAX] = 0; // 追加
DECAF_printf("EIP = %08x, EAX = %d\n", cpu_single_env->eip, cpu_single_env->regs[R_EAX]);
free(ctx);
}

このようにDECAFのプラグインを書くことで,ゲストOSに解析用のエージェントを挿入することなくAPIの戻り値を書き換えることができる.
APIの引数を書き換えたい場合はモジュールに入る段階でコンテキスト構造体のcall_stack[]を書き換えてやればよい.

おわりに

受講者にサンドボックス開発の楽しさと難しさを実感してもらえたなら,講師として冥利に尽きる.
サンプルプログラムには4種類の解析妨害機能を実装しており,APIフックで対処できるのはうち前半2つだけとなっている.限られた演習時間の制約上,3つ目以降の解析妨害機能を回避できた受講者はいなかった.解析トラックリーダーの岩村さんから,受講者の2割がギリギリ解けないような問題を作るようにと仰せつかっていたが,やや意地悪な問題設定だったと思う.
なお,今回は拙作のサンプルを用いたが,より多くの解析妨害機能を備えたOSSにpafishがある.pafishはBackdoor.Win32.Agent.dkbp(MD5: de1af0e97e94859d372be7fcf3a5daa5)など一部のマルウェアに流用されている.

はじめに

V2E: Combining Hardware Virtualization and Software Emulation for Transparent and Extensible Malware Analysis[PDF]“という論文を通して,Record and Replayを用いた解析環境の設計を学ぶ.

著者

この論文のラストオーサーであるYinはSyracuse Universityの助教である.彼はテイント解析の第一人者として知られ,現在はDECAFの開発を主導している.またBitBlaze ProjectのDawn Songや,マルウェア解析の大御所であるChristopher Kruegelと過去に共著を出している.
ファーストオーサーのYanは提案手法をAndroidに適用し,2013年に博士論文を著している.Android向けの拡張にあたっては,DECAFのサブプロジェクトであるDroidScopeを用いているようだ.

Record and Replay

あるいはLogging and Replay, Lockstep, 順序再演法,最小情報トレースなどと呼ばれるこれらは,仮想マシンモニタ上のイベントを記録し,再生するための技術である.乱暴に言うとhistoryからdockerfileやvagrantfileを作成し,deployするようなものだ.
一般にステートマシンにおける命令の出力は,内部状態から一意に与えられる.そこで,ある環境の初期状態と入力のみを記録(Record)し,同じ環境を別の環境の上に再生(Raplay)するといった試みがなされてきた.実マシンにおいては,時刻や割り込みなどの非決定性とその記録の困難性からRecord and Replayは不可能であるとされる.だが,仮想マシンモニタの世界ではこれらの問題をある程度無視できる.実際,VMware Workstationなどにこの機能は実装されている.
本論文では,マルウェア解析に求められるサンドボックスの特性を加味したRecord and Replayについて論じられている.かつて大居さん(@a4lg)が研究されていた内容に近い.

背景

マルウェアを解析するためのサンドボックスは検出不可能(transparent)であり,なおかつ拡張可能であるべきだ.
いかに仮想マシンモニタの存在を隠蔽しようと,Timing Attackなどが成り立つ以上,transparentなサンドボックスを実現することは不可能である.しかし,Intel VTなどハードウェア仮想化技術を用いることで,ほぼtransparentな環境を作り出すことは可能である.例えば,Etherは命令・システムコール単位の解析機能を備えているが,Xenをベースに高いtransparent性を実現している.
だが,ハードウェア仮想化技術に依存した解析環境には拡張性の点で問題がある.特に,instrumentationによる詳細な解析が不可能であるという点は,大きな痛手である.
他方,QEMUなどのソフトウェアエミュレーションは動的バイナリ変換を用いることでDBI(dynamic binary instrumentation)と解析効率の向上を実現している.しかし,transparentなサンドボックスには至れない.
QEMUの動的バイナリ変換はバイナリをコードブロック単位で変換し,softmmuからTLBを参照してアドレス変換を行うというものだ.
そしてその性質から,以下のような自己書き換えコードによって検出されうる.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
__asm{
xor eax, eax
mov edi, target
mov esi, copy_insn
mov ecx, 3
target:
rep movsw // f3 66 a5
jmp qemu_found // eb XX
nop // 90
non_qemu:
...
qemu_found:
...
copy_insn:
_emit 0xeb // eb
_emit 0x01 // 01
_emit 0x90 // 90
_emit 0xeb
_emit 0x01
_emit 0x90
}

実マシンでは,ecx*word=6バイトが1回で書き換わるが,QEMUの動的バイナリ変換では2バイトずつ3回で書き換わる.そのため,1回目の書き換えで0xeb 0x01 0xa5すなわちjmp +01になってしまい,qemu_foundにジャンプしてしまう.
その他には,ページ境界を越えてブロックの変換が行われた場合にページフォルトが発生してしまうことも考えられるし,ブロック境界でのみ割り込みが行われる,CPUサイクルの消費が著しいといった実マシンとの相違点もある.
さらに問題なのが,フラグの遅延評価だ.例えば,cmpjzの組み合わせなどの条件分岐は,EFLAGSを更新する.だが,QEMUにおいてはcmpが実行される段階でEFLAGSの計算は行われない.実際に計算されるのはjzの実行時,それも分岐を決定するためのZFのみが計算される.この設計はエミュレーションの高速化に寄与しているが,もちろん検出に用いることが可能だ.
当然ながら命令のエミュレーション自体にも限界がある.SIMDさえ厳しいのだ,システム管理モードやIntel TXTなんてものは考えたくないだろう.
このように,QEMUによるエミュレーションが検出される余地は枚挙に暇がない.
なお,解析環境検出をテーマとした最近の研究では,第2回システム系論文輪読会で紹介したBareCloudや忠鉢さん(@yuzuhara)のTENTACLEなどがある.

研究目的

ハードウェア仮想化技術を用いる解析環境とソフトウェアエミュレーションを用いる解析環境にはそれぞれ問題がある.そこで,ハードウェア仮想化技術を用いる解析環境でRecordを行い,ソフトウェアエミュレーションを用いる解析環境でReplayを行うことで,検出不可能性と拡張可能性という二つの目的について達成したのが,今回紹介するV2Eである.

形式的定義

本論文におけるRecord and Replayの設計はどのようなものか.
Recorderにおける遷移関数fについて,毎時iにおけるプログラムの状態をSiとし,入力をIiとする.すなわちfSi= f(Si-1, Ii-1)と表される.
次にReplayerにおける遷移関数f'についてプログラムの初期状態をS0とし,全ての入力をIとしたとき,f = f'と言えないだろうか.
これは二つのチューリング機械の同値性が解決可能であるかという問題に相当する.だがEQTM= {(M1, M2)|M1とM2はTMであり,L(M1) = L(M2)}は判定不可能とされ(『計算理論の基礎』における定理5.4),実装上でもハードウェアの割り込みなどの要因からf != f'となってしまう.
そこでV2Eは,プログラムの初期状態と全ての入力を保存することに加え,Sj= S'jとなるようなjについて状態の変化を保存することにした.これはj= Sj- Sj-1と表される.
ここで,新たな遷移関数f'rS'i= f'r(S'i-1, Ii-1, ⊿i)として定義する.これは,i!= nullのときS'i-1+ ⊿iと同値であり,それ以外についてf'(Si-1, Ii-1)と同値をとる.
なお,S0, I, およびf'r, S'i= Sii ∈ [0, n]について恒真である.
これを実装に起こすと,特定の命令やイベントが正しくエミュレート可能な場合は単にそれらをエミュレートし,そうでなければ状態の変化を記録し,Replayにあたって変更を適用するというアプローチになる.

理論と実際

プログラムの大部分を占めるmov, push, popなどのデータ転送命令,call, ret, jz, jmpなどの制御転送命令,add, shlなどの整数演算命令におけるエミュレーションは失敗しないものと見做せる.これらはそのままRecorderでエミュレートされる.
一方で,割り込み,MMIO, Port IO, DMA, TSCについては,V2Eは既存研究を踏襲し,監視領域においてのみこれらをRecordするようになっている.
では,例外,モデル固有レジスタ,cpuidはどうすべきだろうか.既存手法は,これらのエミュレーションは困難であるという理由から,そもそも入力として扱わない戦略を採っていたようだ.V2Eではこれらを, すなわちエミュレートが困難な状態の変化としてRecordすることで,Replayの正確性を高めている.
次に問題となるのが浮動小数点演算とSIMDの扱いだ.MMXやSSEを正確にエミュレートするのは難しい.だが,として命令の結果を記録する設計は大幅なパフォーマンスの低下を招く.そこでV2EはReplayにあたってこれらの命令をパススルーする.もちろん,ReplayerはSIMDをサポートしているマシンで実行されることが前提にある.

Transparent Recorder

RecorderはKVMを用いて実装されている.
V2EはRecord対象の領域とそれ以外のシステムを分割するため,TDP(two dimensional paging)を用いている.何のことかと思ったら,Intel EPTやAMD NPTの総称らしい.

要するに,TDPとは仮想マシンと物理マシン間のページテーブルのことだ.通常のページングでは,メモリアクセスに応じてMMUによってページテーブルが参照され,仮想アドレスが物理アドレスへと変換される.TDPでは,ゲストマシンからの仮想メモリ空間へのアクセスに応じてCR3にセットされたページテーブルが参照され,ゲスト物理アドレスがホスト物理アドレスへと変換される.
この仕組を用いたV2Eは,監視対象用のTDPテーブルと,それ以外用のTDPテーブルを別々に作成する.マルウェアに属するページはCR3の監視に基づき監視対象用のTDPテーブルに書き込まれる.マルウェアとそれ以外の部分のインタラクションはTDPページフォルトやVMExitによって媒介される.共有されるデータは読み取り専用として双方に与えられる.なお,TDPページフォルトに応じてCPUの状態が入力Iiとして保存される.

Precise Replayer

ReplayerはTEMUを用いて実装されている.バイナリ変換器に中間表現がなく,単純に古いQEMU 0.9.1をベースとしているのが玉に瑕だが,TEMUは動的テイント解析に求められる機能をほぼ網羅している.
TEMUはプラグインを共有ライブラリとしてロードし,コールバック関数からテイント解析の機能を呼び出すプラットフォームとなっている.V2EのReplayerは既存のプラグインであるtracecap, unpackerを用いる.だがRecordされたログには監視対象の情報のみが記述されているため,
return ((*TEMU_cpu_hflags & HF_CPL_MASK) != 3)といった,現在実行しているコードが解析対象のものかどうか判定するコードは除去されているようだ.TEMUのプラグインについては,こうした僅かな変更しか施されていない.
一方でその下で動くQEMUには結構手が加えられている.フラグの遅延評価は廃止され,ページフォルト以外の例外は除去されており,SIMDについては独自のヘルパー関数が追加されたようだ.QEMUのdyngenに手を加えるのはなかなか骨の折れる作業だと思う.
さて,Replayを行うためには,ReplayerはRecorderと同様のページングの仕組みをエミュレーションによって再現しなければならない.そこで,V2Eは物理ページコンテナという仕組みを用いている.これは,物理ページがログからロードされていることを示すものである.通常,物理ページコンテナは監視対象用のTDPテーブルを複製する.Replayされたプログラムが物理ページコンテナに存在しないページにアクセスした場合,Replayerは適切なタイミングでログからCPUの状態を復元し,ロードするようになっている.
V2Eにおけるテイント解析はおそらく,マルウェアのメモリ領域を正確に把握するためのものではない.それは,Recorderの段階でTDPテーブルの分割というアプローチによって実現されるべきものだからだ.TEMUのプラグインを使いたかったのだろうが,論文中からはあまりテイント解析を導入することのメリットが読み取れなかった.ここでのテイント解析は解析環境検出の対策に先立つものとして設定されているのだろうか.

評価

解析環境検出については問題なし.cpuid, rdtsc, cmpxch8b, icbp, rep stosb, fnstcwといった命令や,一般保護例外などについてテストされている.なお,rdtscについてはVMRESUME前にホストのTSCを参照することで対応している.
in-the-wildのマルウェアについても実験が行われており,アンパッカーとして期待できるパフォーマンスを見せている.
Recordにおける速度だが,コンテキストスイッチが頻繁に発生するカーネルモードルートキットで17倍,Internet Explorerで5倍と高速だ.KVMのシングルステップモードには3000倍のオーバーヘッドがあると言うのに.
全体的にpositiveな結果で,かなり良い.

おわりに

マルウェアによる解析環境検出に対して,復数の環境を組み合わせたRecord and Replayを用いる研究について紹介した.何より,監視対象とそれ以外で別個にTDPテーブルを作るというアプローチが素晴らしい.自分も研究でテイント解析を扱っているが,この流れを包摂していきたい.
ただ,これはサンドボックス全般に言えることなのだが,感染ホストにおけるユーザーのブラウザ操作が条件分岐に影響するMITBマルウェアについて,どう対処すべきなのだろうか.正常系のユーザーのブラウザ操作をデータセットとしてRecorderに与えたいところだが,果たしてどうなるのか.
このエントリはシステム系論文紹介 Advent Calendar 2014の9日目として書かれた.

参考文献

はじめに

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

シンボリック実行

シンボリック実行とは,プログラムに含まれる変数に具体値を入力せず,その代わりとして値を代表するシンボルの操作を通じてプログラムを模擬的に実行し,結果を評価する技術である.シンボリック実行の目的は,コードカバレッジの拡大にある.シンボリック実行は全てのケースに対して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って奴の仕業なんだ.

はじめに

ここでは,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などの中間表現について,対応を整理したほうが良いかもしれない.

はじめに

シンボリック実行(symbolic execution)という用語をセキュリティ系の論文でよく見かけるようになった.ここでは,シンボリック実行の基礎となる理論を辿る.筆者はソフトウェアテストの研究には疎く,おそらく本稿には若干以上の誤謬と誤解が含まれているだろう.ぜひ識者の教示を乞いたい.

発祥

シンボリック実行は主にソフトウェアテストの領域で古くから研究されてきたトピックである.シンボリック実行という用語の初出は遡ること38年前,James C. KingらによるSymbolic Execution and Program Testing [PDF]という論文だ.Dijkstraがgoto文の濫用による大域脱出を批判したのが1968年であり,Guarded Command Languageを提案したのが1975年のことである.この論文が発表された1976年当時はまさに構造化プログラミングというパラダイムがコンピュータサイエンスの世界を席捲していた時代であった.私が生まれる20年以上前のことで,当時の問題意識を肌身で感じることができないのが少し残念に思える.感覚としては白亜紀のようなもので,主要な登場人物もDijkstraやらKnuthやら,恐竜かよ.
さて,シンボリック実行とはどのような提案だったか.まず,シンボリック実行の目的は「どの入力値でどの実行経路を通るか特定する」ことである.そのためにはどうすればよいだろうか?シンボリック実行はその名の通り,プログラムの変数をシンボル(記号)として表現する.論文中のスニペットはあまりにも古めかしいので,Symbolic execution - Wikipedia, the free encyclopediaを例に考えよう.残念ながら日本語記事はないものの,原理は単純明快.

y = read()
y = 2 * y
if (y == 12)
    fail()
print("OK")

シンボリック実行では入力に具体値を与えない.例えば,変数yに割り当てられる入力値をsというシンボルで表現する.見ての通り,このルーチンはif文で2つの実行経路に分岐するが,この分岐の条件を制約と呼ぶ.ここでの制約は2 * s == 12となる.実行経路を分岐させる条件となる入力値は,式を解けば分かる.言うまでもなく6だ.おっと,これは充足可能性問題というやつじゃないか?その通り,シンボリック実行では制約を解くにあたって制約充足ソルバ(constraint solver)を用いる.ここでは,2 * s == 12という制約が¬s1 ∧ ¬s2 ∧ ¬s3 ∧ ¬s4 ∧ s5 ∧ s6 ∧ ¬s7 ∧ ¬0という連言標準形で表される.2 * ss1s2s3s4s5s6s70に,1200001100となる.
このように,具体値を与えないまま,必ず1つの実行経路を通る制約(path constraints)を求め,条件分岐に影響する入力値の制約を特定する手法がシンボリック実行である.シンボリック「実行」と銘打っていても,実際にプログラムを実行しているわけではない.飽くまでシンボルの操作を通して,擬似的にプログラムを実行しているのだ.

Concolic Testing/Dynamic Symbolic Execution

では,シンボリック実行は銀の弾丸たりえるか?そんなわけがない.真っ先に以下の課題に直面してしまう.

  • 計算爆発
  • 制約充足ソルバで解くことができない制約
  • 入力値が一意に定まらない

そこで,CUTE: A Concolic Unit Testing Engine for C [PDF]において,concolic testingという手法が提案された.concolicとは耳慣れない言葉だが,どういった意味だろうか?これは,symbolic(シンボル)とconcrete(具体値)からなる造語で,concolic testingとはシンボリック実行に具体値(concrete value)を持ち込んだ手法である.またの名を動的シンボリック実行.
具体値を持ち込むとはどういうことか?動的シンボリック実行では,制約充足ソルバが不得手とする非線形な制約に到達した場合,その箇所だけ実際に実行(concrete execution)することで,具体値を代入する.これによって,コードカバレッジを拡大するというのが狙いである.現在「シンボリック実行」と呼ばれているのは概ね動的シンボリック実行である.

KLEE

KLEEはシンボリック実行にLLVM bitcodeを導入したプロジェクトである.チュートリアルはThe Symbolic Maze! - Feliam’s Blogが秀逸.
使い方は簡単で,解析対象のソースコードに#include <klee/klee.h>klee_make_symbolic()とを追加するだけで準備は完了する.klee_make_symbolic()にはシンボリック実行を適用したい変数のアドレスとサイズ,名前を引数として与える.

llvm-gcc --emit-llvm -c -g [file].c
klee [file].o

LLVM bitcodeとしてコンパイルし,KLEEに与えて実行すると,ktestという形式のテストケースが生成される.

ktest-tool --write-ints klee-last/[file].ktest 

ktest-toolを実行すると,入力値が出力される.

ktest file : ‘klee-last/test000001.ktest’
args : ['[file].o']
num objects: 1
object 0: name: ‘hoge’
object 0: size: 4
object 0: data: ‘fuga′

これによって,KLEEは90%以上のコードカバレッジを実現する.論文の評価実験では,Coreutilsについて,15年に渡って作成されてきたテストスイートよりも高いカバレッジをたったの89時間で達成している.
KLEEは多くの研究者に利用されており,シンボリック実行に関する研究のstate-of-the-artはKLEEを分散化したKleeNetだと聞いている.
しかし,もちろんKLEEは万能ではない.特にループ文の解釈がうまくいかないことが多く,これはシンボリック実行が抱える永年の課題である.

STP

KLEEはSTP Constraint Solverという制約充足ソルバを用いている.STPは制約充足ソルバの中でもSMT(Satisfiable Modulo Theories)ソルバと呼ばれるものに相当する.SAT(SATisfiability problem)ソルバはブール式のみを扱うが,SMTソルバはこれに加えて配列やビットベクトル,加減算大小比較など様々な背景理論を用いることができる.STPではAND,OR,NOT,XORといった演算についてもサポートされ,式の最適化についても工夫されているようだ.

S2E

少しばかり,リバースエンジニアリングにも目を向けてみよう.解析対象のソースコードが存在しない場合,どうやってシンボリック実行を適用すればよいだろうか?解決策のひとつとして挙げられるのがS2Eである.
S2EはQEMUの動的バイナリ変換(dynamic binary translation)を用いる.QEMUの動的バイナリ変換機能をTCG(Tiny Code Generator)といい,これによって例えばARM向けにビルドされたバイナリをx86の計算機で動かすといった機能が実現される.
まず,QEMUは対象のバイナリを逆アセンブルし,複数のブロックに分割する.このブロックをTB(translation block)といい,定義はtranslate-all.hに記述されている.TBは分岐命令やページの境界によって区切られる.そして,ブロック単位で逆アセンブルしたコードをgen_intermediate_code()という関数で中間コードに変換し,tcg_gen_code()という関数で他のアーキテクチャの命令とマッピングする.これらはtarget-[arch]/translate.cおよびtcg/tgc.cに記述されている.こうして変換されたコードは,TB単位でキャッシュされる.実行にあたっては,変換されたTBをchainとして繋いでいく.この処理は,main()からcpu_exec()を経由して呼ばれるtb_find_fast()tb_find_slow()に記述されている.こうして,QEMUは異なるアーキテクチャ向けバイナリの実行を可能にしている.
S2Eは,QEMUのTCGを用いてPEファイルをLLVM bitcodeに変換し,KLEEに受け渡す.TCGは,中間コードを変換するにあたって,変換先のアーキテクチャの命令が記述された辞書を参照する.S2Eはこの辞書にLLVM bitcodeを登録することで,実行ファイルをLLVM bitcodeに「逆アセンブル」するのだ.
このようにして,S2Eはシンボリック実行を実現しているが,そもそもLLVM bitcodeに変換する必要はあるのだろうか?KLEEは確かに優れたツールだが,バイナリに直接シンボリック実行を適用すれば良いのではないか?
これには理由がある.QEMUの中間コードも,LLVM bitcodeもレジスタが無限個存在するSSA(Static Single Assignment form,静的単一代入)形式をとっている.一方で,x86アーキテクチャはSSA形式ではない.x86における逆アセンブルコードにシンボリック実行を適用する例を考えよう.

mov esi, 0x09
mov edx, 0x2014

この場合,制約は(esi == 0x09) and (edx == 0x2014)となる.これなら問題はないが,以下の例はどうだろう.

mov esi, 0x09
...
mov esi, 0x2014

同じレジスタに違う値が代入されている.この場合,制約は(esi == 0x09) and (esi == 0x2014)となってしまう.こうした理由から,シンボリック実行にはSSA形式への変換が必要となるようだ.

おわりに

シンボリック実行の基礎を学んだつもりになった.この技術が情報セキュリティの分野でどう活きてくるのかについては,また改めて.進捗だめです.

参考文献