李一鸣 华东师范大学软件工程学院 电子信息
最近在看Symbolic Execution，了解到了一些相关工具。KLEE就是其中之一，这篇文章是基于KLEE的官方教程：Using KLEE With Docker
1. 从Docker Hub拉取KLEE的镜像
$ docker pull klee/klee:2.1
2.运行镜像
通过以下命令创建一个临时容器并获取shell访问权限
其中--ulimit='stack=-1:-1的选项是容器栈大小不做限制，防止stack overflow错误。
$ docker run --rm -ti --ulimit='stack=-1:-1' klee/klee
进入shell查看klee
klee@3c098b05ca85:~$ klee --version
KLEE 2.1 (https://klee.github.io)
Build mode: RelWithDebInfo (Asserts: ON)
Build revision: 938434b2521d4c1ec11af31f1e5e5fbafd2cb2cd
LLVM (http://llvm.org/):
LLVM version 6.0.1
Optimized build with assertions.
Default target: x86_64-unknown-linux-gnu
Host CPU: skylake
同样的查看clang
klee@3c098b05ca85:~$ clang --version
clang version 6.0.1 (branches/release_60 355598)
Target: x86_64-unknown-linux-gnu
Thread model: posix
InstalledDir: /tmp/llvm-60-install_O_D_A/bin
退出容器
klee@3c098b05ca85:~$ exit
3.创建持久化的容器(Persistent Containers)
前面的例子，容器退出之后就被销毁了。如果想接着使用容器，则使用如下命令创建持久化容器
$ docker run -ti --name=my_first_klee_container --ulimit='stack=-1:-1' klee/klee
请注意，没有使用--rm，因此在退出容器时不会销毁它，并且使用--name标志为容器命名。
在容器内部做如下操作
klee@3c098b05ca85:~$ pwd
/home/klee
klee@3c098b05ca85:~$ echo "int main(int argn, char** argv) { return 0; }" > test.c
klee@3c098b05ca85:~$ clang -emit-llvm -g -c test.c -o test.bc
klee@3c098b05ca85:~$ klee --libc=uclibc --posix-runtime test.bc
KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/klee/klee_build/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/klee-out-0"
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 44070352)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: done: total instructions = 5047
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
klee@3c098b05ca85:~$ ls
klee-last klee-out-0 klee_build klee_src test.bc test.c
之后退出容器
klee@3c098b05ca85:~$ exit
可以通过如下命令查看我们刚刚创建的容器
$ docker ps -a
CONTAINER ID IMAGE COMMAND CREATED STATUS PORTS NAMES
1c408467bdf7 klee/klee "/bin/bash" About a minute ago Exited (0) 2 seconds ago my_first_klee_container
通过以下命令重启容器
$ docker start -ai my_first_klee_container
klee@1c408467bdf7:~$ ls
klee-last klee-out-0 klee_build klee_src test.bc test.c
klee@1c408467bdf7:~$ exit
通过以下命令删除容器
$ docker rm my_first_klee_container
4.总结
Docker镜像运行的时候可以不使用--rm，这样就可以得到持久化的镜像。等待开发完成后再将其删除
