动态性符号执行的念头是在一切键入上执行一个软件，与此同时探索全部有可能的执行路径，而不用特定实际值。具体实例如下所示，在其中键入x不明，即标记：
符号执行在全部三个执行路径(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检测tcp协议
在2007年，我一直勤奋寻找的科学研究毕业论文，直到碰到Cristian Cadar的毕业论文“EXE: Automatically Generating Inputs of Death“EXE: Automatically Generating Inputs of Death”。遭受符号执行观念的启迪，在将传到的互联网数据传输到网络堆栈以前，可以标识它的协议书报头吗?是我想的太多，我能用这类技术性寻找协议书标准和完成系统漏洞吗?
因此科研工作人员写了一封电子邮件给Cristian Cadar，并快速收到了回应。并且，Cristian和Daniel Dunbar慷慨大方地为它推送了KLEE的源码，这也是她们已经应用的新专用工具，现阶段还并未向外发布。
下面我拓展了KLEE以执行互相通讯的好几个tcp协议。我将此技术性用以检测无线传感器，并在我的IPSN 2010毕业论文中表述的Contiki OS中看到了2个有意思的系统漏洞。在其中一个造成了TCP/IP局部变量内的感应器连接点的死锁，必须再次设定硬件配置，这是在无线传感器布署中留意到的真真正正系统漏洞。死锁就是指两种或两个以上的进度在执行全过程中，因为市场竞争資源或是因为彼此之间通讯而产生的一种堵塞的状况，如果没有外力，他们都将没法推动下来。这时称系统软件处在死锁情况或系统软件造成了死锁，这种始终在相互之间等候的过程称之为死锁过程。
自2015年至今，我一直沒有太多应用过KLEE，而且想再度试着一下。与此同时，Contiki OS已拷到Contiki-NG。我拷贝了储存库，并将称之为20-packet-parsing的功能测试编译程序为LLVM位码。在功能测试中，我应用KLEE的klee_make_symbolic函数公式标识了检测数据缓冲区域(〜1KB)的标记。Contiki-NG是一套用以下一代IoT(物联网技术)机器设备的开源系统混合开发电脑操作系统，可适用单独服务器。
在我的旧Mac上运作了数分钟后，KLEE在分析一些协议书的标头时发觉了2个运行内存系统漏洞(表针超出)。我将这种发觉与主要的检测实例一起汇报给Contiki-NG的安全性精英团队，以开展进一步的剖析。对于我而言，这一趣味测试是KLEE依然是有效的探讨和检测实例转化成专用工具的又一个直接证据。
对外开放的试炼和机会
将符号执行运用于随意真正程序流程难以，你通常务必对执行自然环境模型，并寻找有效的办法来解决可变性和路径发生爆炸。 并且，很多路径管束难以处理，可是针对现如今的求得器来讲无法立即处理。
即便如此，科学研究和运用符号执行(应用KLEE)仍会产生很多机遇。你将掌握程序结构，c语言编译器，SAT / SMT求得器，及其怎样撰写其他类型的检测工具。根据这种专业知识，我编辑了模糊不清Android应用软件的专用工具，超级优化LLVM IR，及其近期在工作上应用英语拼写撰写的模糊不清通讯卫星管理程序的专用工具。
文中翻譯自：https://sasnauskas.eu/finding-software-bugs-using-symbolic-execution/