Symbolic Execution

Selective Symbolic Execution

ASPLOS'11 - S2E

Hybrid Symbolic Execution

ICSE'14 - Veritesting (MergePoint)

使用路径作为程序执行的抽象并不是完美的。在有些情况下，一段代码可能具有海量的路径数，但从语义的角度看，可以轻易将其划分为数个等价类。

KEY Idea ：对于一些代码片段来说，符号执行难以处理，但是程序验证的手段却容易处理。

当遇到路径分支时，Veritesting 不像传统符号执行那样直接 fork ，而是切换到静态方法。

在 binary-level 静态地恢复 CFG ，以 incomplete loop 、syscall 、exit 等等作为 transition points（即切换回符号执行的位置），然后在 CFG 上作静态符号执行，求取以 VC 形式表示的路径约束。

---

State Merging

ATC'13 - Redundant State Detection

KEY Idea ：如果符号执行的目标是代码行覆盖，那么大多数路径是冗余的、不需要探索的，我们只需要考虑那些能覆盖新代码行的路径。

定义 static relevant branch 为可能影响某些未覆盖的代码是否可达的分支指令。

定义 relevant location 为影响 static relevant branch 的控制流的 variable occurence 的集合。该集合随程序执行动态变化，定义 k-th relevant location set 为第 $k$ 条指令处的集合，记为 $L_k$ 。

该文章的冗余状态检测算法流程如下：

• 初始时，构建 static control dependence graph 以发掘 static relevant branch 。

• 对于分支指令，像一般的符号执行引擎那样进行分叉；对于直接执行指令：

• 根据指令效果更新 dynamic dependence graph 。该图维护了每两个 write 指令之间、以及分支指令与其所控制的 write 指令之间的，运行时刻的动态数据依赖关系。

• 如果是未覆盖的代码，则使用 static control dependence graph 更新 relevant location set（可能去除一些已经不再影响后续未覆盖代码的变量），并且 3.4 对 relevant location set 进行细化。

• 尝试进行状态匹配和冗余去除。

冗余状态检测的关键是如何判定状态的等价性，以两个状态的路径约束完全相同作为判定标准是过于保守的。子集判断比全等价判断更宽松：如果状态 A 的约束集是状态 B 的子集，则称状态 B 是冗余的，因为该状态受到更强的约束，因此不会探索到任何新的代码。

该文章使用更加精确的判断条件（？）：如果状态 A 的相关依赖约束集是状态 B 的子集，则称状态 B 是冗余的。

• 相关依赖约束集：指约束集中依赖于 relevant location set 的部分，例如 $\{a > 0,\ c > 1\}$ 中依赖于 $\{a,\ b\}$ 的部分为 $\{a > 0\}$ 。

dynamic slicing ：

该文章运用 动态切片 (dynamic slicing) 技术来计算 relevant location set ：对于每处 variable occurence ，动态切片能找到所有影响其值的程序指令。

$L_k$ 是动态计算的，需要等到第 $k$ 条指令之后的所有 fork 都执行完成之后，才能从终点出发沿路径后向构造。

定义 relevant control set 为运行时刻控制第 $k$ 条指令的分支指令集，记为 $C_k$ 。$C_k$ 是用作构造 $L_k$ 的中间集合。

$L_k$ 和 $C_k$ 的后向构造过程如下（？？）：

计算 $L_k^{\cup}$ 为第 $k$ 条指令的所有直接后继指令的 relevant location set 的并集。在非分叉点处 $L_k^{\cup} \equiv L_{k + 1}$ 。类似地计算 $C_k^{\cup}$ 。

如果第 $k$ 条指令是（动态）赋值指令 $e2 := e1$ 且 $e2 \in L_k^{\cup}$ ，则计算 $C_k$ 为控制 $b$ 的分支指令集，并将 $e_1$ 中涉及的所有 variable occurence 加入 $L_k$ 。

如果第 $k$ 条指令是（动态）分支指令 $b$ ，则计算 $C_k$ 为（由 dynamic dependence graph 维护的）控制 $b$ 的分支指令集，同时将 $C_k^{\cup} - \{b\}$ 加入 $C_k$ 。

如果上述 $b$ 满足以下条件之一，则将 $b$ 中涉及的所有 variable occurence 加入 $L_k$ ：

• $b$ 对应于某个 static relevant branch ；

• $b \in C_k^{\cup}$ ；

• 存在 $l \in L_k^{\cup}$ potentially depends on $b$ 。

对于 write 指令 $w_1$ 和 $w_2$ ，如果存在分支指令 $b$ 读取了 $w_1$ 写入的位置，并且 $b$ 静态控制赋值指令 $e_2 := e$ not along the path ，并且 $e_2$ 是 $w_2$ 静态的写入位置的别名，则称 $w_2$ potentially depends on $w_1$ 。

---

Directed Symbolic Execution

SAS'11 - SDSE & CCBSE

FSE'13 - KATCH

目标是改善现有的 directed symbolic execution 技术，将其应用于真实软件系统的补丁测试上，并实现测试的完全自动化。

KATCH 实现了三种基于程序分析的启发式策略，使符号执行能更高效地生成能到达指定目标（补丁所影响或新增的基本块）的测试用例。

---