基于符号执行的代码静态检测方法分析与实现-analysis and implementation of code static detection method based on symbol execution.docx

摘 要随着软件技术的普及发展，软件系统被应用到我们生活的各个方面，在带来 极大便利的同时我们也承受着由软件漏洞所带来的巨大风险。如何有效的保证软 件质量是一个极为迫切的需求。在保证软件质量的方法中有两大类，前期可以通 过静态分析源代码尽早发现潜在漏洞；后期可以动态运行二进制代码分析实际运 行结果。程序的漏洞越早发现其修改成本越小，所以程序静态分析是一种重要的 软件质量保证方法。在众多的静态分析方法中，符号执行以其高度的精确性获得 了极大关注。符号执行是一种路径敏感上下文相关的分析方法，在计算资源足够充分的情 况下它可以对程序进行非常精确地分析，从而发现一些细微的漏洞。然而符号执 行理论本身也面临着几大难题，其中包括路径爆炸、约束求解和内存模型。论文首先对近三十年来符号执行技术的发展进行了概述，讨论了符号执行的 基本原理和近年提出的一些改进方法。这些改进包括：在测试数据生成方面提出 了动态符号执行，它是一种结合具体值和符号值的方法；在路径爆炸抑制方面提 出一些启发式有哪些信誉好的足球投注网站策略；在约束求解方面主要提出了无关约束消除和增量式求解。 本文紧接着分析讨论了一种非常强大的中间语言 LLVM IR，对其语法构成、数据 类型及指令集做了分析，并对其数据类型和指令集进行了形式化描述。本文随后 对符号执行中内存模型展开了讨论，对比了当下符号执行理论中各种主流内存模 型（名字值模型、数组模型和基于区域的三元组模型）的优缺点，并提出一种树 状结构的内存模型 TMM（Tree-memory model）。这种内存模型的核心思想是以树 状结构来表示那些嵌套数据。该内存模型能够有效的解决内存模型理论中类型转 换、指针与别名和大小不确定数据等难题。本文最后以 LLVM IR 指令集的一个核 心子集和 TMM 内存模型为基础并集成 SMT 求解器 Z3，实现了一个简单的符号执 行引擎 SSE（Simple symbolic execution engine），并通过实验验证了 SSE 和 TMM 的有效性和先进性。关键词：符号执行，内存模型，静态分析，Z3，LLVM ABSTRACT ABSTRACTWith the development of software technology, the software system is applied to all aspects of our lives. It bring us great convenience, but also bear us tremendous risks which caused by software vulnerabilities. Methods to guarantee software quality are a very urgent need. Those methods can be taked into two categories; one is static checking which usually used early stage to detect the potential vulnerabilities through analysis the source code, the other one is dynamic testing which through runing the binary code and checking the result. The sooner of bugs to be found, the smaller of modification costs. So the static checking is an important method to guarantee software quality. Among the static checking methods, symbolic execution for its high degree of accuracy received great attention.Symbolic execution is a context-sensitive path analysis method. In the case of computing resources sufficient enough, it can deeply analysis the program, and found some minor bugs. However, symbolic execution theory itself is also facing several major challenges which are the path explosion, constrain