はじめに

シンボリック実行(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形式への変換が必要となるようだ.

おわりに

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

参考文献