论文部分内容阅读
符号执行介于程序验证和程序调试之间,是一种静态分析方法。但是符号执行不能全面的对软件可靠性进行检测。因此在符号执行的基础上,发展出了动态符号执行。动态符号执行用符号值来表示程序的输入值,并且为程序提供一个具体值的输入,在应用程序执行的同时进行符号执行,用符号执行来收集条件,求解条件得到具体输入,覆盖尽可能多的路径。程序插桩技术是动态符号执行中的重要技术之一。程序插桩技术是对具体的程序进行分析,构造它的插装模块。在动态符号执行中我们对源程序进行分析,构造插桩模块实现对输入值的符号化、符号计算以及约束收集。程序插桩在程序分析和程序检测方面都有着广泛的应用。目前研究者开发出了一些动态符号执行工具,但基本都是基于Linux平台的。本文是在Windows平台下对动态符号执行技术进行研究,程序插桩的实现也是在该平台下进行的。本文的主要工作是对动态符号执行中的程序插桩进行研究和实现。本文的插桩是基于底层虚拟机(Low Level Virtual Machine,LLVM)中间表示(Intermediate Representation,IR)的,在插桩函数中实现符号运算以及约束收集。本文主要贡献主要有以下几点:1.对动态符号执行技术进行研究,以动态符号执行为目标,设计出Windows平台下的动态符号执行框架。2.研究LLVM IR语言,对其进行词法语法分析,在程序分析的过程中,收集插桩信息。本文主要是对建模仿真验证语言(Modeling Simulation Verification Language,MSVL)编译器产生的LLVM IR进行插桩实现动态符号执行。3.设计实现动态符号执行中的程序插桩。实现动态符号执行中程序插桩的两个目标。(1)设计插桩函数,实现对程序输入值的符号化,对符号变量的运算,以及对约束条件的收集。(2)输出程序的控制流图以供后面路径搜索使用。4.选取具有代表性的测试用例和一个实例“冒泡排序”验证了动态符号执行中程序插桩的正确性和可用性。