Symbolic Execution 白盒静态分析技术

Dynamic Symbolic Execution 动态符号执行：静态+动态

一个程序执行的路径通常是true和false条件的序列，这些条件是在分支语句处产生的。在序列的第i位置如果值是true，那么意味着第i个条件语句走的是then这个分支；反之如果是false就意味着程序执行走的是else分支。程序的所有执行路径可以表示为树，叫做执行树

把输入变为符号值，那么程序计算的输出值就是一个符号输入值的函数，即所谓的形式化（形式模型），就是对计算过程的数学描述。

为了形式化地完成这个任务，符号执行会在全局维护两个变量。

• 符号状态 σ ，变量到符号表达式的映射
• 符号化路径约束（路径条件） PC

在符号执行的开始，符号状态 σ 会先初始化为一个空的映射，而符号化路径约束PC初始化为true。 σ 和PC在符号执行的过程中会不断更新。

在符号执行结束时，PC就会用约束求解器进行求解，以生成实际的输入值。

这样的过程也叫作路径的可行性分析，它是符号执行的关键部分，我们常常将符号取值约束的求解问题转化为一阶逻辑的可满足性问题，从而使用可满足性模理论（SMT）求解器对约束进行求解。

SAT/SMT

正向执行

• 过程内分析：只对单个函数的代码进行分析，逐句地对程序语句进行分析
• 过程间分析（全局分析）：常常需要考虑按照怎样的顺序分析程序语句，如深度优先遍历和广度优先遍历。另外在进行分析时，需要先确定一个分析的起始点，可以是程序入口点、程序中某个过程的起始点或者某个特定的程序点。

逆向执行：用于对可能存在漏洞的部分代码进行有针对性的分析