摘要： 本文首先介绍了符号执行的过程内分析和程序全局分析的基本原理；接着介绍了其中的路径状态空间爆炸、复杂结构语义和操作语义建模及程序全局分析这三个关键技术的难点及相关研究；最后介绍了一些使用符号执行技术开发的研究型工具。本文从基本原理到技术难点，从理论基础到工具，较系统地论述了符号执行技术。
关键词：符号执行 静态分析 源代码安全

Research of Symbolic Execution

Jinbin Lin Xiaofei Zhang Hui Liu

China Information Technology Security Evaluation Center University of Science and Technology of China

Abstract: The first portion of this paper introduces the basic principles of intra-procedural and inter-procedural analysis of symbolic execution. And the second presents the relevant researches of the difficulties of the three critical technologies, which are “Explosion of the state space of Paths”, “Modeling the complex structure-semantic and operation-semantic”, and “inter-procedural analysis”. Final, some tools of research that developed by using the technology of symbolic execution are introduced. This paper systematically presents the symbolic execution range from the basic principles to the technical difficulties and from the theoretical principles to tools.
Key words: Symbolic Execution, Static Analysis, Source code security

一、 简 介
    软件的安全性越来越受到人们的重视，如何检测软件中存在的安全问题也逐渐成为软件工程领域的研究热点。《Software Security》一书的作者Gary McGraw估计，在引发安全问题的错误中，大约有一半是实现时的疏忽、遗漏或误解造成的。基于源代码的静态分析工具是检测软件编码安全问题的一种有效方法。
    静态分析是一种在不执行程序的情况下对代码进行评估的技术，它通过对当前状态及趋势的分析来预判未来所有软件运行可能的情况。源代码静态分析方法涉及的理论包括指称语义、公理化语义、操作语义、抽象解释理论等，常见的实现技术有模型检验、数据流分析、抽象解释、谓词转换、定理证明、类型推导、符号执行等。其中，符号执行是目前源代码静态分析工具常采用的主要技术之一，本文将重点介绍符号执行技术的基本原理、关键技术及发展现状。

二、 符号执行的基本原理
1. 基本原理
    符号执行是指在不执行程序的前提下，用符号值表示程序变量的值，然后模拟程序执行来进行相关分析的技术，它可以分析代码的所有语义信息，也可以只分析部分语义信息（如只分析“内存是否释放”这一部分的语义信息）。
    符号执行分为过程内分析和过程间分析（又称全局分析）。过程内分析是指只对单个过程的代码进行分析，全局分析指对整个软件代码进行上下文敏感的分析。所谓上下文敏感分析是指在当前函数入口点要考虑当前的函数间调用信息和环境信息等。程序的全局分析是在过程内分析的基础上进行的，但过程内分析中包含了函数调用时就也引入了过程间分析，因此两者之间是相对独立又相互依赖的关系。
    过程内分析流程如图1所示。首先，对待分析的单个过程代码对象构建控制流图（Control Flow Graph, CFG）。控制流图（CFG）是编译器内部用有向图表示一个程序过程的一种抽象数据结构，图中的节点表示一个程序基本块，基本块是没有任何跳转的顺序语句代码块，图中的边表示代码中的跳转，它是有向边，起点和终点都是基本块。在CFG上从入口节点开始模拟执行，在遇到分支节点时，使用约束求解器判定哪条分支可行，并根据预先设计的路径调度策略实现对该过程所有路径的遍历分析，最后输出每条可执行路径的分析结果。其中，约束求解是数学上的判定过程，形象地说是对一系列的约束方程进行求解。
    如果要进行源代码的安全性检测，则需要在过程内分析时，根据具体的安全知识库来添加安全约束。例如，如果要添加缓冲区溢出的安全约束，则在执行时遇到对内存进行操作的语句时，就要对该语句所操作的内存对象的边界添加安全约束。以上面的方式来进行安全约束的添加，并且每次在添加之后就使用约束求解器对所有的安全约束进行求解，以判定当前是否可能潜在一个安全问题。
    图 1 过程内分析原理流程图
    程序全局分析流程如图2所示。首先，为整个程序代码构建函数调用图（Call Graph，CG），在函数调用图中，节点表示函数，边表示函数间的调用关系。根据预设的全局分析调度策略，对CG中的每个节点（对应一个函数）进行过程内分析，最终给出CG每种可行的调用序列的分析结果。
    图 2 全局分析原理流程图

(责任编辑：adminadmin2008)