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の初期設定

[公式ドキュメント](https://klee.github.io/releases/docs/v2.0/getting-started/)が丁寧なおかげで、簡単に構築できました.
オプションが多いので、詳しくは公式を読んで下さい.

ここでは, 私が実行できるまでの過程を残しておきます.
尚, `/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/`にパスを通して起きましょう.

[次の記事](https://qiita.com/msymt/items/8b341c9252387e640f76)で,チュートリアルに従いKLEEを触ってみます.

## 参考文献

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

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