符号执行

符号执行是一种确定程序输入与程序执行路径关系的一种技术,与常规程序执行不同,符号执行把原本具体的程序输入值替换为可任意取值的符号值后再执行程序。在符号执行中,如果遇到路径分支,符号执行引擎会对当前的执行状态进行 fork,然后按照一定的策略分别对 fork 后的每个分支符号执行,同时把分支点的约束条件作为执行相应分支的路径约束条件,这样每条执行路径都对应着一个对程序输入进行约束的条件集合,通过对该约束条件集合进行求解,可得到对应每条执行路径的具体输入值。理论上,通过符号执行可以遍历程序中所有的路径分支,从而为发现每条路径上可能存在的漏洞提供了条件。

混合符号执行(Concolic Execution)是一种特殊的符号执行方式,在 2006 年左右提出。不同于传统的的符号执行,在混合符号执行时,需要一个具体的输入值进行引导,符号执行引擎仅对由具体输入值引导的程序执行路径进行符号执行并收集约束条件,但在分支点不进行 fork。混合符号执行主要用于测试用例的生成。

2008 年,Cristian Cadar 等发布了开源符号执行工具 KLEE,KLEE 的开源对于基于符号执行的漏洞挖掘具有深远的意义,后续很多用于漏洞挖掘的工具如 S2E,AEG 等都使用了 KLEE 的符号执行引擎。KLEE 对当时 432 个程序进行了符号执行,发现了 56 个比较严重的漏洞,此外 KLEE 进行符号执行时的代码覆盖率很高,文中很多待测程序的代码覆盖率都达到了 100%。

2010 年,David Brumley 等人开发了针对源码的漏洞挖掘和自动利用工具 AEG,作者在文中提出基于前置条件的符号执行,用于对符号执行的路径进行约简,同时提出了路径优先算法,用于优先挖掘可被利用的漏洞。AEG 分析了当时的 14 个开源程序,自动产生了 16 个控制流劫持的利用代码,其中包含 2 个未知漏洞的利用。2012 年,David Brumley 等人在 AEG 的基础上又发布了针对二进制程序的漏洞挖掘和自动利用工具 MAYHEM,文中提出了一种新的符号执行方式,即把在线符号执行和离线符号执行结合起来,寻求符号执行效率和资源消耗的平衡,MAYHEM 最终成功的对当时 29 个二进制程序进行了漏洞挖掘和漏洞利用。文中还对 AEG 和 MAYHEM 的执行效率进行了对比,MAYHEM 平均仅比 AEG 慢 3.4 倍。

Vitaly Chipounovt 等利用 QEMU 和 KLEE 开发了针对二进制程序的选择符号执行(Selective Symbolic Execution)开源工具 S2E。S2E 的扩展性很好,利用 QEMU 虚拟机,S2E 可以对 x86 架构下的任意平台的二进制代码进行漏洞挖掘,并且很容易扩展到其他 CPU 架构,比如 ARM 或者 PowerPC 等。S2E 利用提出的选择符号执行技术缓解了符号执行中存在路径爆炸和环境交互问题。

最后更新于