KLEEで記号実行してみた~環境構築編~

TL;DR

筆者はシンボリック実行, KLEE, LLVMについては疎く, 誤った情報が含まれているかもしれない.
不十分な点や誤った情報が書かれていた場合は, コメント欄にてお知らせ頂きたい.

KLEEとは

KLEEは、LLVMコンパイラの基板上に構築されたシンボリック仮装マシンです.(中略)
引用元:https://klee.github.io/releases/docs/v2.0/

シンボリック実行とは

シンボリック実行は、入力をシンボル化して実行することをいう。シンボルとは数学でいう変数に相当し、一定の値に固定されない。シンボリック実行では、レジスタ、スタック、メモリ、ファイル等、実行環境がシンボル化される。
引用元:https://speakerdeck.com/katc/girls-meets-symbolic-execution-assertion-2-automated-exploit-generation?slide=9

シンボリック実行については、引用元のスライド(K_atcさん)にて詳しく書かれておりますので、気になった方は読んでみて下さい.

KLEEの初期設定

公式ドキュメントが丁寧なおかげで、簡単に構築できました.
オプションが多いので、詳しくは公式を読んで下さい.

ここでは, 私が実行できるまでの過程を残しておきます.
尚, /path/toは適宜自身の環境に置き換えてください.

Dockerで構築する場合

$ docker pull klee/klee
$ docker run -ti --name=my_first_klee_container --ulimit='stack=-1:-1' klee/klee

Ubuntu18.04.2で構築する場合

筆者の環境

$ uname -a
Linux 5.0.0-37-generic #40~18.04.1-Ubuntu SMP Thu Nov 14 12:06:39 UTC 2019 x86_64 x86_64 x86_64 GNU/Linux
$ lsb_release -a
No LSB modules are available.
Distributor ID:	Ubuntu
Description:	Ubuntu 18.04.3 LTS
Release:	18.04
Codename:	bionic

LLVM周りのライブラリとLLVM6.0の導入

$ sudo apt-get install build-essential curl libcap-dev git cmake libncurses5-dev python-minimal python-pip unzip libtcmalloc-minimal4 libgoogle-perftools-dev libsqlite3-dev doxygen
$ pip3 install tabulate

$ sudo apt-get install clang-6.0 llvm-6.0 llvm-6.0-dev llvm-6.0-tools 

制約ソルバのインストール. ここではSTPを選択.
Z3もその内使ってみたい.

sudo apt-get install cmake bison flex libboost-all-dev python perl zlib1g-dev minisat
$ git clone https://github.com/stp/stp.git
$ cd stp
$ git checkout tags/2.3.3
$ mkdir build
$ cd build
$ cmake ..
$ make
$ sudo make install

$ ulimit -s unlimited

uClibcとPOSIX環境モデルの構築
ERROR:llvm-config cannot be foundと,llvm-configが認識されなかったので、オプションを追加.

$ git clone https://github.com/klee/klee-uclibc.git  
$ cd klee-uclibc  
$ ./configure --make-llvm-lib --with-llvm-config /path/to/llvm-6.0/bin/llvm-config 
$ make -j2  
$ cd .. 

Googleのテストソースを入れる

$ curl -OL https://github.com/google/googletest/archive/release-1.7.0.zip
$ unzip release-1.7.0.zip

テストツールのlitを入れる

$ pip install lit

KLEEのソースを入手

$ git clone https://github.com/klee/klee.git
$ cd klee
$ mkdir build

cmakeを使う. 絶対パスにする事

cmake \
-DENABLE_SOLVER_STP=ON \
-DENABLE_POSIX_RUNTIME=ON \
-DENABLE_KLEE_UCLIBC=ON \
-DKLEE_UCLIBC_PATH=/path/to/klee-uclibc \
-DGTEST_SRC_DIR=/path/to/googletest-release-1.7.0 \
-DLLVM_CONFIG_BINARY=/path/to/llvm-6.0/bin/llvm-config \
-DLLVMCC=/path/to/clang \
-DLLVMCXX=/path/to/clang++ \
..

KLEEをビルド

$ make

一応テストしました

$ make systemtests
Scanning dependencies of target systemtests
[100%] Running system tests
Testing Time: 46.51s
  Expected Passes    : 279
  Expected Failures  : 2
  Unsupported Tests  : 10

litの方も一応

$ lit test/
Testing Time: 47.68s
  Expected Passes    : 279
  Expected Failures  : 2
  Unsupported Tests  : 10

これでkleeが実行できるようになったので, klee/build/bin/にパスを通して起きましょう.

次の記事で,チュートリアルに従いKLEEを触ってみます.

参考文献

Using KLEE with Docker
https://klee.github.io/docker/

Building KLEE with LLVM 6.0
https://klee.github.io/build-llvm60/