5.1.2 选择性符号执行
更新于 2026年10月10日
版权声明
5.1.2 选择性符号执行
经典符号执行技术的一个主要限制就是路径爆炸问题,符号执行技术难以扩展应用到包含很多函数调用的大型程序中。选择性符号执行(Selective Symbolic Execution,SSE)通过选择性地对于用户指定的程序范围使用符号执行或者具体执行来解决符号执行的扩展性问题。这一思路基于如下观察规律:用户很可能需要重点关注程序中的一部分代码是否存在缺陷,对于这部分程序应当搜索所有路径,在其他部分(如库函数中)则不必要搜索每一条程序路径。因此,选择性符号执行将被测程序分成多个部分,在一些部分中利用符号执行技术进行全路径搜索,在其他部分利用动态执行得到一条程序路径。
图5-1给出了选择性符号执行的示意图。被测程序app调用了一个用户定义的库函数lib以及系统函数kernel。图5-1表示在用户定义的库函数lib中利用符号执行进行全路径搜索,文字部分表示在系统函数kernel和app中利用具体执行进行单路径执行。为了实现从符号执行转为具体执行或者从具体执行转为符号执行,选择性执行需要能够将执行状态在符号域和具体域之间进行互相转换。从符号域到具体域的切换方法是通过在满足当前部分路径的约束条件的值域中选择一个解作为具体执行的输入;从具体域到符号域的切换方法是将具体值用符号值代替,同时利用具体执行的路径信息得到具体执行过程中的约束。符号域和具体域之间的转换过程需要保证程序状态的一致性,在文献[3]中提到维持转换过程中约束一致性的策略。(https://www.daowen.com)

图5-1 选择性符号执行的示意图