具体示例如下，其中输入x未知，即符号：

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

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

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

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

在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，以及最近在工作中使用拼写编写的模糊卫星控制程序的工具。

原文来自：

本文地址：//q13zd.cn/klee-symbol-execution-engine.html编辑：王婷，审核员：逄增宝

Linux大全：

Linux系统大全：

红帽认证RHCE考试心得：