（计算机软件与理论专业论文）基于pat树的符号执行工具的设计与实现.pdf

华中科技大学硕士学位论文 i 摘 要 随着软件产业的不断发展，程序的规模越来越大，完全依靠手工进行测试的难度 越来越大，这就需要一些辅助测试的自动化测试工具。自动化测试工具能够自动地分 析项目的源程序，自动地生成测试用例，并且达到一定的程序测试覆盖率，大大提高 软件的可靠性和正确性，并且节约大量的人力和时间。符号执行使用抽象的符号表示 程序中变量的值，来模拟程序的执行。符号执行的研究对于软件测试中测试用例的产 生方法和程序证明理论研究， 以及软件工程中逆向工程的研究都有重要的意义。 因此， 无论在软件工程的理论研究，还是在软件测试自动化的工程实践中，符号执行都有进 一步研究的价值。 目前国内外对符号执行进行了较深入的研究，并且已经开发出了一些工具。但是 符号执行的一些问题尚待解决，而且国内外缺乏针对 java 的符号执行工具。对数组的 处理和模块调用的处理，仍旧是 java 语言符号执行研究的难点。此外，java 语言是一 种面向对象的语言，其面向对象的复杂特性也增加了其符号执行研究的难度。 基于程序静态分析树 pat(program analysis tree)树的符号执行方法是一种自动化 的程序静态分析方法。该方法通过分析 java 源程序建立 pat 树。程序静态分析树能 够对 java 程序进行形式化的描述。基于程序静态分析树的遍历方法是一种基于 java 程序的逻辑结构的算法。此外，符号执行系统的程序基本结构处理策略、符号计算方 法和方法调用也是研究的重点，针对数组这个符号执行的难点也进行了相关的研究。 最后，通过一个针对 java 程序的符号执行工具 jse(java symbolic executor)分析表明 了基于 pat 树的符号执行在实践中的可行性。 关键字： 自动化测试，程序静态分析，符号执行，程序静态分析树 华中科技大学硕士学位论文 ii abstract with the rapid development of software industry, programs are becoming larger and much more complex than ever before. during the development of software, it is too difficult to test all the programs manually, so automatically testing tools are necessary to analysis programs. if the tools can analysis programs automatically, even generate test data automatically with high coverage of programs, the reliability of software will be improved dramatically and considerable resource will be saved. symbolic execution simulates execution of programs with symbols instead of real values. symbolic execution is a useful method for program testing and reverse engineering. many people have done a lot of research on symbolic execution. some symbolic execution tools have been developed. still there are some problems of symbolic execution need to be solved. first of all, no symbolic execution system of java program has been developed. secondly, solutions for array and module call are still difficulties of java symbolic execution. finally, the complexity of java increases the difficulty of the symbolic execution implement. the symbolic execution based on pat(program analysis tree) is an automatic program static analysis method, which can analysis the java program. also, a visiting method is designed for pat. moreover, some researches on symbolic execution have been done. at the end of this thesis, a symbolic execution tool called jse (java symbolic executor) is developed. key words: automatically testing, static analysis, symbolic execution, program analysis tree 3 独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研 究成果。尽我所知，除文中已经标明引用的内容外，本论文不包含任何其他个人或 集体已经发表或撰写过的研究成果。对本文的研究做出贡献的个人和集体，均已在 文中以明确方式标明。本人完全意识到，本声明的法律结果由本人承担。 学位论文作者签名： 日期： 2007 年 月 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：学校有权 保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅。 本人授权华中科技大学可以将本学位论文的全部或部分内容编入有关数据库进行检 索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。 保密 ，在_年解密后适用本授权书。 不保密。 （请在以上方框内打“” ） 学位论文作者签名： 指导教师签名： 日期：2007 年 月 日 日期：2007 年 月 日 本论文属于 华中科技大学硕士学位论文 1 1 绪论 本章首先介绍了软件测试中符号执行系统的研究背景、意义和主要研究内容，概 述了符号执行系统的任务、设计原则和实现难点，然后列举了迄今为止具有代表性的 系统和框架，以及它们的优缺点，接着指出了本文的研究重点：程序符号执行系统设 计与实现。最后指出其存在的不足，并提出了改进的方案。 1.1 研究背景 随着信息技术的飞速发展，软件产品应用到了人类社会生活中的各个领域，但是 各种软件故障也对社会带来了极大的经济损失，甚至产生了一定的破坏作用。特别是 对于安全关键系统(safety critical system，如民航订票系统、银行结算系统、自动飞行 控制软件、军事防御和核电站安全控制系统等) 对系统安全性有特殊的要求，而且软 件系统本身复杂度高。针对这种需求，以软件测试为中心的质量保障技术在软件生产 中得到了迅速的发展和应用，软件测试成为发现软件故障，保证软件质量，提高软件 可靠性的主要手段。有数据表明，软件测试在软件开发中所占用的时间和资源一般在 40%至 70%。随着软件技术不断发展，现代软件系统发展极其迅速，这就对软件测试 技术提出了更高的要求。软件测试技术的进步能够极大的减少软件工程中投入的时 间，人力和物力，因此对软件测试技术的研究显得尤其重要。 ieee 把软件测试定义为：从无限大的执行域中恰当地选取一组有限测试用例， 对照程序已经定义的预期行为，动态地检验程序的行为。实际上，软件测试是软件过 程的一个核心工作流，贯穿于整个软件开发过程始末。软件测试过程包含了测试计划 的制定、测试大纲的编写、测试用例的设计与生成、测试的实施、测试结果与问题的 分析和报告、以及软件测试的管理等工作。软件测试有两个基本要求，一是要验证程 序符合规约的要求；二是要证明此验证过程是可信的。前者强调软件测试是一个软件 验证工程，涵盖软件开发的各个方面，包括从需求说明到概要设计、详细设计乃至编 程和执行的所有阶段。具体来说软件测试需要检查系统的执行是否正确，包括三个方 面：功能方面程序必须能够完成约定的功能，例如实时性要求；输入和输出方面要求 程序对给定的输入须有正确的输出，包括例外情况；对外界的影响方面同具体的环境 华中科技大学硕士学位论文 2 有关，例如程序内存管理、文件管理，以及对其它应用程序的执行干扰等。对于后者， 测试需要一个充分性准则，表明到什么程度测试可以终止并取得可信的结果。程序规 约(specification)是测试的基础。规约一般在程序编写之前就己经明确并规定了程序应 该做什么。测试是在规则的指导下选择一系列测试用例，并在执行测试用例时观察程 序行为是否符合规约的要求。不是所有的程序规约和结构都必须被测试用例所覆盖， 因此需要一个程序的正确性定义和测试的充分性验证准则。 软件测试技术可以分为静态测试和动态测试1。静态测试是不执行程序代码而寻 找程序代码中可能存在的缺陷或评估程序代码的过程。动态测试通过在抽样测试数据 上运行程序来检验程序的动态行为和运行结果以发现缺陷。 测试也分为结构性测试(又 称白盒测试)、功能性测试(黑盒测试)、以及程序与规约相结合的测试(灰盒测试)。白 盒测试包括控制流测试和数据流测试两类主要技术以及域测试、符号执行(symbolic execution)、程序插桩和变异测试等其它技术。黑盒测试又包括：等价类划分、因果 图、判定表、边值分析、组合覆盖测试和状态测试等。灰盒测试综合考虑软件的规范 和程序的内部结构来生成测试数据。 静态测试中大量使用程序静态分析技术2。程序静态分析技术是指不编译运行待 测试程序，而是通过对程序源代码进行分析以发现其中的错误。程序静态分析的目标 不是证明程序完全正确，而是作为动态测试的补充，在程序运行前尽可能多的发现其 中隐含的错误，提高程序的可靠性和健壮性3。事实上在很多相当成熟的系统中包含 着错误，只凭测试人员手工很难找到这些错误，而通过静态测试发现了现存系统的很 多错误4 6。 程序静态分析的方法主要有以下几种： (1) 符号执行7,8。符号执行的基本思想是，用抽象的符号表示程序中变量的值， 来模拟程序的执行。该方法很好的克服了其他测试技术中不能确定程序中变量的值的 问题。符号执行常常使用于对路径敏感的程序分析中。符号执行结合约束求解方法理 论上可以精确地静态模拟程序的执行，因此约束求解工具的接受能力决定了分析程序 和发现错误的能力。 (2) 定理证明9。 自动定理证明是基于语意的程序分析特别是程序验证中常用到的 技术。但是采用消解原理的定理证明器一般并不适合于程序分析，通常使用各种判定 过程来判断公式是否为定理。 (3) 类型推导。类型推导指的是由机器自动地推导出程序中变量和函数的类型， 华中科技大学硕士学位论文 3 它的思想是将程序中的数据划分成不同的集合，再利用类型理论中的算法进行分析。 类型推导适用于控制流无关的分析，能够处理大规模的程序。 (4) 基于规则的检查。在面向不同应用的程序中，存在不同的编程规则。基于规 则的检查使用规则处理器，将规则转换成内部表示，将其应用于程序分析。基于规则 的分析方法的优点是能够针对不同的系统采用不同的规则进行分析。缺点是受到规则 描述机制的局限。 (5) 模型检测。模型检测是一种验证有限状态并发系统的方法。它是基于有限状 态系统构造和有向图等抽象模型的。它的难点在于如何避免状态空间的爆炸。 以上几种方法之间有一定的联系。类型推导和模型检测都是对程序的抽象。符号 执行和类型推导都有程序产生约束，只是约束的形式不同：符号执行的约束形式是布 尔表达式以及线性等式和不等式；类型推导的约束形式是集合关系表达式。上面这些 方法形式各异，各有相关的分析工具10 14，分别实现了各自的理论的将价值。 采用新型的编程语言和开发方式，可以极大的提高软件系统的开发效率，同时也 能明显减少错误的引入。java 语言是当今一种主流的软件系统开发语言，具有较高的 可靠性。 java 使用早期问题检查机制和运行时检查机制，并且 java 的语言模型避免了 拙劣的指针和内存分配错误导致的内存泄漏错误。其次， java 被设计用于网络/分布式 环境，具有一定的安全机制，比如禁止运行时堆栈溢出，禁止破坏运行空间外内存等。 但是 java 语言仍旧无法避免程序设计错误等原因带来的软件错误，例如逻辑错误。因 此，有必要对 java 语言软件测试技术进行一定的研究。 1.2 符号执行系统的意义 符号执行15 (symbolic execution)的思想早已提出。符号执行的基本思想是：用抽 象的符号表示程序中变量的值，来模拟程序的执行。该方法很好地克服了在静态测试 时不能确定程序中变量的值的问题。符号执行常常在对路径敏感的程序分析16,17中使 用。 对符号执行的研究也有很多。通常意义下的程序执行是给出具体的输入数据使得 程序能够沿着某一特定路径执行并输出与之对应的具体结果。然而符号执行的目的在 于分析程序中变量之间的约束关系，不需要指定具体的输入数据，将变量作为代数中 的抽象符号处理，结合程序的约束条件进行推理，结果是输出一些描述变量间关系的 华中科技大学硕士学位论文 4 表达式。 在符号执行的过程中， 控制流图中的分支导致了对于变量的不同的约束条件， 而这些约束条件就描述了相应路径的测试数据间的约束关系。 符号执行的研究无论是对软件工程本身的研究，还是对实际工程中测试技术的发 展，都有比较重要的意义18,19。首先，符号执行和约束求解方法的研究产生了基于符 号执行和约束求解的测试用例产生标准和方法20。其次，符号执行方法的研究中对于 从代码还原状态图的研究对软件工程中的逆向工程有较大的促进作用。此外，对于软 件测试的程序证明(program proving)理论的研究也有重要的意义21。 具体来说符号执行的应用主要有以下几个方面： 1. 产生测试用例 符号执行最重要的一个应用就是可以自动生成测试用例22 24。 符号执行输入符号 值和路径选择，然后符号执行程序的选定路径，得到符号执行的结果以及路径选择条 件集合。对于软件测试来说，可以使用真实值代替符号输入，那么所选用的真实值就 是一组测试数据。 其中， 真实值产生的依据就是符号执行程序某路径的路径选择条件。 因此，我们在软件测试中，可以利用符号执行，设计一些自动生成工具，遍历符号的 执行路径，根据不同路径的选择条件，自动的产生测试用例，而且使用这种产生测试 用例的方法，测试的覆盖率很高25。 2. 程序证明 最著名的程序证明26方法是由 floyd 提出基于断言机制的“诱导断言确认法” 。 该方法将断言设置在程序模块的开始和结尾，那么判断一个模块或者一段程序正确与 否的标准就是模块开始处的断言必须要保证模块结束处断言的正确性，否则程序模块 出现错误。例如在某个程序中要求变量 a 满足 a4 且 a=n) r=r- n; q=q+1; 华中科技大学硕士学位论