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/