基于Matlab的一维条形码检测：符号执行原理与发展

第三章 面向二进制程序的混合符号执 行技术 符号执行（symbolic execution）是一种代码执行空间遍历技术，在软件安 全、恶意代码分析、程序调试等领域有着重要应用。本章介绍符号执行技术的原 理、发展历史，分析符号执行技术的不足。结合二进制程序分析的需求，本章介 绍一种面向二进制程序的混合符号执行技术的设计与实现。 3.1 符号执行原理及发展 符号执行用抽象符号代替程序变量，根据程序的语义，在每条路径上通过符 号计算引擎对抽象符号做等语义操作，模拟程序执行。采用符号执行的好处在于 能够发现变量之间代数运算关系，便于理解程序的内在逻辑，在漏洞挖掘时，有 利于在复杂的数据依赖关系中发现数据之间本质的约束关系，而且符号执行精确 记录了路径的约束条件，可以进一步用于判断路径可行性和路径约束的完备性。 表3.1展示了符号执行过程。其中，第一列表示一条程序路径，第二列表示对 该路径污点分析的结果，第三列是对该路径的符号执行结果。本例中，在第一句 代码执行后，符号执行引擎将变量x赋予符号值x0，并根据后继各行代码的语义， 更新程序变量与符号值的关系，收集路径上的约束条件。 将符号执行与污点分析过程对比，我们可以发现，污点分析跟踪了污点数据 的传播，但并不能提供程序对污点数据处理的运算关系。而符号执行则记录了所 有运算过程。例如，从指令层看，变量m与污点数据x存在数据依赖关系；但是从 宏观角度讲，m在第5句代码处始终为常数值，实际上与污点变量x并不相关。污 点分析并不能有效处理这种问题，仍然会将变量m视为污点数据。但通过符号计 算，符号执行引擎可以计算出此时变量m为常数值2，与符号值x0并不相关。 进一步，第二行代码中条件判断成立时，意味着谓词x0>0成立；符号执行