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

Posted 秦皇汉武

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了实验三:klee的执行重现机制(示例分析)相关的知识,希望对你有一定的参考价值。

结论性内容:

(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 > 1 ? atoi(argv[1]) : 0;
    if (result == 42)
    {
    klee_assert(0);   
    }
    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错误的测试用例:

 

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

可以看到,即使是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/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

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

 

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

 

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

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

使用脚本:

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

 

三个测试输入依次是:

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

42

+42

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

 

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

代码:

int main() { //test4.c
    int argc=2;
    int size=4;
    char argv[size];
    klee_make_symbolic(argv, sizeof argv, "argv");
    argv[3]=\'\\0\';
    int result = argc > 1 ? atoi(argv) : 0;
    if (result == 42)
    {
    klee_assert(0);   
   //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的重现机制。我们看到,可以使用KTEST_FILE的方式。

 

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

 

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

 

 

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

 

以上是关于实验三:klee的执行重现机制(示例分析)的主要内容,如果未能解决你的问题,请参考以下文章

[NTUSTISC pwn LAB 7]Return to libc实验(puts泄露libc中gadget片段定位)

KLEE概览

[NTUSTISC pwn LAB 5]rop入门实验

编译原理 实验一 java语言实现对C语言词法分析

编译原理 实验一 java语言实现对C语言词法分析

[NTUSTISC pwn LAB 6]rop&Return to plt实验