基于PAT树的符号执行工具的设计与实现.docx

上传人:小飞机 文档编号:1729268 上传时间:2022-12-16 格式:DOCX 页数:56 大小:602.40KB
返回 下载 相关 举报
基于PAT树的符号执行工具的设计与实现.docx_第1页
第1页 / 共56页
基于PAT树的符号执行工具的设计与实现.docx_第2页
第2页 / 共56页
基于PAT树的符号执行工具的设计与实现.docx_第3页
第3页 / 共56页
基于PAT树的符号执行工具的设计与实现.docx_第4页
第4页 / 共56页
基于PAT树的符号执行工具的设计与实现.docx_第5页
第5页 / 共56页
点击查看更多>>
资源描述

《基于PAT树的符号执行工具的设计与实现.docx》由会员分享,可在线阅读,更多相关《基于PAT树的符号执行工具的设计与实现.docx(56页珍藏版)》请在三一办公上搜索。

1、分 类 号 学 号2005612100139 学校代码 10487 密 级 硕士学位论文基于PAT树的符号执行工具的设计与实现学位申请人: 黄 晋学科专业: 计算机软件与理论指导教师: 卢 炎 生 教 授答辩日期: 2007年6月2日4A 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的符号执行工具。对数组的处理和模块调用的处理

5、,仍旧是Java语言符号执行研究的难点。此外,Java语言是一种面向对象的语言,其面向对象的复杂特性也增加了其符号执行研究的难度。基于程序静态分析树PAT(Program Analysis Tree)树的符号执行方法是一种自动化的程序静态分析方法。该方法通过分析Java源程序建立PAT树。程序静态分析树能够对Java程序进行形式化的描述。基于程序静态分析树的遍历方法是一种基于Java程序的逻辑结构的算法。此外,符号执行系统的程序基本结构处理策略、符号计算方法和方法调用也是研究的重点,针对数组这个符号执行的难点也进行了相关的研究。最后,通过一个针对Java程序的符号执行工具JSE(Java Sy

6、mbolic Executor)分析表明了基于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 automatic

7、ally 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 simulat

8、es 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

9、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.Th

10、e 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 t

