博客

看了网上的一个klee教程，来源于：https://adalogics.com/blog/symbolic-execution-with-klee

在此记录。

global-buffer-overflow

测试代码：

#include<stdio.h>
#include<stdlib.h>
#include<string.h>
int global_arr[10] = {0,1,2,3,4,5,6,7,8,9};
int test1(char * buf)
{
	int i = 5;
	if (strcmp(buf,"BUG!") == 0)
	{
		i += 20;
	}
	return global_arr[i];
}
int main(int argc,char ** argv)
{
	char arr[10];
	klee_make_symbolic(arr,10,"arr");
	klee_assume(arr[9]=='\0');
	test1(arr);
}

clang编译字节码

clang -c -g -emit-llvm uaf.c

klee符号执行

klee --libc=uclibc uaf.bc

显示结果

查看测试样例，可以看到触发了指针越界的是测试样例3，然后查看测试样例3的内容，可以看到触发漏洞的输入为BUG!开头的字符串。

DF

测试代码：

#include<stdio.h>
#include<stdlib.h>
#include<string.h>
int test4(char * buf)
{
	char * var = malloc(10);
	if(strcmp(buf,"bug!")==0)
	{
		free(var);
	}
	free(var);
	return 1;
}
int main(int argc,char ** argv)
{
	char arr[10];
	klee_make_symbolic(arr,10,"arr");
	klee_assume(arr[9]=='\0');
	test4(arr);
}

clang编译字节码

clang -c -g -emit-llvm uaf.c

klee符号执行

klee --libc=uclibc uaf.bc

显示结果

查看触发漏洞的样例，可以发现触发的输入是bug!开头的字符串。

ktest-tool test000003.ktest

还有两个例子的结果也差不多。

就简单列下漏洞代码。

#include<stdio.h>
#include<stdlib.h>
#include<string.h>
int global_arr[10] = {0,1,2,3,4,5,6,7,8,9};
int test2(char * buf)
{
	int * dyn_mem_arr = malloc(sizeof(int)*10);
    int i =5;
	dyn_mem_arr[0] = 0;
	dyn_mem_arr[1] = 1;
	dyn_mem_arr[2] = 2;
	dyn_mem_arr[3] = 3;
	dyn_mem_arr[4] = 4;
	dyn_mem_arr[5] = 5;
	dyn_mem_arr[6] = 6;
	dyn_mem_arr[7] = 7;
	dyn_mem_arr[8] = 8;
	dyn_mem_arr[9] = 9;
	if (strcmp(buf,"BUG!") == 0)
	{
		i += 20;
	}
	int return_value = dyn_mem_arr[i];
	free(dyn_mem_arr);
	return return_value;
}
int main(int argc,char ** argv)
{
	char arr[10];
	klee_make_symbolic(arr,10,"arr");
	klee_assume(arr[9]=='\0');
	test2(arr);
}

另一个空指针解引用的例子：

#include<stdio.h>
#include<stdlib.h>
#include<string.h>
int *global_string[] = {
    "string1",
    "string2",
    "string3",
    NULL
};
int test3(char * buf)
{
	int i = 1;
	if (strcmp(buf,"BUG!") == 0)
	{
		i = 3;
	}
	char c = *(global_string[i]);
	if(c=='s')
		return 0;
    return 1;
}
int main(int argc,char ** argv)
{
	char arr[10];
	klee_make_symbolic(arr,10,"arr");
	klee_assume(arr[9]=='\0');
	test3(arr);
}