Reading Papers 03 - Symbolic Execution
# 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 为第 条指令处的集合,记为 。
该文章的冗余状态检测算法流程如下:
初始时,构建 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 的部分,例如 中依赖于 的部分为 。
dynamic slicing :
该文章运用 动态切片 (dynamic slicing) 技术来计算 relevant location set :对于每处 variable occurence ,动态切片能找到所有影响其值的程序指令。
是动态计算的,需要等到第 条指令之后的所有 fork 都执行完成之后,才能从终点出发沿路径后向构造。
定义 relevant control set 为运行时刻控制第 条指令的分支指令集,记为 。 是用作构造 的中间集合。
和 的后向构造过程如下(??):
计算 为第 条指令的所有直接后继指令的 relevant location set 的并集。在非分叉点处 。类似地计算 。
如果第 条指令是(动态)赋值指令 且 ,则计算 为控制 的分支指令集,并将 中涉及的所有 variable occurence 加入 。
如果第 条指令是(动态)分支指令 ,则计算 为(由 dynamic dependence graph 维护的)控制 的分支指令集,同时将 加入 。
如果上述 满足以下条件之一,则将 中涉及的所有 variable occurence 加入 :
对应于某个 static relevant branch ;
;
存在 potentially depends on 。
对于 write 指令 和 ,如果存在分支指令 读取了 写入的位置,并且 静态控制赋值指令 not along the path ,并且 是 静态的写入位置的别名,则称 potentially depends on 。
# Directed Symbolic Execution
# SAS'11 - SDSE & CCBSE
# FSE'13 - KATCH
目标是改善现有的 directed symbolic execution 技术,将其应用于真实软件系统的补丁测试上,并实现测试的完全自动化。
KATCH 实现了三种基于程序分析的启发式策略,使符号执行能更高效地生成能到达指定目标(补丁所影响或新增的基本块)的测试用例。
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01