高代码覆盖率的软件自动化测试是开发高质量软件的关键性技术。符号执行是一种重要的形式化和自动化的程序分析理论,是一种生成能够覆盖特定执行路径测试用例的方法模型,能够与程序的抽象和推理、模型检测等理论相互结合,在程序的自动化测试、缺陷检测、程序的验证与确认、正确性证明等方面有较好的应用前景。符号执行的基本原理是通过输入数据符号化,将运算过程表示为路径执行条件的符号表达式,从而将测试数据生成问题转换为可满足性(Satisfiability)理论的约束求解问题。近几年来符号执行技术发展快速,在早期只能分析简单数据类型和简单数据运算的单过程程序,目前向着能够应用于复杂数据类型、复杂运算操作、多过程程序的方向发展。但是符号执行技术向实用化方向发展的过程中仍然存在如下三方面困难。其一,对于任意功能外部过程调用的处理方法存在局限性(外部调用承担了目标程序与执行环境交互的功能,因此这种局限性也称为环境交互问题)。实际情况中或由于外部调用黑盒的特性,或由于外部调用会极大增加程序体积,而无法进行有效符号执行分析。现有的以实际执行值替换符号变量的方法具有严重的片面性,而基于环境建模的方法不具备实用性。其二是路径爆炸问题,符号执行存在程序路径数量会随着程序体积呈指数性增长的现象。这造成对大型程序的分析很难在可容忍的时间消耗和资源消耗内完成。而现有的函数摘要等解决方法存在不精确性和无法处理递归调用等问题。其三,对具有复杂数据结构、基于指针运算、内存动态分配等复杂数据运算的程序的处理模型不健全,对任意形式的数据结构不能完全处理。这些问题是当前符号执行理论发展的最大障碍,已经成为学界研究的热点。本文的研究工作试图解决上述问题,主要包括以下几个方面：第一项工作也是论文中最重要的工作是针对路径爆炸问题,提出了分段符号执行模型。分段符号执行是一种新的符号执行模型,基本思路是将大型程序的分析拆分为多个程序单元的分析,可分多次选择性的执行目标程序中的不同单元。其中每一分析单元内的路径数量都在可控制的范围内,不会造成持续的路径爆炸,但是如果需要满足总的分析时间仅为各部分分析时间的总和,前提是能够处理外部调用和环境交互的问题,使得实际执行的时间消耗要大大小于符号执行的时间消耗。在分段符号执行中,各目标单元间的调用也成为了外部调用,因此环境交互问题就成为了分段符号执行模型的关键性问题。论文通过对外部调用的参数属性判断、实际执行过程的程序行为分析及IO对象建模的方法来处理环境交互问题。论文的第二项工作是在数据流分析理论和方法的基础上,定义并判断外部过程调用的参数属性。通过参数属性抽象描述了外部过程中的数据输入与输出等行为,从而能够检测到并符号化输入的数据。这将程序分析过程中对外部调用的处理转换为了函数内部分析。论文中所采用数据流分析是一种成熟的程序分析方法,对符号执行的时间消耗影响很小。第三是提出了实际执行过程的程序行为分析及IO对象建模的方法,这两种方法在分段符号执行系统框架中体现。系统框架包括一种适用于分段符号执行模型的中间语言和一个执行引擎。通过设立内置的堆块数据类型、监控内存分配与释放操作、符号化系统对象、监控实际执行过程中的I0操作、使用函数调用序列等方法,建立了外部过程的程序实行行为与目标单元中符号执行行为的联系,化解了程序表示的缺失所造成的无法进行符号执行分析的问题,从而能够有效处理外部调用过程中的环境交互性。这使得在分析目标的程序内,任意的选择若干过程作为一次分析的目标单元成为了可能,是分段符号执行能够正确进行的基础。第四,论文研究了分段符号执行模型的一个典型应用——检测程序中缓冲区溢出等内存相关缺陷。在任意形式的数据结构的抽象表示方法的基础上,研究了使用分离逻辑推导规则和约束求解等方法在分段符号执行结果中检测程序的潜在安全缺陷,以提高复杂程序的安全性。论文实验验证了分段符号执行模型解决符号执行中路径爆炸问题和环境交互问题的有效性。