![]()
本文为看雪论坛优秀文章
看雪论坛作者ID：来杯柠檬红茶
符号执行是一种程序分析技术，使用抽象符号作为程序输入，可以探索程序的每个路径并输出结果，能够做到有效的发现程序中的漏洞。在运行时所有对输入符号的运算操作会转化为数学表达式进行求解，对符号表达式求解时确认问题可解将会生成新的状态叉，其结构类似二叉树，但又有所不同，也可以把状态叉简单的理解为程序路径，在对非符号化的数值进行运算时会使用引擎内部的指令进行实际运算。
当符号执行时每发现一个程序问题都会终止这个存在问题的状态叉并生成测试用例，只要把测试用例输入回程序就可以复现这个问题并进行调试分析，当有多个问题出现在同一代码位置时，通常只会生成一个测试用例，在这里就不对符号执行技术进行深入介绍了。在本文中使用的符号执行引擎是经过笔者自己修改的，原本的引擎不支持命令注入检测，本来打算直接把代码提交到官方仓库，但无奈官方的代码审核速度实在感人，后面可能会上传到自己的仓库。目标CVE编号: CVE-2019-10101741.进入源码目录
cd CImg-v.2.3.4/examples/2.修改makefile
export LLVM_COMPILER=clang在这里把wllvm指向的编译器为clang，然后把CC和CXX指向的编译器设置为wllvm，这样就可以把整个程序编译为llvm的.bc文件了，后面把.bc文件给符号执行引擎进行漏洞挖掘。3.进行编译
4.使用wllvm的extract-bc脚本提取.bc文件
find . -executable -type f | xargs -I '{}' extract-bc '{}' use_draw_gradient是被测试的目标程序。1.启动klee
klee -search=dfs --libc=uclibc --posix-runtime -check-command-inject use_draw_gradient.bc -i -sym-arg 10--posix-runtime 链接posix库 其作用是支持参数、文件等内容符号化-check-command-inject 开启命令注入检测功能2.检查klee运行结果
在klee运行半个小时后出现错误提示,在CImg.h文件第4874行可能出现命令注入。3.查看生成的测试用例
测试用例会生成在klee-last目录下,在这里有两个测试用例,命令注入是第二个。4.查看测试用例堆栈信息以及触发位置
5.查看命令注入触发位置
6.使用ktest-tool查看测试用例中的符号信息
由于启动时符号化了-i选项指定的路径，那么路径就会被符号化，它的符号名称为arg00，对符号求解后的具体值在这里可以看到，由于输入的是路径参数，那么text属性的内容就是求解后的具体数值了，也就是说只要把HTTP://H作为输入就可以到达漏洞位置。符号执行不但能够挖掘一般的内存错误，还能够挖掘命令注入、格式化字符串，只要是和内存相关的问题都可以挖，符号化参数功能能够很好的解决fuzz工具无法对程序参数进行fuzz的问题。根据笔者对开源库的持续探索，发现很多开源库在参数这一块经常出现栈溢出或格式化字符串漏洞，符号执行主要是获得的错误信息很充足，可以很直观的知道错误的类型、位置、堆栈信息，到此所有内容就结束了。顺便说一下，如果大家有想要的符号执行功能或者想让klee添加一些新的功能并开源给大家使用可以发私信联系我。https://klee.github.io/tutorials/看雪ID：来杯柠檬红茶
https://bbs.pediy.com/user-home-763252.htm
*本文由看雪论坛 来杯柠檬红茶 原创，转载请注明来自看雪社区
文章来源: http://mp.weixin.qq.com/s?__biz=MjM5NTc2MDYxMw==&mid=2458430155&idx=1&sn=43a5ad56c413f82139ce389985bb19db&chksm=b18f9a4186f81357d4adf46cd0dd5d56ea2e67cadbd9c4f0ec5d0b2e69a1044e970624328a50#rd
如有侵权请联系:admin#unsafe.sh