结论性内容:

(1)如果是在程序中使用klee_make_symbolic,则可以使用下列脚本进行重现。

export LD_LIBRARY_PATH=/home/klee/xiaojiework/klee-xiaojie/build/debug/lib/:$LD_LIBRARY_PATH
gcc -L /home/klee/xiaojiework/klee-xiaojie/build/debug/lib/ test4.c -lkleeRuntest
KTEST_FILE=klee-last/test000015.ktest ./a.out

(2)如果是对命令行参数进行建模,即对klee进行符号执行的时候,使用 --posix-runtime选项,设定sym-args等参数,则重现只能用klee-replay,不能用(1)中的脚本。不需要链接到klee的运行库-lkleeRuntest,并且直接用gcc对代码进行编译成本地代码即可。

示例代码:

#include <stdio.h>//test.c
#include <string.h>
#include <stdlib.h>
#include <assert.h>
#include <klee/klee.h>
int main(int argc, char* argv[]) {
int result = argc > ? atoi(argv[]) : ;
if (result == )
{
klee_assert();
}
return result;
}

脚本:

clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3

执行结果:

klee@ubuntu:~/kleeexperiment/modeltest$ klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3

KLEE: NOTE: Using klee-uclibc : /usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca

KLEE: NOTE: Using model: /usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bca

KLEE: output directory is "/home/klee/kleeexperiment/modeltest/klee-out-31"

KLEE: Using STP solver backend

KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 71386000)

KLEE: WARNING ONCE: calling __user_main with extra arguments.

KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.

KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:22: ASSERTION FAIL: 0

KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 11567

KLEE: done: completed paths = 73

KLEE: done: generated tests = 69

查看对应assertion错误的测试用例:

实验三:klee的执行重现机制(示例分析)-LMLPHP

我们直接对程序输入+42,进行执行重现。

实验三:klee的执行重现机制(示例分析)-LMLPHP

可以看到,即使是gcc test2.c -o test2(不是gcc -L /home/klee/xiaojiework/klee-xiaojie/build/debug/lib/ test2.c -lkleeRuntest),并且LD_LIBRARY_PATH是空的。为什么gcc能够在不链接到-lkleeRuntest的时候,对klee-assert进行解释呢?

实验三:klee的执行重现机制(示例分析)-LMLPHP

这是因为在klee/klee.h中是这样定义的:

# define klee_assert(expr) \
((expr) \
? (void) (0) \
: __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__)) \

所以压根不需要链接到kleeRuntest运行库。

下面改用--sym-arg选项,

clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee --libc=uclibc --posix-runtime test2.bc --sym-arg 3

实验三:klee的执行重现机制(示例分析)-LMLPHP

实验三:klee的执行重现机制(示例分析)-LMLPHP

可以看到,和使用--sym-args生成了同样的测试用例。即+42,我们可以直接在命令行使用./test2 +42进行执行重现。

但是,在实际的实验进程中(由于反复试验,求解每次随机返回一个解),我还生成了另外内容的测试用例,同样覆盖assertion错误。内容如下:

实验三:klee的执行重现机制(示例分析)-LMLPHP

对于这个测试用例,内容是\x0b42,实际上就是三个字符,第一个是垂直制表符号,第二个是字符'4',第三个是字符'2'。第一个无法直接通过命令行输入,所以我们使用klee的重现机制。

我们同时搜集的还有内容是‘42\x00\x00’的测试用例,连同之前的两个测试用例,三个测试用例都放在了generatedtests目录下:

使用脚本:

实验三:klee的执行重现机制(示例分析)-LMLPHP

均没有任何assertion fail的反应。但是使用klee-repaly的时候,

实验三:klee的执行重现机制(示例分析)-LMLPHP

三个测试输入依次是:

垂直字表符,42(垂直字表符,我们从键盘是敲不出来的)

42

+42

所以,对命令行建模的时候,需要用klee-replay的机制。

我们采取在程序中使用klee_make_symbolic的方式,再分析一下klee执行重现机制。

代码:

int main() { //test4.c
int argc=;
int size=;
char argv[size];
klee_make_symbolic(argv, sizeof argv, "argv");
argv[]='\0';
int result = argc > ? atoi(argv) : ;
if (result == )
{
klee_assert();
//printf("yes");
}
return result;
}

由于不需要对命令行参数进行建模,我们使用如下脚本:

clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test4.c

klee --optimize --libc=uclibc test4.bc --sym-args 0 1 3

去除了--posix-runtime选项,因为不需要对命令行参数进行建模。需要保留--libc=uclibc选项,因为还要对atoi函数进行建模和处理。

实验三:klee的执行重现机制(示例分析)-LMLPHP

下一步使用klee的重现机制。我们看到,可以使用KTEST_FILE的方式。

实验三:klee的执行重现机制(示例分析)-LMLPHP

再试试klee-replay,结果显示:

实验三:klee的执行重现机制(示例分析)-LMLPHP

由于test4.c中有klee_make_symbolic的语句,导致我们必须链接到lkleeRuntest才能执行重现。我们手动去掉这个语句,再编译成本地可执行代码,不链接到kleeRuntest运行库,即直接使用gcc -o test4 test4.c。结果仍然报错。

实验三:klee的执行重现机制(示例分析)-LMLPHP

分析完毕!klee-replay和KTestFile指定文件各有应用场景,正如随笔一开始所给出的结论性内容。

05-11 17:39