11、ool called JSE (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程序静

12、态分析(15)3.2程序静态分析树(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)481 绪论本章首先介绍了软件测试中符号执行系统的研究背景、意义和主要研究内容,概述了符号执行系统的任务、设计原则和实现难点,然后列举了迄今为止具有代表性的系统和框架,以及它们的优缺点,接着指出了本文的研究重点:程序符号执行系统设计与实现。最后指

13、出其存在的不足,并提出了改进的方案。1.1 研究背景随着信息技术的飞速发展,软件产品应用到了人类社会生活中的各个领域,但是各种软件故障也对社会带来了极大的经济损失,甚至产生了一定的破坏作用。特别是对于安全关键系统(Safety Critical System,如民航订票系统、银行结算系统、自动飞行控制软件、军事防御和核电站安全控制系统等) 对系统安全性有特殊的要求,而且软件系统本身复杂度高。针对这种需求,以软件测试为中心的质量保障技术在软件生产中得到了迅速的发展和应用,软件测试成为发现软件故障,保证软件质量,提高软件可靠性的主要手段。有数据表明,软件测试在软件开发中所占用的时间和资源一般在40

14、%至70%。随着软件技术不断发展,现代软件系统发展极其迅速,这就对软件测试技术提出了更高的要求。软件测试技术的进步能够极大的减少软件工程中投入的时间,人力和物力,因此对软件测试技术的研究显得尤其重要。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语言仍旧无法避免程序设计错误等原因带来的软件错误,例如逻辑错误。因此,

21、有必要对Java语言软件测试技术进行一定的研究。1.2 符号执行系统的意义符号执行15 (symbolic execution)的思想早已提出。符号执行的基本思想是:用抽象的符号表示程序中变量的值,来模拟程序的执行。该方法很好地克服了在静态测试时不能确定程序中变量的值的问题。符号执行常常在对路径敏感的程序分析16,17中使用。对符号执行的研究也有很多。通常意义下的程序执行是给出具体的输入数据使得程序能够沿着某一特定路径执行并输出与之对应的具体结果。然而符号执行的目的在于分析程序中变量之间的约束关系,不需要指定具体的输入数据,将变量作为代数中的抽象符号处理,结合程序的约束条件进行推理,结果是输出

22、一些描述变量间关系的表达式。在符号执行的过程中,控制流图中的分支导致了对于变量的不同的约束条件,而这些约束条件就描述了相应路径的测试数据间的约束关系。符号执行的研究无论是对软件工程本身的研究,还是对实际工程中测试技术的发展,都有比较重要的意义18,19。首先,符号执行和约束求解方法的研究产生了基于符号执行和约束求解的测试用例产生标准和方法20。其次,符号执行方法的研究中对于从代码还原状态图的研究对软件工程中的逆向工程有较大的促进作用。此外,对于软件测试的程序证明(program proving)理论的研究也有重要的意义21。具体来说符号执行的应用主要有以下几个方面:1. 产生测试用例符号执行最

23、重要的一个应用就是可以自动生成测试用例2224。符号执行输入符号值和路径选择,然后符号执行程序的选定路径,得到符号执行的结果以及路径选择条件集合。对于软件测试来说,可以使用真实值代替符号输入,那么所选用的真实值就是一组测试数据。其中,真实值产生的依据就是符号执行程序某路径的路径选择条件。因此,我们在软件测试中,可以利用符号执行,设计一些自动生成工具,遍历符号的执行路径,根据不同路径的选择条件,自动的产生测试用例,而且使用这种产生测试用例的方法,测试的覆盖率很高25。2. 程序证明最著名的程序证明26方法是由Floyd提出基于断言机制的“诱导断言确认法”。该方法将断言设置在程序模块的开始和结尾,

24、那么判断一个模块或者一段程序正确与否的标准就是模块开始处的断言必须要保证模块结束处断言的正确性,否则程序模块出现错误。例如在某个程序中要求变量A满足A4且A10,那么我们将断言插入程序中。在符号执行过程中,我们可以将路径执行条件加入程序的断言中去。当一个断言中包含路径选择条件的程序符号执行时,如果路径选择条件与断言一致,那么可以发现程序该路径是可达的。反之,如果路径选择条件与断言矛盾,可以很容易的发现路径是不可达的。3. 符号调试符号执行本身可以模拟程序的执行过程,因此符号执行可以用于程序的调试7技术。通常意义上的程序跟踪调试只能跟踪显示程序运行过程中变量的当前真实值。但是一个基于符号执行的调

25、试工具能够跟踪显示变量的符号表达式,这样变量的意义就更加明显。1.3 符号执行系统的研究现状对于符号执行的研究,目前不仅已经有了一定的理论成果2729,而且还针对各种语言开发出了许多的工具3032。本节主要介绍几个有代表性的系统,并针对各个系统进行相应的评价。1.3.1 交互符号执行系统EFFIGYEFFIGY是一个由IBM Thomas J. Watson Research Center的James C. King等人研发的符号执行系统,针对程序的调试和测试的交互性符号执行器(Interactive Symbolic Executor),能处理PL/I型语言的程序。EFFIGY是第一个使用符

26、号执行的系统。它利用符号执行的特性,用于程序的开发和测试。该系统具有一定的适应性,其最大的特点是具有一定的交互性。符号执行可以得到程序路径的符号结果,并且在系统中逐行显示变量的符号值。EFFIGY功能上最大的诟病在于没有提供一个程序路径的流程图,这样不便于使用者确定路径的执行情况。同时,它没有提供一个路径选择的策略,而必须由使用者制定测试的策略,选则路径,例如每一次循环,都要选择是否继续循环。这样就加大了使用者的工作量。该系统没有直接提出模块调用的处理方法。对于数组和指针,该系统也没有涉及。1.3.2 功能全面的符号执行系统SELECT这个试验系统主要实现的功能包括:符号执行程序遍历所有可能的

27、程序路径;简化符号执行结果;自动产生测试用例;用于程序的符号调试。SELECT具有一定的判断程序路径可达性的能力。这个系统本身就是设计用于根据设定的算法自动产生路径选择策略,从而使得符号执行能够覆盖程序的每一个分支。随着符号执行的进行,每添加一条程序分支,就计算程序分支的路径选择条件,进而判断路径的可达性。SELECT的分析器能够处理线性和非线性的不等式,并且根据结果产生测试用例。对于存在大量循环的程序的处理,SELECT使用交互性的策略,根据使用者的需求设定循环的次数,然后系统自动更新路径选择条件和变量的符号表达式,知道循环结束。SELECT使用预备策略处理模块调用。当模块满足复用的条件时,

28、即不存在不确定的过程,例如循环,那么在符号执行前单独处理每一个子模块,记录下符号执行结果和路径选择条件。当子模块被调用时,直接使用子模块的处理结果。但是这样会导致程序可选择路径的数量爆炸,影响符号执行的运行效率。1.3.3 单元测试引擎CUTECUTE33是近年来出现的一个针对C语言和Java语言的单元测试工具。该工具能够系统的自动的测试面向过程的C语言(包含指针)和并行的Java程序。CUTE结合了具体执行和符号执行的优点,避免了随机测试的低效性。CUTE通过具体执行和符号执行相结合的方式执行待测程序。它的符号执行的方式区别传统的符号执行方式,符号执行是在程序具体执行的基础上进行的。在CUT

29、E的执行过程当中,收集程序执行路径的路径选择条件,在程序某条路径的结尾,处理收集到的一组符号约束条件,产生该路径的测试用例。CUTE的算法首先随机产生一个具体的输入,然后循环执行以下过程:(1) 使用产生的输入执行代码,同时计算路径符号约束条件;(2) 如果遇到程序分支,随机产生一个具体输入;(3) 如果当前程序分支执行完成,那么退回前一个分支节点,处理路径的符号约束,计算出执行该分支节点的其他未执行路径的具体输入值。CUTE采用了深度优先遍历的策略,遍历了整个程序的分支。更重要的是,算法使用的是具体值来执行程序,因此发现的程序错误具有较高的可信度。为了验证CUTE的正确性,进行了相关的测试实

30、验。一个是比较流行的用C语言编写的数据结构库SGLIB,另一个是著名的Sun公司在JDK1.4中被广泛使用的安全的线程收集框架。使用CUTE对SGLIB进行单元测试,在三秒钟内发现了两个错误。一个错误是在一个双链表库中发现的,一个非空的链表链接到了一空链表中去了。另一个错误是一个死循环。后来SGLIB的开发者证实了错误的存在。使用JCUTE对安全的线程收集框架进行测试,意外的发现了潜在的多线程之间的竞争,死锁,不能被捕获的异常和死循环。这再一次的证明了CUTE的算法的正确性。1.3.4现有研究总结对于符号执行研究的难点,国内外的许多学者有了一些初步的研究。国内特别是中科院的张健等研究员对于符号

31、执行的指针,结构变量,路径可达性问题和约束求解问题有一定的研究。具体来说,符号执行研究存在的主要难题有以下四个:1. 循环(loop)的处理如果程序中循环7的次数是未知的,或者说是动态的取决于程序的输入或者状态,那么符号执行是无法获知执行的路径的,会造成符号执行处理过程复杂化。如果循环次数太多,那么符号执行也是不可行的。因此对于循环,主要采取交互式的方式,手动设置循环次数上限或者交互式设置循环次数,处理符号执行中的循环执行次数不确定的问题。2. 模块调用 (module call)的处理程序中存在着大量的模块调用7,如函数的调用。但是这样的调用会造成符号执行处理过程的爆炸34,那么对于符号执行

32、也是不可行的。处理符号执行中的模块调用主要有两种策略:动态扩展策略和预处理策略。前者在对某个模块符号执行时,实时地对某个模块进行符号执行,它的优点是符号执行过程灵活,且存储空间需求低,但是消耗了一定的执行时间。后者在针对某个程序符号执行时前,已经将所有模块进行了符号执行,并将符号执行的结果纪录下来,以后在符号执行过程中如果需要调用模块,只需要调用该模块的符号执行结果。它的优点是一次执行,永久使用。但是它不适用于存在不确定元素,如循环和数组的模块,灵活性差,且对于大型程序,占用大量的存储空间。3. 数组(array)的处理对于数组35,如果程序中出现了下标是变量的数组成员,比如Ai,其中i是一个

33、变量,那么符号执行时,对Ai的操作,比如赋值,处理起来就会十分复杂。对数组元素的混淆,已经提出了一种处理符号执行中数组元素混淆的方法,通过转换存在数组元素混淆的代码段,可以被一般的符号执行工具识别。此外,中科院软件所的张健提出了基于形式转换的处理数组和指针的方法,设计了工具PAT,实现了对数组和指针元素的操作。4. 不可达路径 (infeasible path)的处理符号执行研究中的不可达路径问题36,37实际上是基于约束性问题38的。由于程序中存在着大量的不可达路径,符号执行揭示这些不可达路径,从而测试程序分支的正确性。因此,对不可达路径的研究也是十分有意义的。目前中科院的张健对此进行了一定

34、的研究,给出了分离路径执行条件和针对整形和布尔型的线性条件约束求解的方法,提出了基于程序流图的搜索算法,并且实现了约束求解工具BoNuS2。1.4 论文的组织结构本文符号执行系统的研究与实现分为理论研究和技术实现这两个方面。理论研究的主要内容包括建立程序静态分析的中间表示模型和建立描述符号执行的行为模型。符号执行系统的技术实现包括Java程序静态分析技术、符号计算技术和可视化技术。基于上述研究内容,本文各章的内容安排如下:第1章概述了符号执行系统的研究背景,然后介绍了研究符号执行的意义、主要任务、设计原则以及实现难点,最后讲述未来发展方向和本论文的研究内容。第2章介绍了符号执行系统JSE的整体

35、结构,包括其层次结构和各个组成模块的主要功能,然后描述了符号执行的工作流程。第3章主要提出了符号执行系统静态分析中信息提取的需求,阐释了JSE的代码信息提取框架,分析了其对应的信息提取策略。JSE的信息提取框架极大优化了信息存储结构,而其对应的信息提取策略较好的改进了信息提取的方式和效率。第4章主要针对符号执行的特点和难点,提出了相应的解决策略和算法;同时,针对模块调用产生的超大规模问题,提出了灵活分类机制,并通过高效的数据分类算法和模块处理算法对其进行了实现。第5章系统测试包括功能测试和性能测试。针对JSE的信息提取策略,测试了符号执行的信息提取效果,包括多种代码静态信息的显示,程序变量的符

36、号表达式的实时更新,程序的路径可达性的等。针符号执行中处理模块调用的不同机制,在符号执行程序效率方面,分别比较了简单策略和优化策略两种情况下的性能,最终证实了该理论研究的可行性和有效性。第6章对全文进行总结并展望了未来的工作。主要对信息提取策略和符号执行优化策略进行了评价,并初步规划了在该研究领域的未来的改进方案。最后是致谢和参考文献。2 符号执行系统JSE在分析了现有符号执行系统的优缺点之后,针对Java语言的特点,设计了Java语言的符号执行系统JSE(Java Symbolic Executor)。本章简要描述了JSE的系统构架、工作流程和用户实例,说明了该系统在构架上具有清晰的层次和良

37、好的可扩展性。2.1 符号执行系统概述针对Java语言的符号执行工具JSE能够模拟程序执行,并且用抽象的符号表示程序中变量的值。该方法可以对Java这种路径敏感语言使用,并且能够克服在其他静态测试时不能确定程序中变量的值的问题。JSE的实现主要有以下三个方面的意义:(1) 提供一个针对Java语言的程序静态分析架构。不同于已有的基于某种语言提供断言机制的符号执行技术,JSE的研究基础实质上是Java源程序的静态分析技术,类似于程序的编译技术。它是一种底层的技术,通过分析代码的成分,各种成分之间的关系,然后产生一个适用于符号执行的框架结构,从而进行符号执行。从这一点上来说,现有的编译技术可以给系

38、统设计以很好的启发。(2) 符号调试方法。符号执行本身可以模拟程序的执行过程,因此符号执行可以用于程序的调试技术。通常意义上的程序跟踪调试只能跟踪显示程序运行过程中变量的当前真实值。但是一个基于符号执行的调试工具能够跟踪显示变量的符号表达式,这样变量的意义就更加明显。因此,符号执行运用于调试技术也是很有意义的。(3) 为今后进一步的相关研究奠定坚实的理论和实践基础。对于软件测试,符号执行系统的研究可以产生测试用例,并且相对于随机测试等其他的方法,产生的测试用例的覆盖率要高出很多。对于程序证明等理论研究,符号执行提供了一个形式化工具,为程序证明提供了强有力的试验工具。JSE的基础就是对程序进行使

39、用一定的静态分析技术进行一定的处理,并通过灵活、可靠的框架将这些数据汇聚、结构化并用于符号执行。系统能保证正确和全面地提取信息,并且满足系统高效、可扩展性和健壮性的要求。2.2 符号执行系统架构2.2.1主体框架结构系统基于Java的访问者(Visitor)模型,提供了一系列代码分析功能。系统模块结构如图2.1所示。图中标识了JSE的两个主要逻辑层:静态分析层和应用层。静态分析层主要负责Java源程序的预处理和静态分析,生成PAT树和源程序文本对象;应用层主要实现了基于PAT树的符号执行功能,此外还实现了PAT树和Java源程序文本的可视化功能。各种功能各司其职,互相协作,保证符号执行系统功能

40、完善、结构清晰,并具有良好的可维护性。图2.1 JSE系统模块框架图静态分析层分析源程序,得到程序的一个中间形式程序静态分析树。虽然由源程序直接实现应用层的功能是可行的,甚至更高效,但是使用中间形式,可以实现分析程序与符号执行应用的逻辑独立性,能够比较容易的实现面向不同应用和不同语言的符号执行系统。在不改变符号执行前端代码分析程序的情况下为新的应用构造一个新的应用框架。同样对于一个新的语言,在不改变已有应用框架的情况下,为新的语言构造一个分析该语言的分析程序,就可以构造出新语言的符号执行系统。使用中间形式的主要缺点是:中间形式的生成相比不使用中间形式的应用在效率上会有所降低,这是因为中间形式需

41、要再一次的处理才能生成符号执行所需目标结构。程序的中间形式常见的是树形表示,如图2.2所示。树形表示是一种最常见的表示方式,它最大的优点就是能够反映出程序的自然层次结构,而且能够满足应用的需求。程序分析树在程序分析和提取符号执行有效信息之间建立了一个清晰的接口。WXYZ图2.2程序分析树应用层主要实现符号执行和可视化这两个方面的功能,它的实现是基于程序分析树及其遍历算法组成的数据结构框架的。结构化显示程序元素的功能主要通过遍历程序分析树,提取出相关的信息,然后通过图形用户接口显示。符号执行功能首先提取符号执行有效信息,然后进行相关的处理。图2.3描述了符号执行JSE的执行模型。图2.3 原型系

42、统JSE执行模型2.2.2系统模块设计符号执行系统JSE的主要任务是符号执行Java源程序,并实现可视化功能。下面对设计的模块作总体性的介绍:1. 静态分析模块在原型系统中,采用开源项目eclipse的JDT(Java Development Tool)对Java源程序进行静态分析,静态分析的主要功能包括词法分析和改进的语法分析。词法分析是将Java惯用的词法如关键字、专用符号、注释、标识符、数字等终结符划分出来作为语法分析的输入;语法分析的任务是对词法分析的结果进行语义分析,产生抽象语法树。进一步地产生类结构信息表、函数、语句列表等。语法分析是识别程序结构的过程,通常采用递归下降法,具体做法

43、是将语法规则的每一项都写成一个处理函数,分析过程中采用向前看一个语言单元,判断所处的状态并调用相应的处理函数。JSE的语法分析经过改进,加入了针对符号执行系统的PAT树语法,并在抽象语法树的基础上,使用Java的合成模式,生成了针对符号执行的程序静态分析树。此外,静态分析模块还使用JDT生成的文本对象,实现了对代码文本副本的辅助操作功能。2. 符号执行模块符号执行模块是应用层的主要功能模块,也是原型系统的核心模块。符号执行模块的输入是PAT树,核心方法是PAT树的遍历方法,输出的符号执行结果。符号执行的主要流程是:首先遍历根据程序生成PAT树,生成变量列表;然后使用路径控制模块控制模拟程序执行

44、的执行路径,每当遇到分支时,与用户进行交互,根据用户的选择从而选择执行的路径,并且记录路径选择条件;每当执行到需要符号执行的语句时,就对相应的变量进行符号计算,然后更新变量列表,将符号计算结果输入变量列表。符号执行模块包括四个子模块:(1) PAT树遍历功能模块。针对基于Java的合成模式构造的PAT树,采用访问者模式设计PAT树的遍历功能。该遍历功能能够遍历Java语言的各种语法结构,如类文件、包声明、import声明、类声明、类结构体、变量声明、类的方法、if结构、while结构、赋值语句和中缀表达式等结构。(2) 变量列表相关功能模块。变量列表主要内容包括变量名和变量的符号值。首先,遍历

45、PAT树,初始化符号执行的变量列表,变量的符号值初始化为变量名;在符号计算过程中,每次计算到一个变量就在变量列表中查找相应的变量;每次符号计算完成后,查找需更新变量,更新相关变量。(3) 符号计算模块。符号计算模块是该原型系统的核心模块之一,该模块实现了中缀表达式中变量值的符号替换。当符号执行系统处理赋值语句的中缀表达时,系统根据PAT树遍历方法遍历中缀表达式,每次遍历到一个变量,查找变量列表,用变量的符号值替换变量,最后就得到了符号计算的结果。(4) 路径控制模块。路径控制模块也是该原型系统的核心模块之一,该模块实现了在符号执行系统模拟程序执行过程中选择执行路径的功能。Java程序中存在分支

46、结构和循环结构,因此程序执行路径不是简单的顺序结构。当符号执行分支结构时,使用PAT树的相应的遍历方法,符号执行系统提示用户输入执行分支选择,然后系统根据输入执行用户选择的路径。同样,当符号执行循环结构时,使用PAT树处理循环的遍历方法,符号执行系统提示输入执行次数,用户输入后系统根据输入次数循环执行相应的语句。3. 可视化模块可视化模块属于原型系统的应用层。可视化模块分为三个子模块:源程序文本显示模块、PAT树可视化模块和符号执行结果可视化模块。(1) 源程序文本可视化模块:使用已生成的文本对象和文本控件,可视化源程序,并实现代码高亮和代码定位等功能;(2) PAT树可视化模块:根据已生成的

47、PAT树和PAT树的遍历方法,使用树状控件,实现一个可视化的树型结构;(3) 符号执行结果可视化模块:符号执行结果包括变量的符号值和路径选择条件,可以使用文本控件,实现符号执行结果的可视化。2.3 小结本章主要介绍了JSE的体系结构和工作流程。为了使符号执行系统具有良好的健壮性和可维护性,JSE采用了分层的构架。系统的四个功能模块(文件管理模块、程序静态分析模块、可视化组件、符号执行组件)分布在三个逻辑层(基础层、中间层和应用层)中。在描述了符号执行系统基础构架之后,介绍了各模块的调用关系。最后,从用户的角度介绍了JSE中程序静态分析和符号执行的工作流程,以及如何完成各种不同的功能。通过此章的介绍可以看出,该系统在结构上遵循了符号执行系统可扩展性和健壮性的设计原则。不过要真正进行较好的符号执行,还需要各个模块的细节设计和实现。其中程序信息的有效组织和符号执行的机制是JSE的重点和难点。3 Java程序静态分析技术程序静态分析39是符号执行的基础,也是一个实现的难点。程序静态分析的主要功能包括构造程序静态分析树和实现程序静态分析树的遍历这两个部

展开阅读全文
相关资源
猜你喜欢
相关搜索
资源标签

当前位置:首页 > 生活休闲 > 在线阅读


备案号:宁ICP备20000045号-2

经营许可证:宁B2-20210002

宁公网安备 64010402000987号