李一鸣 华东师范大学软件工程学院 电子信息

最近在看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，这样就可以得到持久化的镜像。等待开发完成后再将其删除

5.参考的教程链接：