符号执行初探
这篇博客可以说是非常详尽了，里面讲述了如下内容，以下部分是记得一些笔记和理解
符号执行的过程、原理
静态符号执行到动态符号执行的演变
符号执行的优缺点和展望
还附带了很多参考论文去学习
通俗地理解符号执行
符号执行技术是一种白盒的静态分析技术。即分析程序可能的输入需要能够获取到目标源代码的支持。同时，它是静态的，因为并没有实际的执行程序本身，而是分析程序的执行路径。通过路径分析最终到达我们的目标节点(也就是想让程序走到的代码行)，通过这种方式逆向发现了输入向量。如果把结果条件更改为漏洞条件，理论上也是能够进行漏洞挖掘了。
对于如何根据最终得到的结果求解输入向量，已经有很多现成的数学工具可以使用。上述问题其实可以规约成约束规划的求解问题（更详细的介绍看这里： Constraint_programming ）。比较著名的工具比如SMT（Satisfiability Modulo Theory，可满足性模理论）和SAT。 其实这个概念我是知道的，更简单的例子就是Z3，或者是解方程，约束规划的求解只是更专业的说法了
但是在实际的漏洞分析过程中，目标程序可能更加复杂，没有我们上面的例子这么简单。实际的程序中，可能包含了与外设交互的系统函数，而这些系统函数的输入输出并不会直接赋值到符号中，从而阻断了此类问题的求解。 
这个地方其实也很好理解，符号执行是在当前程序中进行路径分析、扩展，但是突然的系统调用函数，我们又不能跟进系统调用的过程进入看变量变化，这就导致中间的变量变化是未知的，所以导致这些系统函数的输入输出并不会直接赋值到符号中，就会影响符号执行的过程
从公式原理上理解符号执行
符号执行的关键思想就是，把输入变为符号值，那么程序计算的输出值就是一个符号输入值的函数。也就是说把具体的值抽象成符号
为了形式化地完成这个任务，符号执行会在全局维护两个变量。其一是符号状态 σ，它表示的是一个从变量到符号表达式的映射。其二是符号化路径约束PC（或者叫路径条件），这是一个==无量词的一阶公式==，用来表示路径条件。在符号执行的开始，符号状态 σ 会先初始化为一个空的映射，而符号化路径约束PC初始化为true。 σ 和PC在符号执行的过程中会不断更新。在符号执行结束时，PC就会用约束求解器进行求解，以生成实际的输入值。这个实际的输入值如果用程序执行，就会走符号执行过程中探索的那条路径，即此时PC的公式所表示的路径。
再简单的理解就是要记住符号状态和符号化路径约束这两个关键名词，符号状态就是一个变量到符号表达式的映射，符号化路径约束由一些逻辑表达式组成
静态符号执行的缺陷
当我们遇到了循环和递归应该怎么办呢？如果循环或递归的终止条件是符号化的，包含循环和递归的符号执行会导致无限数量的路径。比如上面代码中这个例子，这段代码就有无数条执行路径，每条路径的可能性有两种：要么是任意数量的true加上一个false结尾，要么是无穷多数量的true。我们形式化地表示包含n个true条件和1个false条件的路径
其实这就是符号执行面临的问题之一，即如何处理循环中的无限多路径。在实际中，有一些方法可以应对，比如对搜索加入限制，要么是限制搜索时间的长短，要么是限制路径数量、循环迭代次数、探索深度等等。
void testme_inf() {
int sum = 0;
int N = sym_input();
while (N > 0) {
sum = sum + N
N = sym_input();
}
}
还需要考虑到的一个问题就是，如果符号路径约束包含不能由求解器高效求解的公式怎么办？比如说，如果原本的代码发生变化，把twice函数替换为下述语句：
int twice(int v) {
return (v*v) % 50;
}
其实我们上述介绍的内容，应该属于纯粹的静态符号执行的范畴。我们提出的两个问题，是导致静态符号执行不能够实用的原因之一。符号执行的概念早在1975年[4]就提出了，但是符号执行技术真正得到实用，却是在一种方式提出之后，即混合实际执行和符号执行，称为concolic execution，是真正意义上的动态符号执行。
动态符号执行 Concolic Execution
Concolic执行维护一个实际状态(concrete state)和一个符号化状态(symbolic state)：实际状态将所有变量映射到实际值，符号状态只映射那些有非实际值的变量。Concolic执行首先用一些给定的或者随机的输入来执行程序，收集执行过程中条件语句对输入的符号化约束，然后使用约束求解器去推理输入的变化，从而将下一次程序的执行导向另一条执行路径。简单地说来，就是在已有实际输入得到的路径上，对分支路径条件进行取反，就可以让执行走向另外一条路径。这个过程会不断地重复，加上系统化或启发式的路径选择算法，直到所有的路径都被探索，或者用户定义的覆盖目标达到，或者时间开销超过预计。
PS：注意在这个搜索过程中，其实Concolic执行使用了深度优先的搜索策略。也就是说每次产生新的输入Concolic执行都将执行完整个程序，直到程序结束，然后才返回上一个没有测试的路径约束条件，取反约束条件，得到新的输入，进入新的路径。
总的来说，将实际执行与符号执行相结合是一种很好的方法，弥补了静态符号执行的很多缺陷。
EGT本质上还是将实际执行与符号执行相结合，通过路径取反探索所有可能路径。Concolic执行的方法是非常实用的，有效解决了遇到不支持的运算以及应用与外界交互的问题。比如调用库函数和系统调用的情况下，因为库和系统调用无法插桩，所以这些函数相关的返回值会被实际化，以此获得简化的程序约束
面临挑战
1.路径爆炸(Path Explosion)
2.约束求解(Constraint Solving)
3.内存建模(Memory Modeling)
4.处理并发(Handling Concurrency)
发展脉络(至2017)
本节仍然摘录自r1ce的文章，主要是以时间的顺序梳理符号执行技术的发展脉络，同时对值得关注的项目和论文做一个小小总结和推荐。
符号执行最初提出是在70年代中期，主要描述的是静态符合执行的原理，到了2005年左右突然开始重新流行，是因为引入了一些新的技术让符号执行更加实用。Concolic执行的提出让符号执行真正成为可实用的程序分析技术，并且大量用于软件测试、逆向工程等领域。在2005年作用涌现出很多工作，如DART[5]、CUTE[6]、EGT/EXE[7]、CREST[8]等等，但真正值得关注和细读的，应该是2008年Cristian Cadar开发的KLEE[3]。KLEE可以说是源代码符号执行的经典作品，又是开源的，后来的许多优秀的符号执行工具都是建立在KLEE的基础上，因此我认为研究符号执行，KLEE的文章是必读的。
基于二进制的符号执行工具则是2009年EPFL的George Candea团队开发的S2E[9]最为著名，其开创了选择符号执行这种方式。2012年CMU的David Brumley团队提出的Mayhem[10]则采用了混合offline和online的执行方式。2008年UC Berkeldy的Dawn Song团队提出的BitBlaze[11]二进制分析平台中的Rudder模块使用了online的执行方式，也值得一看。总之，基于二进制的符号执行工作了解这三个就足够了。其中，S2E有开源的一个版本，非常值得仔细研究。最近比较火的angr[12]，是一个基于Python实现的二进制分析平台，完全开源且还在不断更新，其中也实现了多种不同的符号执行策略。
在优化技术上，近几年的两个工作比较值得一看其一是2014年David Brumley团队提出的路径融合方法，叫做Veritesting[13]，是比较重要的工作之一，angr中也实现了这种符号执行方式。另一个是2015年Stanford的Dawson Engler（这可是Cristian Cadar的老师）团队提出的Under-Constrained Symbolic Execution[14]。
另外，近年流行的符号执行与fuzzing技术相结合以提升挖掘漏洞效率，其实早在DART和2012年微软的SAGE[15]工作中就已经有用到这种思想，但这两年真正火起来是2016年UCSB的Shellphish团队发表的Driller[16]论文，称作符号辅助的fuzzing（symbolic-assisted fuzzing），也非常值得一看。
总结
符号执行已是一种有效的程序测试技术，它提供了一种自动生成"触发软件错误的输入"的方法，这些错误从底层程序崩溃到高层语义特性不等。符号执行技术可以用于测试例的自动生成，也可以用于源代码安全性的检测。这两项工作的成效都十分依赖于约束求解器的性能，同时还受硬件设备处理能力的影响。
虽然需要更多的研究来提高符号执行的代码覆盖率，测试精度，分析效率等等指标，但是事实证明，现有工具可以有效地测试和发现各种软件中的错误，从低级网络和操作系统代码到高级应用程序代码，不一而足。
从实用性的角度来说：
（2018年）现有的符号执行工具，在开源方面，主要还是基于KLEE项目的。可见对于KLEE项目的深入理解，将有助于我们打造更加高效的工具。有了高效的工具，就能够使得我们一边学习理论，一遍验证，从而走上高速公路。Inception工具是就ARM架构，而对于路由器中常使用的MIPS架构，现在应该还尚未有类似的符号执行工具发布（如果已经由类似工具，欢迎读者留言）。其中，基于IDA的脚本工具bugscam，经过揭秘路由器0DAY漏洞的作者修改之后，也能够支持分析MIPS架构的漏洞了。然而，其误报率非常之高，该工具报告的漏洞基本都不可用。因此，如何基于上述符号执行的思想，结合IDA工具中强大的反汇编能力，开发也具有符号执行功能的MIPS架构漏洞分析工具，相信也是非常有价值的。
To Learn More
摘自r1ce的文章：
对于符号执行入门，有两篇文章可以参考。其一是2010年David Brumley团队在S&P会议上发表的《All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)》[1]。这篇文章同时介绍了动态污点分析和前向符号执行的基本概念，作者构造了一种简化的中间语言，用来形式化地描述这两种程序分析技术的根本原理。其二是2011年Cristian Cadar发表在ACM通讯上的一篇短文《Symbolic execution for software testing: three decades later》[2]，以较为通俗的语言和简单的例子阐述了符号执行的基本原理，并介绍了符号执行技术的发展历程和面临挑战。
其实这两篇文章的作者都是二进制分析领域大名鼎鼎的人物，卡内基梅隆的David Brumley是AEG的提出者，其带领团队是DARPA CGC比赛的第一名；英国帝国理工的Cristian Cadar则是符号执行引擎KLEE[3]的作者——KLEE在符号执行领域的地位不言而喻。这两篇文章各有千秋：前者更加学术化一些，用中间语言进行的形式化描述有些晦涩难懂，但对于进一步研究符号执行引擎的源码很有帮助；后者则更通俗一些，有助于初学者的理解，且对于符号执行的发展脉络有更多的介绍。
参考文章
K0rz3n：https://www.k0rz3n.com/2019/02/28/简单理解符号执行技术/
r1ce：https://zhuanlan.zhihu.com/p/26927127
符号执行——从入门到上高速：https://www.anquanke.com/post/id/157928
http://pwn4.fun/2017/03/20/ 符号执行基础/
[2]* Symbolic execution for software testing: three decades later：https://people.eecs.berkeley.edu/~ksen/papers/cacm13.pdf
[1] Schwartz E J, Avgerinos T, Brumley D. All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask) [C]// Security & Privacy. DBLP, 2010:317-331.
[2] Cadar C, Sen K. Symbolic execution for software testing: three decades later[M]. ACM, 2013.
[3] C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI’08), volume 8, pages 209–224, 2008.
[4] R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT – a formal system for testing and debugging programs by symbolic execution. SIGPLAN Not., 10:234–245, 1975.
[5] P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In PLDI’05, June 2005.
[6] K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In ESEC/FSE’05, Sep 2005.
[7] C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically Generating Inputs of Death. In Proceedings of the 13th ACM Conference on Computer and Communications Security, pages 322–335, 2006.
[8] J. Burnim and K.Sen,“Heuristics for scalable dynamic test generation,” in Proc. 23rd IEEE/ACM Int. Conf. Autom. Software Engin., 2008, pp. 443–446.
[9] V. Chipounov, V. Georgescu, C. Zamfir, and G. Candea. Selective Symbolic Execution. In Proceedings of the 5th Workshop on Hot Topics in System Dependability, 2009.
[10] S. K. Cha, T. Avgerinos, A. Rebert, and D. Brumley. Unleashing Mayhem on Binary Code. In Proceedings of the IEEE Symposium on Security and Privacy, pages 380–394, 2012.
[11] Song D, Brumley D, Yin H, et al. BitBlaze: A New Approach to Computer Security via Binary Analysis[C]// Information Systems Security, International Conference, Iciss 2008, Hyderabad, India, December 16-20, 2008. Proceedings. DBLP, 2008:1-25.
[12] Yan S, Wang R, Salls C, et al. SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis[C]// Security and Privacy. IEEE, 2016:138-157.
[13] T. Avgerinos, A. Rebert, S. K. Cha, and D. Brumley. Enhancing Symbolic Execution with Veritesting. pages 1083–1094, 2014.
[14] D. a. Ramos and D. Engler. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In Proceedings of the 24th USENIX Security Symposium, pages 49–64, 2015.
[15] P. Godefroid, M. Y. Levin, and D. Molnar. SAGE: Whitebox Fuzzing for Security Testing. ACM Queue, 10(1):20, 2012.
[16] N. Stephens, J. Grosen, C. Salls, A. Dutcher, R. Wang, J. Corbetta, Y. Shoshitaishvili, C. Kruegel, and G. Vigna. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In Proceedings of the Network and Distributed System Security Symposium, 2016.