KLEE 学习笔记

KLEE 的介绍建议直接 GPT。

安装

KLEE 由于是一款符号执行工具，需要 clang 和 llvm 的支持，这两者都可以直接通过 apt 安装，下面介绍 klee 的安装：

git clone https://github.com/klee/klee.git
cd klee
mkdir build
cd build
cmake .. -DENABLE_UNIT_TESTS=OFF -DENABLE_SYSTEM_TESTS=OFF
sudo make install -j4

这里介绍下，安装过程中出现的一些错误：

错误1:

CMake Error at CMakeLists.txt:419 (message):
  Can't find "gperftools/malloc_extension.h"

解决方法：

删除 klee 包文件，重新 git，然后执行

sudo apt-get install libtcmalloc-minimal4 libgoogle-perftools-dev

错误2：

-- Could NOT find SQLITE3 (missing: SQLITE3_LIBRARY SQLITE3_INCLUDE_DIR)
CMake Error at CMakeLists.txt:434 (message):
  SQLite3 not found, please install

解决方法：

删除 klee 包文件，重新 git，然后执行

sudo apt-get install sqlite3 libsqlite3-dev

另外的一些可能存在的错误，可以参考这篇文章

使用

由于 klee 使用 llvm IR 符号执行，那么就需要将源程序编译为 llvm IR 文件，测试文件如下

#include <memory.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>

char* get_message(const char* message) {
	if (strlen(message) <= 4)
		return NULL;

	if (!('F' == message[0] && '\x1' == message[1]))
		return NULL;

	unsigned int message_length = *(unsigned int*)&message[2];
	char* output_message = (char*)malloc(message_length);

	memcpy(output_message,&message[2],message_length);

	return output_message;
}

int main(int argc,char** argv) {
	char input_buffer[0x10] = {0};

	scanf("%s",input_buffer);

	char* message_data = get_message(input_buffer);

	if (NULL == message_data)
		printf("Error for resolve message\n");
	else
		printf("message data : %s\n",message_data);

	return 0;
}

编译命令如下：

clang -emit-llvm -c test.c

这样会发现原目录就会生成一个 test.bc 文件，

klee -libc=klee test.bc 

程序调用了scanf() 函数,需要手动填写一些参数进去,第一次使用klee 执行程序时在scanf() 传递字符 k 并没有触发崩溃,但是在第二次使用klee 执行时输入AAAAAAAAAAAAAAAAAAAAA 就会导致程序崩溃。

查看报错信息，在 test000001.ptr.err 文件中。

使用 ktest-tool 查看test 样本的信息:

$  ktest-tool test000001.ktest 
ktest file : 'test000001.ktest'
args       : ['test.bc']
num objects: 0

使用 klee-stats 查看当前本次测试的状态:

$ klee-stats .
---------------------------------------------------------------------
| Path |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
---------------------------------------------------------------------
|  .   |     372|     1.87|    42.21|    21.43|     154|        0.00|
---------------------------------------------------------------------

klee_make_symbolic()

klee 可以自动对输入进行追踪测试，在之前的程序中，scanf() 函数是输入点，在KLEE 里对于这种用户可控的输可以手工给打上标记，KLEE 提供一个函数，声明如下:

void klee_make_symbolic(void *array, size_t nbytes, const char *name);
//  klee_make_symbolic(内存地址,内存大小,变量名字);

替换scanf为klee_make_symbolic

#include <memory.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>

#include "klee/klee.h"


char* get_message(const char* message) {
	if (strlen(message) <= 4)
		return NULL;

	if (!('F' == message[0] && '\x1' == message[1]))
		return NULL;

	unsigned int message_length = *(unsigned int*)&message[2];
	char* output_message = (char*)malloc(message_length);

	memcpy(output_message,&message[2],message_length);

	return output_message;
}

int main(int argc,char** argv) {
	char input_buffer[0x10] = {0};

	klee_make_symbolic(input_buffer,sizeof(input_buffer),"input_buffer");

	char* message_data = get_message(input_buffer);

	if (NULL == message_data)
		printf("Error for resolve message\n");
	else
		printf("message data : %s\n",message_data);

	return 0;
}

编译命令如下：

clang -emit-llvm -c -I ../../../klee/include test.c

这里的 ../../../klee/include 指向的是安装的 klee 的那个文件夹下 include 的目录路径。

执行命令

klee -libc=klee test.bc 

然后 klee 就可以自动帮我们找漏洞了。

输出的结果都保存到了 klee-out-2 文件夹当中。

这里可以找到发现的所有的崩溃示例：

henry@henry:~/Documents/test/test_klee/klee-out-2$ ls
assembly.ll       test000005.ktest      test000012.ktest    test000019.kquery   test000025.ktest
info              test000006.ktest      test000013.ktest    test000019.ktest    test000025.ptr.err
messages.txt      test000007.kquery     test000014.kquery   test000019.ptr.err  test000026.ktest
run.istats        test000007.ktest      test000014.ktest    test000020.ktest    test000027.ktest
run.stats         test000007.model.err  test000014.ptr.err  test000021.ktest    test000028.ktest
test000001.ktest  test000008.ktest      test000015.ktest    test000022.ktest    test000029.ktest
test000002.ktest  test000009.ktest      test000016.ktest    test000023.ktest    test000030.ktest
test000003.ktest  test000010.ktest      test000017.ktest    test000024.ktest    test000031.ktest
test000004.ktest  test000011.ktest      test000018.ktest    test000025.kquery   warnings.txt
henry@henry:~/Documents/test/test_klee/klee-out-2$ ktest-tool test000005.ktest
ktest file : 'test000005.ktest'
args       : ['test.bc']
num objects: 1
object 0: name: 'input_buffer'
object 0: size: 16
object 0: data: b'\xff\xff\xff\xff\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff'
object 0: hex : 0xffffffff00ffffffffffffffffffffff
object 0: text: ................
henry@henry:~/Documents/test/test_klee/klee-out-2$ ktest-tool test000006.ktest
ktest file : 'test000006.ktest'
args       : ['test.bc']
num objects: 1
object 0: name: 'input_buffer'
object 0: size: 16
object 0: data: b'\xff\xff\xff\xff\xff\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff'
object 0: hex : 0xffffffffff00ffffffffffffffffffff
object 0: text: ................
henry@henry:~/Documents/test/test_klee/klee-out-2$ ktest-tool test000007.ktest
ktest file : 'test000007.ktest'
args       : ['test.bc']
num objects: 1
object 0: name: 'input_buffer'
object 0: size: 16
object 0: data: b'F\x01\xff\xff\xff\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff'
object 0: hex : 0x4601ffffff00ffffffffffffffffffff
object 0: text: F...............

随便使用其中一个崩溃示例用来做测试，部分代码修改如下

// klee_make_symbolic(input_buffer, sizeof(input_buffer),"input_buffer");
char* message_data = get_message('\xff\xff\xff\xff\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff');