基于PAT树的符号执行工具的设计与实现(提交图书馆).docx
《基于PAT树的符号执行工具的设计与实现(提交图书馆).docx》由会员分享,可在线阅读,更多相关《基于PAT树的符号执行工具的设计与实现(提交图书馆).docx(56页珍藏版)》请在三一办公上搜索。
1、分 类 号 学 号2005612100139 学校代码 10487 密 级 硕士学位论文基于PAT树的符号执行工具的设计与实现学位申请人: 黄 晋学科专业: 计算机软件与理论指导教师: 卢 炎 生 教 授答辩日期: 2007年6月2日A Thesis Submitted in Partial Fulfillment of the Requirements for the Degree of Master of EngineeringA Symbolic Execution Tool based on Program Analysis TreeCandidate :Huang JinMajor
2、:Computer Software and TheorySupervisor :Prof. Lu YanshengHuazhong University of Science and TechnologyWuhan 430074, P. R. ChinaJun., 2007独创性声明本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知,除文中已经标明引用的内容外,本论文不包含任何其他个人或集体已经发表或撰写过的研究成果。对本文的研究做出贡献的个人和集体,均已在文中以明确方式标明。本人完全意识到,本声明的法律结果由本人承担。 学位论文作者签名: 日期:2007年
3、 月 日学位论文版权使用授权书本学位论文作者完全了解学校有关保留、使用学位论文的规定,即:学校有权保留并向国家有关部门或机构送交论文的复印件和电子版,允许论文被查阅和借阅。本人授权华中科技大学可以将本学位论文的全部或部分内容编入有关数据库进行检索,可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。本论文属于 保密 ,在_年解密后适用本授权书。不保密。(请在以上方框内打“”)学位论文作者签名: 指导教师签名:日期:2007 年 月 日 日期:2007年 月 日摘 要随着软件产业的不断发展,程序的规模越来越大,完全依靠手工进行测试的难度越来越大,这就需要一些辅助测试的自动化测试工具。自动化测
4、试工具能够自动地分析项目的源程序,自动地生成测试用例,并且达到一定的程序测试覆盖率,大大提高软件的可靠性和正确性,并且节约大量的人力和时间。符号执行使用抽象的符号表示程序中变量的值,来模拟程序的执行。符号执行的研究对于软件测试中测试用例的产生方法和程序证明理论研究,以及软件工程中逆向工程的研究都有重要的意义。因此,无论在软件工程的理论研究,还是在软件测试自动化的工程实践中,符号执行都有进一步研究的价值。目前国内外对符号执行进行了较深入的研究,并且已经开发出了一些工具。但是符号执行的一些问题尚待解决,而且国内外缺乏针对Java的符号执行工具。对数组的处理和模块调用的处理,仍旧是Java语言符号执
5、行研究的难点。此外,Java语言是一种面向对象的语言,其面向对象的复杂特性也增加了其符号执行研究的难度。基于程序静态分析树PAT(Program Analysis Tree)树的符号执行方法是一种自动化的程序静态分析方法。该方法通过分析Java源程序建立PAT树。程序静态分析树能够对Java程序进行形式化的描述。基于程序静态分析树的遍历方法是一种基于Java程序的逻辑结构的算法。此外,符号执行系统的程序基本结构处理策略、符号计算方法和方法调用也是研究的重点,针对数组这个符号执行的难点也进行了相关的研究。最后,通过一个针对Java程序的符号执行工具JSE(Java Symbolic Execut
6、or)分析表明了基于PAT树的符号执行在实践中的可行性。关键字: 自动化测试,程序静态分析,符号执行,程序静态分析树AbstractWith 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
7、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
8、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 nee
9、d 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 ex
10、ecution 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 JS
11、E (Java Symbolic Executor) is developed. Key words: Automatically Testing, Static Analysis, Symbolic Execution, Program Analysis Tree目 录摘 要IABSTRACTII1 绪 论 1.1 研究背景(1)1.2 符号执行系统的意义(3)1.3 符号执行系统的研究现状(5)1.4 论文的组织结构(8)2 符号执行系统JSE2.1 符号执行系统概述(9)2.2 符号执行系统架构(10)2.3 小结(13)3 JAVA程序静态分析技术3.1程序静态分析(15)3.2程序静
12、态分析树(16)3.3 小结(22)4 基于PAT树的符号执行技术4.1控制流图(23)4.2基于PAT树的符号执行方法(25)4.3 小结(32)5 符号执行系统测试5.1测试环境(33)5.2功能测试(33)5.3 小结(39)6 总结及未来的工作6.1本文总结(40)6.2进一步工作(40)致 谢(42)参考文献(44)1 绪论本章首先介绍了软件测试中符号执行系统的研究背景、意义和主要研究内容,概述了符号执行系统的任务、设计原则和实现难点,然后列举了迄今为止具有代表性的系统和框架,以及它们的优缺点,接着指出了本文的研究重点:程序符号执行系统设计与实现。最后指出其存在的不足,并提出了改进的
13、方案。1.1 研究背景随着信息技术的飞速发展,软件产品应用到了人类社会生活中的各个领域,但是各种软件故障也对社会带来了极大的经济损失,甚至产生了一定的破坏作用。特别是对于安全关键系统(Safety Critical System,如民航订票系统、银行结算系统、自动飞行控制软件、军事防御和核电站安全控制系统等) 对系统安全性有特殊的要求,而且软件系统本身复杂度高。针对这种需求,以软件测试为中心的质量保障技术在软件生产中得到了迅速的发展和应用,软件测试成为发现软件故障,保证软件质量,提高软件可靠性的主要手段。有数据表明,软件测试在软件开发中所占用的时间和资源一般在40%至70%。随着软件技术不断发
14、展,现代软件系统发展极其迅速,这就对软件测试技术提出了更高的要求。软件测试技术的进步能够极大的减少软件工程中投入的时间,人力和物力,因此对软件测试技术的研究显得尤其重要。IEEE把软件测试定义为:从无限大的执行域中恰当地选取一组有限测试用例,对照程序已经定义的预期行为,动态地检验程序的行为。实际上,软件测试是软件过程的一个核心工作流,贯穿于整个软件开发过程始末。软件测试过程包含了测试计划的制定、测试大纲的编写、测试用例的设计与生成、测试的实施、测试结果与问题的分析和报告、以及软件测试的管理等工作。软件测试有两个基本要求,一是要验证程序符合规约的要求;二是要证明此验证过程是可信的。前者强调软件测
15、试是一个软件验证工程,涵盖软件开发的各个方面,包括从需求说明到概要设计、详细设计乃至编程和执行的所有阶段。具体来说软件测试需要检查系统的执行是否正确,包括三个方面:功能方面程序必须能够完成约定的功能,例如实时性要求;输入和输出方面要求程序对给定的输入须有正确的输出,包括例外情况;对外界的影响方面同具体的环境有关,例如程序内存管理、文件管理,以及对其它应用程序的执行干扰等。对于后者,测试需要一个充分性准则,表明到什么程度测试可以终止并取得可信的结果。程序规约(Specification)是测试的基础。规约一般在程序编写之前就己经明确并规定了程序应该做什么。测试是在规则的指导下选择一系列测试用例,
16、并在执行测试用例时观察程序行为是否符合规约的要求。不是所有的程序规约和结构都必须被测试用例所覆盖,因此需要一个程序的正确性定义和测试的充分性验证准则。软件测试技术可以分为静态测试和动态测试1。静态测试是不执行程序代码而寻找程序代码中可能存在的缺陷或评估程序代码的过程。动态测试通过在抽样测试数据上运行程序来检验程序的动态行为和运行结果以发现缺陷。测试也分为结构性测试(又称白盒测试)、功能性测试(黑盒测试)、以及程序与规约相结合的测试(灰盒测试)。白盒测试包括控制流测试和数据流测试两类主要技术以及域测试、符号执行(Symbolic Execution)、程序插桩和变异测试等其它技术。黑盒测试又包括
17、:等价类划分、因果图、判定表、边值分析、组合覆盖测试和状态测试等。灰盒测试综合考虑软件的规范和程序的内部结构来生成测试数据。静态测试中大量使用程序静态分析技术2。程序静态分析技术是指不编译运行待测试程序,而是通过对程序源代码进行分析以发现其中的错误。程序静态分析的目标不是证明程序完全正确,而是作为动态测试的补充,在程序运行前尽可能多的发现其中隐含的错误,提高程序的可靠性和健壮性3。事实上在很多相当成熟的系统中包含着错误,只凭测试人员手工很难找到这些错误,而通过静态测试发现了现存系统的很多错误46。程序静态分析的方法主要有以下几种:(1) 符号执行7,8。符号执行的基本思想是,用抽象的符号表示程
18、序中变量的值,来模拟程序的执行。该方法很好的克服了其他测试技术中不能确定程序中变量的值的问题。符号执行常常使用于对路径敏感的程序分析中。符号执行结合约束求解方法理论上可以精确地静态模拟程序的执行,因此约束求解工具的接受能力决定了分析程序和发现错误的能力。(2) 定理证明9。自动定理证明是基于语意的程序分析特别是程序验证中常用到的技术。但是采用消解原理的定理证明器一般并不适合于程序分析,通常使用各种判定过程来判断公式是否为定理。(3) 类型推导。类型推导指的是由机器自动地推导出程序中变量和函数的类型,它的思想是将程序中的数据划分成不同的集合,再利用类型理论中的算法进行分析。类型推导适用于控制流无
19、关的分析,能够处理大规模的程序。(4) 基于规则的检查。在面向不同应用的程序中,存在不同的编程规则。基于规则的检查使用规则处理器,将规则转换成内部表示,将其应用于程序分析。基于规则的分析方法的优点是能够针对不同的系统采用不同的规则进行分析。缺点是受到规则描述机制的局限。(5) 模型检测。模型检测是一种验证有限状态并发系统的方法。它是基于有限状态系统构造和有向图等抽象模型的。它的难点在于如何避免状态空间的爆炸。以上几种方法之间有一定的联系。类型推导和模型检测都是对程序的抽象。符号执行和类型推导都有程序产生约束,只是约束的形式不同:符号执行的约束形式是布尔表达式以及线性等式和不等式;类型推导的约束
20、形式是集合关系表达式。上面这些方法形式各异,各有相关的分析工具1014,分别实现了各自的理论的将价值。采用新型的编程语言和开发方式,可以极大的提高软件系统的开发效率,同时也能明显减少错误的引入。Java语言是当今一种主流的软件系统开发语言,具有较高的可靠性。Java使用早期问题检查机制和运行时检查机制,并且Java的语言模型避免了拙劣的指针和内存分配错误导致的内存泄漏错误。其次,Java被设计用于网络/分布式环境,具有一定的安全机制,比如禁止运行时堆栈溢出,禁止破坏运行空间外内存等。但是Java语言仍旧无法避免程序设计错误等原因带来的软件错误,例如逻辑错误。因此,有必要对Java语言软件测试技
21、术进行一定的研究。1.2 符号执行系统的意义符号执行15 (symbolic execution)的思想早已提出。符号执行的基本思想是:用抽象的符号表示程序中变量的值,来模拟程序的执行。该方法很好地克服了在静态测试时不能确定程序中变量的值的问题。符号执行常常在对路径敏感的程序分析16,17中使用。对符号执行的研究也有很多。通常意义下的程序执行是给出具体的输入数据使得程序能够沿着某一特定路径执行并输出与之对应的具体结果。然而符号执行的目的在于分析程序中变量之间的约束关系,不需要指定具体的输入数据,将变量作为代数中的抽象符号处理,结合程序的约束条件进行推理,结果是输出一些描述变量间关系的表达式。在
22、符号执行的过程中,控制流图中的分支导致了对于变量的不同的约束条件,而这些约束条件就描述了相应路径的测试数据间的约束关系。符号执行的研究无论是对软件工程本身的研究,还是对实际工程中测试技术的发展,都有比较重要的意义18,19。首先,符号执行和约束求解方法的研究产生了基于符号执行和约束求解的测试用例产生标准和方法20。其次,符号执行方法的研究中对于从代码还原状态图的研究对软件工程中的逆向工程有较大的促进作用。此外,对于软件测试的程序证明(program proving)理论的研究也有重要的意义21。具体来说符号执行的应用主要有以下几个方面:1. 产生测试用例符号执行最重要的一个应用就是可以自动生成
23、测试用例2224。符号执行输入符号值和路径选择,然后符号执行程序的选定路径,得到符号执行的结果以及路径选择条件集合。对于软件测试来说,可以使用真实值代替符号输入,那么所选用的真实值就是一组测试数据。其中,真实值产生的依据就是符号执行程序某路径的路径选择条件。因此,我们在软件测试中,可以利用符号执行,设计一些自动生成工具,遍历符号的执行路径,根据不同路径的选择条件,自动的产生测试用例,而且使用这种产生测试用例的方法,测试的覆盖率很高25。2. 程序证明最著名的程序证明26方法是由Floyd提出基于断言机制的“诱导断言确认法”。该方法将断言设置在程序模块的开始和结尾,那么判断一个模块或者一段程序正
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 基于 PAT 符号 执行 工具 设计 实现 提交 图书馆
链接地址:https://www.31ppt.com/p-1729263.html