利用 KLEE 符号执行引擎挖掘软件漏洞
2021-04-21 11:00:00 Author: www.4hou.com(查看原文) 阅读量:157 收藏

动态符号执行的想法是在任何输入上执行一个软件,同时探索所有可能的执行路径,而无需指定具体值。具体示例如下,其中输入x未知,即符号:

微信截图_20201226154806.png

符号执行在所有三个执行路径(x < 0, x > 100, 0 < = x < =100)并生成三个具体的测试用例:x=-1, x=101和x=23在击中断言之后。

你不再需要手动编写测试用例,你会沿执行路径捕获断言失败和内存安全漏洞。以上说的可不是理论层面上的事情,哪这种方法可以在实践中用于实际程序吗?

KLEE

KLEE是一个符号执行引擎,可对任何输入执行未修改的真实程序。你将程序编译为LLVM位码,将某些输入标记为符号,然后启动KLEE。 KLEE使用约束解决方案探索可能的执行路径,并为每个路径生成具体的测试用例。如果发生漏洞,你可以使用触发它的输入来重播程序。

2019年11月,关于KLEE的OSDI 2008开创性论文被选入ACM SIGOPS名人堂。在过去的十年里,KLEE的研究和应用产生了超过150篇科学出版物、数十篇博士论文、研究资助、工具和安全初创公司。

使用KLEE测试网络协议

在2007年,我一直努力寻找自己的研究论文,直到遇到Cristian Cadar的论文“EXE: Automatically Generating Inputs of Death“EXE: Automatically Generating Inputs of Death”。受到符号执行思想的启发,在将传入的网络数据包传递到网络堆栈之前,可以标记它的协议报头吗?如果是这样,我可以用这种技术找到协议规范和实现漏洞吗?

于是研究人员写了一封电子邮件给Cristian Cadar,并迅速收到了答复。而且,Cristian和Daniel Dunbar慷慨地向它发送了KLEE的源代码,这是他们正在使用的新工具,目前还尚未对外公布。

接下来我扩展了KLEE以执行相互通信的多个协议栈。我将此技术用于测试传感器网络,并在我的IPSN 2010论文中描述的Contiki OS中发现了两个有趣的漏洞。其中一个导致了TCP/IP堆栈内的传感器节点的死锁,需要重新设置硬件,这是在传感器网络部署中观察到的真正漏洞。死锁是指两个或两个以上的进程在执行过程中,由于竞争资源或者由于彼此通信而造成的一种阻塞的现象,若无外力作用,它们都将无法推进下去。此时称系统处于死锁状态或系统产生了死锁,这些永远在互相等待的进程称为死锁进程。

自2015年以来,我一直没有过多使用过KLEE,并且想再次尝试一下。同时,Contiki OS已拷贝到Contiki-NG。我复制了存储库,并将称为20-packet-parsing的测试用例编译为LLVM位码。在测试用例中,我使用KLEE的klee_make_symbolic函数标记了测试数据包缓冲区(〜1KB)的符号。Contiki-NG是一套用于下一代IoT(物联网)设备的开源跨平台操作系统,可适用于独立高防服务器。

在我的旧Mac上运行了几分钟后,KLEE在解析某些协议的标头时发现了两个内存漏洞(指针超出范围)。我将这些发现与具体的测试案例一起报告给Contiki-NG的安全团队,以进行进一步的分析。对我来说,这个小测试是KLEE仍然是有用的研究和测试案例生成工具的又一个证据。

开放的挑战和机遇

将符号执行应用于任意真实程序很难,你通常必须对执行环境建模,并找到有效的方法来应对不确定性和路径爆炸。 而且,许多路径约束很难解决,但是对于当今的求解器而言难以及时解决。

尽管如此,研究和应用符号执行(使用KLEE)仍会带来许多机会。你将了解程序结构,编译器,SAT / SMT求解器,以及如何编写其他类型的测试工具。基于这些知识,我编写了模糊Android应用程序的工具,超级优化LLVM IR,以及最近在工作中使用拼写编写的模糊卫星控制程序的工具。

本文翻译自:https://sasnauskas.eu/finding-software-bugs-using-symbolic-execution/如若转载,请注明原文地址:


文章来源: https://www.4hou.com/posts/OL7L
如有侵权请联系:admin#unsafe.sh