共计 1672 个字符，预计需要花费 5 分钟才能阅读完成。
| 导读 | 将符号执行应用于任意真实程序很难，你通常必须对执行环境建模，并找到有效的方法来应对不确定性和路径爆炸。动态符号执行的想法是在任何输入上执行一个软件，同时探索所有可能的执行路径，而无需指定具体值。 |
具体示例如下，其中输入 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，以及最近在工作中使用拼写编写的模糊卫星控制程序的工具。
