对 KLEE 的学习，一些小小的自动化操作。

按照 Panda 大佬的博客 CISCN little_evil 走到了最后一层，也就是 VM 分析，这种情况怎么能不上自动化工具呢。我尝试了一下 angr 没跑出来，可能是参数配置有问题，换成 KLEE 跑出来了。

KLEE 的安装配置暂且不谈。在分析 VM 时我们把虚拟机指令转换为一个 .c 文件，暂且称它为 vm.c。接下来使用 clang 将它编译为 .bc。

1

clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone vm.c

编译参数介绍

  • -emit-llvm -c 生成 .bc IR 而不是 .ll IR。
  • -O0 -Xclang -disable-O0-optnone 关闭编译器优化功能，并禁止 optnone 阻止 KLEE 对 IR 的优化。

然后传给 KLEE。

1

klee -posix-runtime --libc=uclibc --exit-on-error vm.bc -sym-stdin 10

调试的时候发现所有 arr1[var6] = getchar(); 中的 var6 都是 2，也就是说每次输入的位置相同。klee 的参数含义如下。

  • -posix-runtime 允许使用符号环境选项作为程序选项的一部分。
  • --libc=uclibc 默认情况下，KLEE 只适用于不使用任何外部代码的封闭程序，如果想使用 KLEE 运行实际程序的话需要启用 KLEE POSIX 运行时，它构建在 uClibc C 库上。
  • --exit-on-error 一出错就立刻退出，但这里没有用上。
  • -sym-stdin 10 将标准输入符号化，这里的大小为 10。

在探索完所有路径之前，KLEE 一般不会自动停止，跑了一会让它强行退出。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

KLEE: NOTE: Using POSIX model: /tmp/klee_build90stp_z3/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca
KLEE: NOTE: Using klee-uclibc : /tmp/klee_build90stp_z3/runtime/lib/klee-uclibc.bca
KLEE: output directory is "/ctf/klee-out-4"
KLEE: Using STP solver backend
warning: Linking two modules of different target triples: test.bc' is 'x86_64-unknown-linux-gnu' whereas '__uClibc_main.os' is 'x86_64-pc-linux-gnu'

KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 94565417872864) at klee_src/runtime/POSIX/fd.c:1007 10
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
Input:OK

实际上可以看到，KLEE 已经跑出了正确的结果并且输出 “OK” 了，接下来就是寻找正确的输入了。

查看 klee 的输出文件夹 klee-last，发现里面的 testcase 有成百上千个，这很难一个一个找。但是我们有源码啊，修改代码，在最后一个 putchar 之后添加一个 klee_assert(0)，同时也别忘了在开头加上 #include <klee/klee.h>。我们重新编译

1

clang -emit-llvm -c -g -I /home/klee/klee_build/include/ -O0 -Xclang -disable-O0-optnone vm.c

接下来再用 KLEE 跑就能成功地在输出 “OK” 之后停下了：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

klee@4288a4d61a45:/ctf$ klee -posix-runtime --libc=uclibc --exit-on-error vm.bc -sym-stdin 10
KLEE: NOTE: Using POSIX model: /tmp/klee_build90stp_z3/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca
KLEE: NOTE: Using klee-uclibc : /tmp/klee_build90stp_z3/runtime/lib/klee-uclibc.bca
KLEE: output directory is "/ctf/klee-out-6"
KLEE: Using STP solver backend
warning: Linking two modules of different target triples: vm.bc' is 'x86_64-unknown-linux-gnu' whereas '__uClibc_main.os' is 'x86_64-pc-linux-gnu'

KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 93853363972112) at klee_src/runtime/POSIX/fd.c:1007 10
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
Input:OKKLEE: ERROR: vm.c:1568: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: EXITING ON ERROR:
Error: ASSERTION FAIL: 0
File: vm.c
Line: 1568
assembly.ll line: 14844
State: 1
Stack:
        #000014844 in __klee_posix_wrapped_main () at vm.c:1568
        #100007349 in __user_main (=3, =93853346892320, =93853346892352) at klee_src/runtime/POSIX/klee_init_env.c:245
        #200000587 in __uClibc_main (=93853363422608, =3, =93853346892320, =0, =0, =0, =0) at libc/misc/internals/__uClibc_main.c:401
        #300000752 in main (=3, =93853346892320)

我们看一下最新的输出是

1
2
3
4

klee@4288a4d61a45:/ctf$ cat klee-last/test000011.ktest
KTESTvm.bc
-sym-stdin10stdin
M5Ya7

“M5Ya7” 为我们想要的结果。我们可以手动验证，也可以用 klee-replay 功能重放。但是在那之前，需要我们生成可执行文件：

1
2

export LD_LIBRARY_PATH=/home/klee/klee_build/lib/:$LD_LIBRARY_PATH
gcc -I /home/klee/klee_build/include/ -L /home/klee/klee_build/lib/ vm.c -lkleeRuntest

之后运行

1
2
3
4
5
6
7
8
9

klee@4288a4d61a45:/ctf$ klee-replay ./a.out klee-last/test000011.ktest
KLEE-REPLAY: NOTE: Test file: klee-last/test000011.ktest
KLEE-REPLAY: NOTE: Arguments: "./a.out"
KLEE-REPLAY: NOTE: Storing KLEE replay files in /tmp/klee-replay-XZMaQu
KLEE-REPLAY: NOTE: Creating file /tmp/klee-replay-XZMaQu/fd0 of length 10
KLEE-REPLAY: WARNING: check_file stdin: dev mismatch: 108 vs 2096
a.out: vm.c:1568: main: Assertion `0' failed.
KLEE-REPLAY: NOTE: EXIT STATUS: CRASHED signal 6 (0 seconds)
KLEE-REPLAY: NOTE: removing /tmp/klee-replay-XZMaQu

参考资料