原文 A Survey of Symbolic Execution Techniques
目录
2.4 回溯符号执行 Symbolic Backward Execution
重用约束的解。Reuse of Constraint Solutions.
处理不确定的约束。Handling Problematic Constraints.
7.1 分割逻辑 separation logic (SL)
1. 介绍
1.1 例子
一个状态表示 state (stmt, σ, π)
stmt 语句
σ 符号表达式：存储变量的表达式，具体的和符号化的都有
π 约束关系：执行到该语句需要满足的条件
void foobar(int a, int b) {
int x = 1, y = 0;
if (a != 0) {
y = 3+x;
if (b == 0)
x = 2*(a+b);
}
assert(x-y != 0);
}
符号执行树
1.2 挑战
内存：符号执行引擎怎样处理复杂的结构？可能对符号存储数据和符号表达式描述的地址造成风险
环境和第三方组件：调用库函数…
状态空间爆炸：比如循环…
约束求解：SMT(satisfiability modulo theories)求解器可以扩展到数百个变量的复杂约束组合。 然而，诸如非线性算术(比如乘法)之类的构造成为效率的主要障碍。
对二进制代码的分析：
1.3 相关工作
符号执行一直是学术界关注的焦点。截至2017年8月，谷歌学术中找到标题包括“符号执行”一词的有742篇文章。
其他技术综述：自动测试用例生成
1.4 文章的组织
2. 符号执行引擎
在这一节中我们介绍了符号执行的一些重要的设计原则，和执行过程中的关键折衷。从具体化和符号化的概念出发，介绍了混合执行的思想。
2.1 混合符号和具体执行
混合符号执行
符号执行理论上可以产生所有可能的控制流路径，实际上这通常是不可能的，特别是在真实的软件环境中。复杂的应用程序通常建立在非常复杂的软件栈之上。一个符号执行引擎静态地分析整个堆栈，在执行过程中准确评估任何可能的副作用是相当具有挑战性的。在这种情况下出现的一些问题，用第1.1节纯粹符号化的方法很难做到这几点：
1. 对外部库调用的彻底探索可能导致状态的指数爆炸，从而妨碍分析到达感兴趣的代码部分。
2. 对外部第三方组件的调用可能无法由执行器跟踪。
3. 符号引擎在分析过程中不断调用SMT求解器。在约束求解中花费的时间是引擎的主要性能障碍之一，程序可能会产生约束，即使是强大的求解器也不能很好地处理。
解决上述问题并使符号执行在实践中可行的一个基本思想是将具体和象征性的执行混合起来。
动态符号执行。。。。。。。。。。。。。。。。。。。。。。。。
有选择的符号执行。。。。。。。。。。。。。。。。。。。。。。
搜索策略：深度优先 generational search
假阴性（即，错过的路径）和路径偏差是动态符号执行的显着缺点。
在concolic执行过程中，外部调用，异常，类型转换和符号指针是关键方面，必须由引擎仔细处理以减少路径偏差的数量。
2.2 符号执行的设计原则
1. 处理：程序应能在不超过给定资源的情况下进行任意长时间的工作。由于庞大数量的控制流路径,内存消耗是特别关键的问题。
2. 避免重复工作：不应该重复执行工作，避免为分析可能有共同前置的不同路径,从一开始就多次重启一个程序。
3. 分析结果重用：以前运行的分析结果应该尽可能地重复使用。特别是，应避免调用昂贵的SMT求解器来求解之前解决过的路径约束。
2.3 路径选择
DFS:占用内存更小，受到包含循环和递归调用的路径的阻碍
BFS:占用内存更大，能快速的遍历早期行为，需要更长时间完成特定路径的探索
下面是几个启发式搜索：
最大覆盖率:
最短距离:与程序中特定点的距离
buggy-path优先策略:
loop exhaustion策略:探索访问循环的路径,很多溢出和内存错误由循环引起
利用FSM(Finite State Machine, 有限状态机): [Zhang et al., 2015]提出了一种动态符号执行的新方法，以自动找到一个满足规则属性的程序路径，即一个可以由FSM表示的属性（例如文件使用或内存安全性）。动态符号执行由FSM引导，以便首先探索最有可能满足属性的执行路径的分支。该方法利用静态和动态分析来计算将被选择用于探索的路径的优先级：在符号执行期间动态地计算当前执行路径已经到达的FSM的状态，并静态分析向后的数据流被用于计算未来状态。如果这两个集合的交集非空，则可能有满足该属性的路径。
Fitness function：衡量探索路径到达目标测试覆盖的距离，优先考虑可能更接近特定分支的路径。例如目标分支|a-c|==0，路径的接近度被定义为|a-c|，越小越接近。
2.4 回溯符号执行 Symbolic Backward Execution
从目标点回溯到程序的入口点。
SBE和CCBSE中逆向探索的一个关键要求是程序间控制流程图的可用性，需要提供了一个完整的程序控制流程。比如C++中的成员函数的被调用关系，怎么回溯？
反向收集约束时，可能会出现一些实际的优点（第6章）。
3. 内存模型
3.1 完全符号化内存
3.2 地址具体化
分析的复杂性爆炸时，很难把指针变量限制到足够小的范围内。给指针变量一个具体的值，是流行的方案。但是会造成分析引擎错过一些路径。
3.3 部分内存建模
为了缓解完全符号化的可测性问题(3.1)和具体化后完整性的丢失(3.2)。
部分内存模型关键点：写总是具体化 ; 读时，如果假定的可能值的连续区间足够小，读就被符号化。
Mayhem、Angr
3.4 延迟初始化
针对面向对象的高级语言。变量被首次访问时才初始化。
4. 与环境和第三方组件的交互
文件系统，环境变量，网络，第三方闭源组件和流行框架 ，符号执行必须考虑周围的整个软件堆栈，包括系统库，内核和驱动程序。
5. 路径爆炸
5.1 裁剪不可达路径
5.2 函数和循环摘要
早期只能通过循环来生成摘要，循环通过向迭代中添加一个固定数量来更新符号变量。而且，它们不能处理嵌套循环或多路径循环，即在其体内具有分支的循环。 Proteus 是一个总结多路径循环的总体框架。它根据路径条件中值变化的模式（即是否更新了一个归纳变量）和循环内路径的交错（即是否有规律性）对循环进行分类。分类利用控制流图的扩展形式，然后用于构建对交织进行建模的自动机。自动机以深度优先的方式遍历，并为其中所有可行的轨迹构建了分离的汇总，其中轨迹表示循环中的执行。分类确定是否可以精确地或近似地捕获一个循环（这仍然是实际相关的）。对具有不规则模式或非归纳更新的多路径循环进行精确的总结，更重要的是对嵌套循环的总结仍然是一个开放的研究问题。
对控制流程图中循环路径的分析，产生模板，该模板将一部分代码生成的程序状态描述为紧凑符号执行树。 通过利用模板，符号执行引擎可以探索大量减少的程序状态。 这种方法的缺点是可能会显着增加约束求解器的负担。
5.3 路径归并与等价
探索相似性路径，丢弃不能导致新发现的路径，在有利的时候将差异抽象出来。
插值
无限循环的处理
后置符号执行
路径分割 ：有些路径等价
5.4 约束下的符号执行
受约束的变量与经典的完全约束的符号变量具有相同的语义，除非在可能产生错误的表达式中使用。
虽然这种技术不够完善，可能会错过错误，但它仍然可以扩展到在更大的程序中找到bug。
5.5 利用预置条件和输入特性
预处理符号执行：在初始化时向π添加更多的约束。状态空间变小了，但在每个分支的检测增多了
循环扩展符号执行[Saxena 2009]
5.6 状态合并
例子中利用ite表达式合并状态
是否需要合并？
启发式状态合并、动态状态合并
5.7 利用程序分析和优化技术
程序分片：这种分析从程序行为的一个子集开始，从程序中提取忠实地表示该行为的最小指令序列
污点分析
Fuzzing：和符号执行相互结合
分支预测：
类型校验：
编译器优化：符号执行几个要素：程序优化、搜索启发式、状态合并、约束求解优化。
编译器优化对约束生成和路径探索的影响，研究很少，是一个开放性的问题。
6. 约束求解
是否存在一组变量赋值，使問題为可满足。
确定是否有一个解,使符号化的公式为真。
Although SAT is a well-known NP-complete problem, recent advances have moved the boundaries for what is intractable when it comes to practical applications.
虽然SAT(Boolean Satisfiability Problem)是一个著名的NP完全问题，但在实际应用中，最新进展已使难以解决的问题发生了变化。
观察表明一些问题用更自然的语言来描述比具有逻辑连接词的布尔公式更具表现力。 因此，SMT将SAT问题推广到支持理论，以捕获涉及例如线性算术和阵列上的运算的公式。 SMT求解器将SMT公式中的原子映射到新的布尔变量：SAT决策程序检查重写的公式的可满足性，理论求解器检查由SAT程序生成的模型。
SMT求解器有几个独特的优势。它们的核心算法是通用的，可以处理许多单独约束的复杂组合。当添加或删除约束时，它们可以逐步工作和回溯，并提供对不一致性的解释。可以以任意方式添加和组合理论，例如，对字符串数组进行推理。决策过程不需要单独进行：通常，它们是结合在一起的，以减少在较重的任务中的时间开销，例如，首先用非线性算术公式求解线性部分。不完整的程序也很有价值：只有在无法给出结论性答案的情况下，完整而昂贵的程序才能被调用。所有这些因素都允许SMT求解器解决没有单个程序可以孤立解决的大问题。
在符号执行器中，约束求解在检查路径的可行性、生成符号变量的赋值以及验证断言方面起着关键的作用。多年来，符号执行器采用了不同的求解器，这取决于所支持的理论和当时的相对性能。
然而，尽管过去几年取得了重大的进展 - 这也使符号执行成为现实，但约束求解仍然是符号执行引擎可扩展性的主要障碍之一，也阻碍了在involve expensive theories（例如，非线性算术）或不透明的库调用的约束下的可行性。
在本节的其余部分中，我们将讨论不同的技术来扩展符号处理所能处理的程序的范围，并优化约束求解的性能。突出的方法包括：（i）降低约束的规模和复杂性，（ii）公开的一些方法，例如，使用约束求解缓存，延迟约束求解器的查询，或具体化，（iii）增加符号执行处理约束问题的决策程序。
限制约束。Constraint Reduction.
A common optimization approach followed by both solvers and symbolic executors is to reduce constraints into simpler forms. For example, the expression rewriting optimization can apply classical techniques from optimizing compilers such as constant folding, strength reduction, and simplification of linear expressions.
求解器和符号执行器共同的优化方法是将约束简化为更简单的形式。例如，表达式重写优化可以应用编译器优化中的经典技术，如常数折叠，强度降低，线性表达式的简化。
重用约束的解。Reuse of Constraint Solutions.
The idea of reusing previously computed results to speed up constraint solving can be particularly effective in the setting of a symbolic executor, especially when combined with other techniques such as constraint independence optimization. Most reuse approaches for constraint solving are currently based on semantic or syntactic equivalence of the constraints.
重用先前计算结果以加快约束求解的思想在符号执行器的设置中尤其有效，特别是在与约束独立优化等技术相结合时。大多数用于约束求解的重用方法目前都是基于语义或语法等价的约束。
懒惰约束。Lazy Constraints.
[Ramos and Engler, 2015]采用约束求解查询超时的方法。在他们最初的实验中，作者将大多数超时追踪到符号除法和余数运算，最坏的情况发生在无符号余数运算在分母中具有符号值的情况下。
因此，他们实现了如下解决方案：当执行器遇到一个涉及大开销的符号操作的分支语句时，它将同时使用真和假分支，并将对开销操作结果的延迟约束添加到路径条件中。当探索到达满足某个目标的状态（例如发现一个错误）时，该算法将检查路径的可行性，并且如果在真实执行中被视为不可达，则抑制该路径。
具体化。Concretization.
A concolic executor generates some random input for the program and executes it both concretely and symbolically: a possible value from the concrete execution can be used for a symbolic operand involved in a formula that is inherently hard for the solver, albeit at the cost of possibly sacrificing soundness in the exploration.
concolic执行为程序生成一些随机的输入，并以具体和象征的方式执行它：当符号执行遇到一个对求解器来说很困难的公式时，具体执行中的一个可能值可以用于这个公式中涉及的一个符号操作数，尽管代价是有可能在探索中牺牲正确性。
- void test(int x, int y) {
- if (non_linear(y) == x)
- if (x > y + 10)
- ERROR;
- }
- int non_linear(int v) {
- return (v*v) % 50;
- }
由于存在v*v，不支持非线性的求解器无法计算。举例：concolic执行随机选择出x=3，y=5作为初始输入，这个具体化执行不会进入第3行的语句。但引擎可以重新使用y的值， ay=5计算出ax=25，走到ERROR。值得注意的是：如果y被固定为5，将无法生成新的输入，总是走到ERROR分支，这种情况下，可以重新运行程序，为y选择不同的值，比如y=2计算出x=4，不会走到ERROR分支。
[P˘as˘areanu et al., 2011] suggests mixed concrete-symbolic solving, which considers all the path constraints collectable over a path before binding one or more symbols to specific concrete values.
[P˘as˘areanu等人，2011]提出mixed concrete-symbolic solving，它将一个或多个符号绑定到特定的具体值之前，考虑路径上可收集的所有路径约束。
处理不确定的约束。Handling Problematic Constraints.
这节主要讲涉及非线性算术和库调用的问题
[Dinges and Agha, 2014a] proposes a concolic walk algorithm that can tackle control-flow dependencies involving non-linear arithmetic and library calls. The algorithm treats assignments of values to variables as a valuation space: the solutions of the linear constraints define a polytope that can be walked heuristically, while the remaining constraints are assigned with a fitness function measuring how close a valuation point is to matching the constraint. An adaptive search is performed on the polytope as points are picked on it and non-linear constraints evaluated on them. Compared to mixed concrete-symbolic solving [P˘as˘areanu et al., 2011], both techniques seek to avoid blind commitment. However, concolic walk does not rely on the solver for obtaining all the concrete inputs needed to evaluate complex constraints, and implements search heuristics that guide the walk on the polytope towards promising regions.
[Dinges and Agha, 2014a]提出了一种concolic walk算法，可以处理涉及非线性算术和库调用的控制流依赖。该算法将值的赋值作为估值空间来处理：线性约束的解决方案定义了可以启发式walk的多面体，而其余的约束被赋值为适应度函数，来测量估值点与约束匹配的程度。 在多面体上进行自适应搜索，在其上选取点并对其进行非线性约束评估。 与上一节的mixed concrete-symbolic solving相比，这两种技术都试图避免盲目的折中。 然而，concolic walk并不依赖于求解器来获得评估复杂约束所需的所有具体输入，并且实现了搜索启发式，指导多面体在有前途的区域前进。
[Dinges and Agha, 2014b] describes symcretic execution, a novel combination of symbolic backward execution (SBE) (Section 2) and forward symbolic execution. The main idea is to divide exploration into two phases. In the first phase, SBE is performed from a target point and a trace is collected for each followed path. If any problematic constraints are met during the backward exploration, the engine marks them as potentially satisfiable by adding a special event to the trace and continues its reversed traversal. Whenever an entry point of the program is reached along any of the followed paths, the second phase starts. The engine concretely evaluates the collected trace, trying to satisfy any constraint marked as problematic during the first phase. This is done using a heuristic search, such as the concolic walk described above. An advantage of symcretic over classic concolic execution is that it can prevent the exploration of some unfeasible paths. For instance, the backward phase may determine that a statement is guarded by an unsatisfiable branch regardless of how the statement is reached, while a traditional concolic executor would detect the unfeasibility on a per-path basis only when the statement is reached, which is unfavourable for statements “deep” in a path.
[Dinges and Agha，2014b]描述了symcretic execution，后向符号执行SBE和前向符号执行的新颖组合。在第一阶段，从目标点执行SBE，并且为每个后续路径收集轨迹。如果在向后探索过程中遇到任何有问题的约束条件，引擎就会通过向追踪添加一个特殊事件, 将其标记为可能满足的并继续其反向遍历来,只要程序的入口点沿任何后续路径到达，那么就开始第二阶段，引擎具体地评估收集的轨迹，试图满足在第一阶段期间标记约束，这是通过启发式搜索完成的，比如上面描述的concolic walk。与传统的concolic执行相比，一个优点是它可以阻止探索一些不可行的路径。例如，SBE阶段可以确定一个状态是由一个不可满足的分支到达的，而不管这个状态是如何得到的，而一个传统的concolic执行者只有当这个状态被达到时才会根据每个路径检测到不可行性，对于在路径中很“深”的状态这是不利的。
7. 更多的研究方向
7.1 分割逻辑 separation logic (SL)
检查指针程序的内存安全属性是程序验证中的一个主要挑战。
SL主要思想：二元运算符*被用来把堆分成两部分，其参数分别保存
A ∗ x → [n : y] 表示有x指向一个记录，该记录在y的n字段，而A保留堆的其余部分。
程序状态被建模为一个符号堆Π|Σ：Π是与变量相关的纯谓词的有限集合，而Σ是堆谓词的有限集合。符号堆是使用抽象语义根据程序代码符号执行的SL公式。 通常使用SL规则来支持符号堆的包含，推断哪些堆部分不受语句影响，并确保经由抽象（例如，使用扩展操作符）来终止符号执行。
7.2 不变量
Loop invariants play a key role in verifiers that can prove programs correct against their full functional specification.
循环不变量在验证者证明程序的正确与完整的功能规范中发挥关键作用。
An invariant is an inductive property that holds when the loop is first entered and is preserved for an arbitrary number of iterations.
不变量是一个归纳属性，它在第一次进入循环时被保留，并被保存在任意次的迭代中。
困难：没有该领域专家的人工干预，计算循环不变量很困难。事实上，验证实践的经验表明，与其他规范元素（如方法前置/后置条件）相比，提供循环不变式要困难得多。
几个研究：
Termination analysis
Predicate abstraction
7.3 函数摘要Function Summaries
函数摘要（第5.2节）主要用于静态和动态程序分析，尤其是程序验证。
7.4 程序分析和优化
我们认为，符号执行可能会从编程语言领域的相关问题的解决方案中获益。例如，在并行计算社区中，诸如循环合并等转换可以通过平滑索引的迭代空间来将嵌套循环重构为单个循环。这样的转换可能会简化符号探索，增强搜索启发式和状态合并策略。
Loop unfolding 循环展开
Program synthesis
7.5 符号计算
SAT虽然是NP问题，但过去几十年也有一些实际的应用方法。
In particular, advances in symbolic computation have produced powerful methods such as Gr¨obner bases for solving systems of polynomial constraints, cylindrical algebraic decomposition for real algebraic geometry, and virtual substitution for non-linear real arithmetic formulas [Abraham, 2015].
特别是符号计算方面的进步已经产生了强大的计算方法，如用于求解多项式约束系统的Gr¨obner基，用于实数代数几何的圆柱代数分解，以及用于非线性实数算式的虚拟替换。
While SMT solvers are very efficient at combining theories and heuristics when processing complex expressions, they make use of symbolic computation techniques only to a little extent, and their support for non-linear real and integer arithmetic is still in its infancy [Abraham, 2015]. To the best of our knowledge, only Z3 [De Moura and Bjørner, 2008] and SMT-RAT [Corzilius et al., 2015] can reason about them both.
尽管SMT解算器在处理复杂表达式时非常有效地将理论和启发式算法相结合，但是它们只是在一定程度上利用了符号计算技术，而且它们对非线性实数和整数算术的支持还处于起步阶段[Abraham，2015]。 据我们所知，只有Z3 [De Moura andBjørner，2008]和SMT-RAT [Corzilius et al。，2015]可以推测这两者。
8. 总结
在过去的十年中，符号执行技术已经发生了重大变化，导致重大的突破。2016年，DARPA网络大挑战赛主机系统可以检测并修复未知软件中的漏洞，如Angr和Mayhem，赢得$ 2 M的Mayhem也是第一个在DEF CON 24黑客大会上进行Capture-The-Flag比赛的自主软件。
事件表明，基于符号执行的自动漏洞检测工具可以与人类专家竞争，为未来几十年潜在影响软件可靠性的前所未有的应用铺平道路。
本次调查讨论了符号执行的一些关键方面和挑战。为了解释符号执行者的基本设计原理和主要的优化技术，我们把注意力集中在整数运算的单线程应用上。多线程程序的符号执行例如[Khurshid et al., 2003, Sen, 2007, Bucur et al., 2011, Farzan et al., 2013, Bergan et al., 2014, Guo et al., 2015]，而用于处理浮点数据的程序的技术例如[Meudec, 2001, Botella et al., 2006, Lakhotia et al., 2010, Collingbourne et al., 2011, Barr et al., 2013, Collingbourne et al., 2014, Ramachandran et al., 2015]。
我们希望这次调查能够帮助非专家把握好符号执行这一令人兴奋的研究领域的重大发明，激发进一步的工作和新的思路。
附录
工具：
|
Symbolic engine |
References |
Project URL (last retrieved: August 2016) |
|
CUTE |
[Sen et al., 2005] |
– |
|
DART |
[Godefroid et al., 2005] |
– |
|
jCUTE |
[Sen and Agha, 2006] |
|
|
KLEE |
[Cadar et al., 2006, Cadar et al., 2008] |
|
|
SAGE |
[Godefroid et al., 2008, Elkarablieh et al., 2009] |
– |
|
BitBlaze |
[Song et al., 2008] |
|
|
CREST |
[Burnim and Sen, 2008] |
|
|
PEX |
[Tillmann and De Halleux, 2008] |
|
|
Rubyx |
[Chaudhuri and Foster, 2010] |
– |
|
Java PathFinder |
[P˘as˘areanu and Rungta, 2010] |
|
|
Otter |
[Reisner et al., 2010] |
|
|
BAP |
[Brumley et al., 2011] |
|
|
Cloud9 |
[Bucur et al., 2011] |
|
|
Mayhem |
[Cha et al., 2012] |
– |
|
SymDroid |
[Jeon et al., 2012] |
– |
|
S2E |
[Chipounov et al., 2012] |
|
|
FuzzBALL |
[Martignoni et al., 2012, Caselden et al., 2013] |
|
|
Jalangi |
[Sen et al., 2013] |
|
|
Pathgrind |
[Sharma, 2014] |
|
|
Kite |
[do Val, 2014] |
|
|
SymJS |
[Li et al., 2014] |
– |
|
CIVL |
[Siegel et al., 2015] |
|
|
KeY |
[Hentschel et al., 2014] |
|
|
Angr |
[Shoshitaishvili et al., 2015, Shoshitaishvili et al., 2016] |
|
|
Triton |
[Saudel and Salwan, 2015] |
|
|
PyExZ3 |
[Ball and Daniel, 2015] |
|
|
JDart |
[Luckow et al., 2016] |
|
|
CATG |
– |
|
|
PySymEmu |
– |
|
|
Miasm |
– |