前言

符号执行是一种程序分析技术,使用抽象符号作为程序输入,可以探索程序的每个路径并输出结果,能够做到有效的发现程序中的漏洞.

在运行时所有对输入符号的运算操作会转化为数学表达式进行求解,对符号表达式求解时确认问题可解将会生成新的状态叉,其结构类似二叉树,但又有所不同,也可以把状态叉简单的理解为程序路径,在对非符号化的数值进行运算时会使用引擎内部的指令进行实际运算.

当符号执行时每发现一个程序问题都会终止这个存在问题的状态叉并生成测试用例,只要把测试用例输入回程序就可以复现这个问题并进行调试分析,当有多个问题出现在同一代码位置时,通常只会生成一个测试用例,在这里就不对符号执行技术进行深入介绍了,在本文中使用的符号执行引擎是经过笔者自己修改的,原本的引擎不支持命令注入检测,本来打算直接把代码提交到官方仓库,但无奈官方的代码审核速度实在感人,后面可能会上传到自己的仓库.

操作系统: ubuntu20.04

目标软件: CImg-v.2.3.4

目标CVE编号: CVE-2019-1010174

符号执行引擎: klee

使用wllvm编译CImg开源库:

1.进入源码目录

cd CImg-v.2.3.4/examples/

2.修改makefile

makefile86行加入:

export LLVM_COMPILER=clang

CC=wllvm

CXX=wllvm++

在这里把wllvm指向的编译器为clang,然后把CC和CXX指向的编译器设置为wllvm,这样就可以把整个程序编译为llvm的.bc文件了,后面把.bc文件给符号执行引擎进行漏洞挖掘.

cflags选项加入以下参数:

-g -O0

3.进行编译

使用以下命令:

make linux

4.使用wllvm的extract-bc脚本提取.bc文件

find . -executable -type f | xargs -I '{}' extract-bc '{}'  

提取的.bc文件如下:

use_draw_gradient是被测试的目标程序.

使用klee进行漏洞挖掘:

1.启动klee

klee -search=dfs --libc=uclibc --posix-runtime -check-command-inject use_draw_gradient.bc -i -sym-arg 10

命令选项解释如下:

-search 指定路径搜索算法

--libc 指定linux c标准库

--posix-runtime 链接posix库 其作用是支持参数、文件等内容符号化

-check-command-inject 开启命令注入检测功能

-sym-arg 符号化参数内容

2.检查klee运行结果

在klee运行半个小时后出现错误提示,在CImg.h文件第4874行可能出现命令注入.

3.查看生成的测试用例

测试用例会生成在klee-last目录下,在这里有两个测试用例,命令注入是第二个.

4.查看测试用例堆栈信息以及触发位置:

5.查看命令注入触发位置:

位置已经确认无误

6.使用ktest-tool查看测试用例中的符号信息

由于启动时符号化了-i选项指定的路径,那么路径就会被符号化,它的符号名称为arg00,对符号求解后的具体值在这里可以看到,由于输入的是路径参数,那么text属性的内容就是求解后的具体数值了,也就是说只要把HTTP://H作为输入就可以到达漏洞位置.

符号执行不但能够挖掘一般的内存错误,还能够挖掘命令注入、格式化字符串,只要是和内存相关的问题都可以挖,并且获得的错误信息很充足,可以很直观的知道错误的类型、位置、堆栈信息,到此所有内容就结束了,顺便说一下,如果大家有想要的符号执行功能或者想让klee添加一些新的功能并开源给大家使用可以发私信联系我,在结尾祝大家明天除夕快乐,希望新的一年里大家虎虎生威,也希望自己能够继续多整一些新的发明,展示一些新的绝活.

参考资料:

https://klee.github.io/tutorials/

【公告】欢迎大家踊跃尝试高研班11月试题，挑战自己的极限！