使用符号执行查找软件错误

动态符号执行的思想是在任何输入上执行一个软件，在不指定具体值的情况下同时探索所有可能的执行路径，请考虑以下示例，其中输入x是未知的，即符号：

if（x＆lt; 0）{// ...} else if（x＆gt; 100）{// ...} else {断言（＆＃34;不应达到此值！＆＃34;）}}

符号执行在所有三个执行路径（x 100、0 <= x <= 100）上运行此代码，并在命中断言后生成三个具体的测试用例：x = -1，x = 101和x = 23 。

您不再需要手动编写测试用例。您可以沿执行路径捕获断言失败和内存安全错误。好吧，从理论上讲，但是这种方法在实践中是否可以适用？

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

2019年11月，关于KLEE的OSDI 2008开创性论文被选为ACM SIGOPS名人堂。在过去的十年中，KLEE的研究和应用产生了150多种科学出版物，数十种博士学位。这些论文，研究补助金，工具和安全性初创公司。我代表我在KLEE度过了超过五年的生活，并在此过程中学到了很多东西。

在2007年，我一直难以找到自己的研究论文，直到遇到Cristian Cadar的论文“ EXE：自动生成死亡输入”。受符号执行概念的启发，我问自己以下问题：我可以标记一个程序的协议头吗？如果传入的网络数据包在传递到网络堆栈之前是符号性的，如果可以，我是否可以使用这种技术找到协议规范和实现错误？

我写了一封电子邮件给克里斯蒂安·卡达尔（Cristian Cadar），并立即收到了答复。

在接下来的五年博士学位中在旅途中，我扩展了KLEE以执行相互通信的多个协议栈。我将该技术应用于测试传感器网络，并在IPSN 2010论文中描述的Contiki OS中发现了两个有趣的错误，其中一个导致了死锁TCP / IP堆栈中需要硬件重置的传感器节点的数量。这是在传感器网络部署中观察到的真实错误。

自2015年以来，我一直没有积极使用KLEE，并且想再次尝试使用KLEE。同时，Contiki OS已分叉给Contiki-NG，我克隆了repo并将编译成20个数据包的测试用例编译为LLVM位代码在测试用例中，我使用KLEE的klee_make_symbolic函数将测试数据包缓冲区（〜1KB）标记为符号。

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

将符号执行应用于任意现实世界的程序非常困难，您通常必须对执行环境进行建模并找到有效的方法来应对不确定性和路径爆炸问题，而且许多路径约束很难解决但难以及时解决与今天的求解器。

尽管如此，学习和应用符号执行（使用KLEE）仍会带来许多机会。您将学习程序结构，编译器，SAT / SMT求解器以及如何编写其他类型的测试工具。鉴于这一系列知识，我编写了模糊测试工具Android应用程序对LLVM IR进行了超优化，最近又投入使用，这是一种使SPELL编写的卫星控制程序模糊化的工具。

考虑尝试符号执行。如果您是博士学位。的学生并在该领域中努力寻找论文主题，请不要忘记更大的图景并继续努力。