（计算机应用技术专业论文）形式化技术在逆向工程中的应用研究.pdf

摘要 随着计算机技术的飞速发展，产生了越来越多的遗产系统，对这些系统进 行维护和升级是软件工程师们经常要面对的问题。要对遗产系统进行维护和再工 程，就需要用逆向工程技术对当前系统的结构和行为进行理解。作为软件工程中 的种新技术，逆向工程能够分析目标系统，确定系统的组件和它们之间的相互 关系，并以另一种形式或者在更高的抽象级别上建立对系统的表示，从而帮助 维护人员理解并重构软件系统。 形式化方法对于软件的发展，尤其是正向工程方面提供了许多好处。形式化 方法的一个优点是它的表示是精确的、可验证的，这样有助于使用自动化的处理。 一种利用形式化方法优点的方式就是通过对现有程序代码进行逆向工程来得到 形式化规约。 本文描述的逆向工程中的形式化方法采用最强后置条件谓词转换技术和 h o a r e 理论中有关程序语义的部分正确性模型，研究的重点是利用形式化技术和 非形式化技术对程序代码进行逆向工程，以支持软件理解和维护。针对c 程序的 基本语法结构定义了赋值语句规则、选择语句规则、循环语句规则、顺序语句规 则和函数调用规则，建立了一个最小的公理系统。介绍了以c m i n u s 语言( 自定义 的一种简化的c 语言子集) 为实例进行逆向工程的过程。在进行逆向分析的过程 中，首先对源程序进行词法语法分析生成语法树，从结构化源程序中提取源程序 的模板信息，并把模板信息用一个二叉树表示，之后按照设计的二叉树遍历算法， 把二叉树转化为pad ( p r o b l e ma n a l y s i sd i a g r a m ) 图，用以描述程序的结构， 并作为可视化的人工理解辅助工具，便于我们从中方便的选出源代码的关键部 分。在结构化分析的基础上，对关键性的源代码文件进行扫描，对每条语句进行 分析，根据c 程序语句中各种基本结构的最强后置条件形式化语义，对每条语句 按照相应的规则进行转换，得到程序的形式规约。 关键词：逆向工程；形式化方法；最强后置条件；p a d 图；形式规约 a b s t r a c t w i t ht h er a p i dd e v e l o p m e n to fc o m p u t e rt e c h n o l o g y ，m o r ea n dm o r el e g a c y s y s t e m sw e r ep r o d u c e d m a i n t a i n i n ga n du p g r a d i n gt h e s es y s t e m sh a v el o n gb e e na p r o b l e mf a c e db ys o f t w a r ee n g i n e e r s i ti sn e c e s s a r yt ou s et h et e c h n o l o g yo fr e v e r s e e n g i n e e r i n gt oa n a l y s i st h es t r u c t u r ea n db e h a v i o ro ft h ec u r r e n ts y s t e mi no r d e rt o m a i n t a i na n dr e e n g i n e e r i n gt h el e g a c ys y s t b m s r e v e r s ee n g i n e e r i n gi st h ep r o c e s s o fa n a l y z i n gas y s t e mt oi d e n t i f yt h ec o m p o n e n t sa n dt h e i rr e l a t i o n s h i p sa n dc r e a t e r e p r e s e n t a t i o n so ft h es y s t e mi na n o t h e rf o r mo r a tah i g h e rl e v e lo fa b s t r a c t i o n ， w h i c hc a nh e l pe n g i n e e r su n d e r s t a n da n dr e c o n s t r u c ts o f t w a r es y s t e m f o r m a lm e t h o d si ns o f t w a r ed e v e l o p m e n tp r o v i d em a n yb e n e f i t si nt h ef o r w a r d e n g i n e e r i n g ab e n e f i to ff o r m a lm e t h o d si st h a tt h e i rn o t a t i o n sa r ew e l l d e f i n e da n d t h u s ，a r ea m e n a b l et oa u t o m a t e dp r o c e s s i n g o n em e t h o df o ri n t r o d u c i n gf o r m a l m e t h o d s ，a n dt h e r e f o r et a k i n ga d v a n t a g eo ft h eb e n e f i t so ff o r m a lm e t h o d si s t h r o u g ht h er e v e r s ee n g i n e e r i n go fe x i s t i n gp r o g r a mc o d ei n t of o r m a ls p e c i f i c a t i o n s t h i sp a p e rd e s c r i b e sa na p p r o a c ht or e v e r s ee n g i n e e r i n gb a s e do nt h ef o r m a l s e m a n t i c so ft h e s t r o n g e s tp o s t c o n d i t i o np r e d i c a t et r a n s f o r m e r ，a n dt h ep a r t i a l c o r r e c t n e s sm o d e lo fp r o g r a ms e m a n t i c si n t r o d u c e db yh o a r e t h em a i np o i n to fo u r i n v e s t i g a t i o ni sh o wt ou s ei n f o r m a la n df o r m a lm e t h o d sf o rr e v e r s ee n g i n e e r i n g t h ea p p r o a c hp r o v i d e db yt h i st h e s i si sm a i n l yt op r o c e s st h ecp r o g r a ms y s t e mf o r r e v e r s ee n g i n e e r i n g i nt h et h e s i sw ed e f i n e dt h ea s s i g n m e n tr u l e ，a l t e r n a t i o nr u l e ， i t e r a t i o n r u l e ，s e q u e n c e r u l ea n df u n c t i o nr u l e a c c o r d i n gt o t h eb a s i cs y n t a x s t r u c t u r e so fc p r o g r a m sa n d s e tu pa na x i o ms y s t e mo fc p r o g r a m s t h ep r o c e s so f r e v e r s ee n g i n e e r i n gi si n t r o d u c e dt h r o u g ha ni n s t a n c e ，c m i n u s ( as i m p l i f i e dc l a n g u a g e ) i nr e v e r s ee n g i n e e r i n g ，t h ea b s t r a c ts y n t a xt r e ei sg e n e r a t e db yl e x i c a l a n a l y s i sa n ds y n t a xa n a l y s i sf r o ms o u r c ec o d e t h et e m p l a t ei n f o r m a t i o ni se x t r a c t e d f r o ms t r u c t u r e ds o u r c ec o d e ，w h i c hi sr e p r e s e n t e db yab i n a r yt r e e t h e nt h eb i n a r y t r e ei st r a n s l a t e di n t ot h epad ( p r o b l e ma n a l y s i sd i a g r a m ) a c c o r d i n gt ot h e d e s i g n e da l g o r i t h m a f t e rs t r u c t u r e da n a l y s i s ，t h es t a t e m e n t so fk e ys o u r c ec o d ew i l l b es c a n n e d ，a n de a c hs t a t e m e n tw i l lb et r a n s l a t e di n t of o r m a ls p e c i f i c a t i o na c c o r d i n g t ot h es t r o n g e s tp o s t e o n d i t i o ns e m a n t i c so ft h eb a s i cs t r u c t u r e k e yw o r d s ： r e v e r s ee n g i n e e r i n g ；f o r m a lm e t h o d ； s t r o n g e s tp o s t c o n d i t i o n ； p r o b l e ma n a l y s i sd i a g r a m ；f o r m a ls p e c i f i c a t i o n i i 长沙理工大学 学位论文原创性声明 本人郑重声明：所呈交的论文是本人在导师的指导下独立进行研究所 取得的研究成果。除了文中特别加以标注引用的内容外，本论文不包含任 何其他个人或集体己经发表或撰写的成果作品。对本文的研究做出重要贡 献的个人和集体，均己在文中以明确方式标明。本人完全意识到本声明的 法律后果由本人承担。 作者签名：马2 r j 珠艮 日期：2 嘧戽乒月17 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意 学校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文 被查阅和借阅。本人授权长沙理工大学可以将本学位论文的全部或部分内 容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存 和汇编本学位论文。 本学位论文属于 l 、保密口，在年解密后适用本授权书。 2 、不保密囹。 ( 请在以上相应方框内打“”) 作者签名：马l r 辛良 日期：加；年牛月，7 日 导师签名： 勿弘日期洲年争月7 日 1 1 研究背景 第一章绪论 随着计算机技术的飞速发展，计算机应用的领域不断扩大，人们希望计算机 能够解决各个领域更多、更复杂的问题，从而也对计算机软件产品的功能、质量、 开发成本和时间提出了越来越高的要求。计算机软件在各个领域经过了几十年应 用的积累，特别是自九十年代以来，应用软件系统的规模越来越大，功能越来越 复杂，使得更多的大型软件的开发必须考虑到原先已运行了多年的系统，包括系 统的需求、设计决策、业务逻辑、业务规则、历史数据等等，称之为遗产系统。 遗产系统是一种巨大的、长期的投资，许多用户还依靠这些系统进行运作，所以 不能简单的抛弃这些系统，而需要对它们进行维护和升级。而在很多情况下遗产 系统完整可靠的信息是其程序代码，其它很多信息必须由此导出，只有通过程序 理解获得足够的信息才能让系统按照期望的方式演化。为了充分有效地利用这些 有用的资产，软件逆向工程是有效的技术途径1 1 】。 软件维护、遗产系统的改造以及软件再工程等问题都是软件界普遍关注的话 题【2j 。近年来对现有软件系统进行维护、重构以及再工程的需求大量增加，例如 用户需求的改变或者进行软件移植都需要对现有的软件系统进行更新。据统计， 软件开发支出的5 0 n 7 5 用于软件的维护1 3 】。而重用和改造遗产系统的工作也是 非常复杂而且费用昂贵的，其中整个程序理解的过程就是一个非常耗时的过程。 据估计，5 0 9 0 的演化工作是花费在程序理解上的，而提高理解效率的最良好 和可行的方法是软件逆向工程。用来理解软件的费用，虽然很少被看成直接费 用，但却是实际需要花费的。理解软件所花费的时间也是很明显的，这其中还包 括对软件理解错误所浪费的时间。因此，研究促进程序理解的软件工程方法和工 具就显得非常必要。 逆向工程正是在这种需要下产生的软件工程方法。逆向工程着眼于分析软 件并用抽象形式将其表现出来，使其更易于理解。逆向工程可用于软件维护、软 件再工程、重用以及文档化等多种用途。软件逆向工程作为软件工程界新兴的研 究领域，其目标就是开发帮助人们理解己有软件系统的方法、工具，为软件系统 的维护和演化提供支持。逆向工程的基本原理是抽取软件系统的主要部分而隐藏 细节，然后使用抽取出的实体在高层上描述软件系统。逆向工程抽取的实体应比 源代码更容易推理和接近应用领域，同时在高层上对软件系统的抽象表示要简洁 和易于理解。 目前的逆向工程技术集中于从程序代码恢复高层设计的表示。其中一类方法 是构造软件的结构信息( 如图表) ，另一类方法用来恢复软件的功能信息。这些 方法大多数都是非形式化的，它们主要依赖于语法分析和模式匹配。然而这些技 术不能在一定程度上确认软件的可靠性，而这一点对于关键安全系统是非常重要 的。形式化方法是基于数学的用于描述系统性质的技术，它为系统的开发提供了 一个框架，并用严格的数学符号和计算规则对目标系统的结构和行为进行有效的 综合、分析和推理，以验证目标系统的正确性和一致性。形式化方法的个优点 是它的表示是明确的，这样有助于使用自动化的处理。因此本文针对结构化程序， 尝试应用非形式化方法和形式化方法结合对源程序进行逆向分析，从程序代码生 成程序规约，构造程序实现的高层抽象以支持软件理解和维护。 1 2 研究现状 无论是在国内还是国外，对逆向工程的研究都已经有相当长的时间了，虽然 己经形成了一定的研究规模，但是逆向工程仍然属于相当不成熟的领域，这主要 表现在对理论和实践的研究都还处于早期的探究阶段，并未形成统一的、系统化 的、科学化的逆向工程的理论和方法。逆向工程最早是在国外作为软件维护的一 部分出现的。c m us e i 成立了专门的再工程中心，致力于通过逆向工程进行程 序理解技术的标识、增强和实践推广。c h i k o f s k y 等人于t 9 9 3 年发起的逆向工程 会议每年举行一次，研究和讨论逆向工程的问题、技术及其支持工具f 5 】。 国外应用于逆向工程软件工具很多，它们主要提供三种类型的能力：一是常 规的静态模型逆向产生能力，从某种特定语言的源码或编译后的目标码转换出静 态模型( 如类图、活动图、控制流图等) ；二是动态模型逆向产生能力，将程序 运行过程中的标志性信息进行搜集、存储和整理，再转换成相应的动态模型( 如 序列图、状态图、协同图等) ；三是扩展的静态模型逆向产生能力，将常规的静 态模型逆向产生能力加以扩展，以体现静态模型的领域特征，提高静态模型的抽 象层次或者表现形式，以利于理解和使用。就目前许多典型的国内外逆向工程相 关工具而言，对常规静态模型逆向产生的支持已经十分广泛，但对于面向对象的 程序，必须进行动态模型的逆向产生，才能真正获得程序的行为特征。同时，各 种工具都有很强的前提条件，例如所支持的程序设计语言、操作系统和数据库平 台、调试工具和系统支撑工具、面向对象建模语言、人机交互语言和界面等，在 不同的前提条件下，工具的支持能力有很大的区别。 现在已有多种逆向工程工具在不同的领域被应用，下面是一些典型的工具。 ( 1 ) r i g i 逆向工程环境| 6 | 。用半自动的工具从软件表示中提取数据信息， 将信息存入低层库中，系统被抽象为子系统的分层结构。主要由3 部分构成：支 持c c + + 、c o b o l 等语言的程序静态信息解析器、用于存储从源代码提取的信 息的程序静态信息库以及展示和操纵程序静态信息的交互式窗口图形编辑器。 2 ( 2 ) i s v i s ( i n t e r a c t i o ns c e n a r i ov i s u a l i z e r ) 工具。这种工具的功能包括：读 入源程序文件，解析后产生静态信息文件；利用源代码、静态信息文件以及用户 提供的相关的信息，产生获取动态信息所需的代码。执行插入上述代码后的目标 系统，产生动态事件跟踪信息，并自动转变成剧情，用户通过所产生的剧情视图 进行交互式分析i7 1 。 ( 3 )s n i f 升+ 。s n i f f + + 是一个开放的、可扩展的、可伸缩的c c + + 程序设 计环境，它具有逆向工程的能力，提供了一个有效而轻便的环境，适用于不能完 全解析的半成品软件系统，在产生可打印的视图和浏览半成品系统等方面也具有 特色隋1 。 ( 4 ) r a t i o n a lr o s e 工具1 9 。r a t i o n a lr o s e r o s er e a l t i m e 的逆向工程工具可 以从多种程序设计语言源程序中自动产生静态设计模型，当前只能产生类图。 r o s e a r c h i t e c t 是u s c 与r a t i o n a l 合作开发的一种可视化工具，用于对u m l 类 图中的实体进行基于规则的等价合并，以突出地呈现系统的软件体系结构成份。 ( 5 ) i m a g i x 4 d f ”】。i m a g i x 4 d 是一个c c + + 程序的静态理解工具。i m a g i x 4 d 以三维图形的形式展示关键信息，还提供产生大量视图、从源代码生成文档和有 助于迅速理解程序的交互式询问功能。 ( 6 ) d e s i r e 是基于模型的软件设计恢复工具。它使用概念识别和程序理 解，提供智能式查找用户定义的概念实例，识别与领域模型相符合的概念，为某 一给定的集合进行概念赋值。该工具可产生调用图，全局变量引用点，给定范围 的符号定义及构件等】。 ( 7 ) 国内的工具主要有青乌程序分析系统( j b p a s ) 。j b p a s ( j a d eb i r d p r o g r a ma n a l y s i ss y s t e m ) 是一个针对c + + 语言的程序理解系统，由一个c 十+ 分 析器前端和一组分析工具组成。该系统是北大青鸟基于异构平台、具有多信息源 接口的应用系统集成环境青鸟i i i 型( j b 31 系统的组成部分【1 ”。青鸟程序分 析系统( j b p a s ) 是一组基于程序分析的工具。首先通过概念建模建立面向对象程 序的概念模型，然后用编译器前端分析源代码，按照概念模型抽取信息并存入程 序信息库中。在信息浏览和使用上，建立一组基于程序信息库的工具，包括设计 文档逆向生成工具、测试支持工具、构件提取工具以及度量工具等。j b p a s 的前 端分析器充分处理了语言的预编译功能，从而准确定位了程序实体与源代码之间 的位置关系，并有效地抽取代码注释信息。 1 3 本文的主要工作 本文研究的重点是利用非形式化技术和形式化技术对c 程序代码进行逆向 工程，以支持软件理解和维护。针对c 程序的语法结构应用最强后置条件谓词 转换定义了赋值语句规则、选择语句规则、循环语句规则、顺序语句规则和函数 3 调用规则，建立了一个最小的公理系统，对c 程序的逆向工程就是基于这个公 理系统进行的。 介绍了以c m if i l l s 语言( 自定义的一种简化的c 语言子集) 为实例进行逆向工 程的过程。在进行逆向分析的过程中，首先利用词法和语法分析自动生成工具生 成词法语法分析程序，对源程序进行词法语法分析后生成抽象语法树，从结构化 源程序中提取源程序的模板信息，并把模板信息用一个二叉树表示，之后按照设 计的二叉树遍历算法，把二叉树转化为p a d ( p r o b l e m a n a l y s i s d i a g r a m ) 图以 帮助理解程序。在结构化分析的基础上，对关键性的源代码文件进行扫描，对每 条语句进行分析，根据c 程序语句中各种基本结构的最强后置条件形式化语义， 对每条语句进行相应的转换，得到程序的形式规约。 1 4 论文的组织 全文共分六章，各章主要内容如下： 第一章：介绍了本文研究的背景和国内外研究现状，给出了本文研究内容 和论文的组织方式。 第二章：介绍了软件逆向工程的基本概念、研究目标和基本过程，阐明了 逆向工程技术的研究方法和实现途径。 第三章：介绍了形式化方法的分类和特点，重点讨论了程序语义的形式化 描述，详细讨论了最弱前置条件和最强后置条件的形式语义。 第四章：对命令式程序设计语言中几种基本结构的最强后置条件进行了描 述，包括赋值语句、选择语句、顺序语句、循环语句和函数调用的最强后置条件。 第五章：对c 程序设计语言中的赋值语句、选择语句、顺序语句、循环语 句和函数调用的最强后置条件谓词转换进行了定义，用一种三阶段法对c 程序 进行形式化的逆向工程。 第六章：针对c 语言的一个子集，介绍了词法语法分析程序的实现，通过 对源程序进行词法语法分析生成抽象语法树，将源程序抽象成p a d 图以帮助理 解程序。用形式化方法对关键部分的语义进行说明，采用基于h o a r e 逻辑的最强 后置条件谓词转换，生成程序代码的形式规约，并用实例说明了这种方法的应用。 结束语：对全文进行了总结，对本文的主要工作给予了评价，并给出了进 一步研究的内容。 4 第二章逆向工程技术 “逆向工程”一词来自硬件领域，是通过检查样品来开发复杂硬件系统规 约的过程j ，主要指研究他人的系统，发现其工作原理，以达到复制硬件系统 的目的1 1 4 。但是，逆向工程也同样适用于其他领域，逆向工程在软件工程领域 中是一个较新的令人感兴趣的领域m 】。 在软件工程中，正向工程指高层设计到低层的实现，逆向工程可看作它的反 过程。软件的逆向工程是分析程序，力图在比源代码更高抽象层次上建立程序表 示的过程，逆向工程是一个设计恢复过程，从现存的程序中抽取数据、体系结构 和过程的设计信息【1 6 】。 。 2 1 逆向工程的概念 在软件领域中，迄今为止还没有逆向工程的标准定义。一般将逆向工程定义 为包含两个步骤的过程1 1 7 】：第一步分析目标系统，标识系统对象及其关系；第 二步创建不同形式或更高抽象层次的系统表示。s c o t tr t i l l e y 将抽取和抽象进 一步精化为建模、抽取和抽象三个步骤： ( 1 ) 建模，采用建模技术构造应用程序的领域模型； ( 2 ) 抽取，利用适当的抽取机制从目标系统中收集原始数据； ( 3 ) 抽象，对目标系统进行抽象，以辅助系统理解并允许浏览、分析和表示抽 象结果。 国家自然科学学科发展战略报告计算机科学技术部分中是这样定义软件逆 向工程的ds ：从可运行的程序系统出发，生成对应的源程序、系统结构以及相 关设计原理和算法思想的文档等。从这个定义可以看出，软件逆向工程可以用于 较低级的抽象层次，例如把可执行程序转换为源代码，但主要是用于将源代码转 换为更高抽象层次上的表示，如控制图、数据流图和类关系图等【”】。 下面是与逆向工程相关的几个术语： 再文档( r e d o c u m e n t a t i o n ) ：根据源代码，在同一层次上创建或修改系统文档。 设计恢复( d e s i g nr e c o v e r y ) ：结合目标系统、领域知识和外部信息认定更高 层次的抽象。 重构( r e s t r u c t u r i n g ) ：保持系统外部行为( 功能和语义) ，在同一抽象层次上 改变表示形式。 再工程( r e e n g i n e e r i n g ) ：结合逆向工程、重构和正向工程对现有系统进行审 查和改造，将其重组为一种新形式。 5 2 2 逆向工程的目标 软件系统逆向工程的首要目的是增加系统在维护和新开发时的可理解性，总结 起来具体要完成下列任务： a ) 处理复杂性：软件系统越来越复杂，人工方法已经很难有效维护、理解， 研究逆向工程技术和c a s e 工具辅助控制软件系统的复杂性是软件成功的关键。 b 1 自动生成系统的其它视图：代码的图形表示可以大大促进理解，自动由代 码生成数据流图、控制流图、类图、实体关系图等是软件逆向工程的基础部分。 c ) 映射应用程序领域和问题域：计算机程序表示了应用领域中的问题，但是 程序通常不包含问题的提示，逆向工程的任务之一是重构应用程序领域到问题域 的映射。 d ) 映射具体和抽象级别：软件开发过程从高层抽象到详细设计再到具体实 现；逆向工程则反向运作，从具体细节创建抽象表示。 e ) 重新发现高层结构：程序是具有良好定义的高层结构的载体。但是因为时 间的推移和不断维护等一些问题的存在，这些高层结构可能己经丢失。 n 帮助重用：逆向工程可以帮助或自动检测、筛选在遗产软件系统中的候选 重用组件。 g ) 恢复丢失的设计知识：在软件代码的不断修改中，有许多业务规则被加入 而没有反映在文档中，这部分知识可以通过逆向工程来恢复。此外还有一些知识， 如反映代码质量的一些度量数据只有通过逆向工程才可以发现。 h ) 检测边缘效应：软件修改或加入的部分可能会带入新的问题，而对原来的 代码运行有一定的影响。这种影响无法在正向工程中反映出来。 2 3 逆向工程的基本过程 软件逆向工程并不改变目标系统，它只是一个分析检查的过程，而不是一个 修改的过程。软件逆向工程通过标识系统组件及发现这些组件之间的关系，对系 统做出抽象的表示，从而辅助对系统的理解。它涉及的对象可分为三类f 2 0 】： ( 1 ) 数据( d a t a ) ：作为学习、推理和讨论基础的实际信息，这些数据包括系 统源程序、源代码注释、需求分析、分析文档、设计文档、用户手册以及观测到 的系统的外部行为等。 ( 2 ) 知识( k n o w l e d g e ) ：所有内容的总和，包括数据和从数据中推导出的关 系与规则，例如在程序理解过程中得到的各种中间结果和对系统各子模块产生的 层次结构图等。 ( 3 ) 信息( i n f o r m a t i o n ) ：相互交织的交流知识，这些信息包括所有的数据和 知识，以及软件工程人员的各种非正式的思路和建议。 基于这三类对象，s c o t tr t i l l e y 等人给出了软件逆向工程的三个规范活动： 6 数据收集、知识组织和信息浏览。 2 3 1 数据收集 原始数据是构造和浏览高层抽象的基础，因而数据收集是软件逆向工程的一 项基本活动。而作为构造抽象表示的基础，数据收集不能误导或误解，必须客观 实际。因此，数据收集时，应尽量遵循下列原则1 21 】： ( 1 ) 采用成熟的技术：数据收集所采用的技术包括静态分析、动态分析和 获取非正式数据( 如调查) 等，其中最流行的是分析程序源代码，构造带有语法单 位及其依赖关系的抽象语法树。在编译领域中，语法分析和交叉索引等技术已经 很成熟，采用基于编译的成熟技术，可以得到预期的结果，使收集的数据更加准 确和可靠。 ( 2 ) 利用多种数据：遗产系统有四种数据来源m 】：( a ) 系统源代码，包括数 据结构、规则控制进程、报表格式以及计算机的编码指令；( b ) 系统行为，即系 统用户所看到的系统功能和性能；( c ) 系统文档，包括需求分析文档、设计文档、 用户手册和源代码注释；( d ) 系统的设计者和维护者。系统的多种数据从不同的 方面刻画了系统对象及其关系，从而为更深入详细地理解系统提供了基础。利用 系统源代码以外的其它数据，能够更好地辅助软件工程人员理解那些难以理解的 系统。例如，软件工程专家常常利用源代码注释理解系统；调查系统设计者和维 护者可以获得他们的经验，从而使数据更准确、更可靠。 ( 3 ) 过滤数据：为理解大型系统所收集的数据量可能是巨大的，以至于超 出了人们理解的能力。人们要理解系统，首先必须吸收其中的数据，而系统理解 的关键之一在于清楚了解什么和忽略什么1 2 3 。数据过滤是从丰富的数据源中抽 取所选择的对象及其关系，因而，在辅助系统理解中起着重要作用。 2 3 2 知识组织 知识组织涵盖了创建、表示和推理数据模型的技术，包括概念建模、领域 建模和可扩展知识库。数据模型体现了系统的本质属性及其关系，利用数据模型 保存数据可以对所采集的数据实现高效的存储和检索，便于数据的保存和使用。 逆向工程的建模必须满足人们理解系统的要求。和传统的数据模型如层次模型、 网络模型和关系模型不同，概念建模所建模的对象及其关系是面向人的，其建模 机制适用于逆向工程领域。程序结构本身不足以反映程序所应用的问题域，通过 领域建模可以标识、组织和表示领域元素及其组成结构，辅助人们按领域组织目 标系统的知识，识别系统的标准构件。 2 3 3 信息浏览 逆向工程从数据采集开始，依赖于知识组织，将数据组织成应用程序领域的 7 概念模型，其中信息浏览是整个过程的关键行为，多数程序理解都是在该过程中 进行的。信息浏览通过遍历浏览代表目标系统的信息的多维结构，按领域相关的 标准分析和过滤信息，利用多种机制表示所得到的信息。 遍历：遍历采用定向和高级模式匹配等机制，辅助人们浏览逆向工程知识组 织阶段所产生的多维信息结构。 分析：分析多维信息结构是程序理解的关键。分析从原始数据中导出并抽取 那些并不显式存在的信息，并产生关于系统的深层视图。 表达：表达是在研究人们程序理解时所采用的认知策略基础上，创建多方位、 正交、结构化视图表现分析结果。 2 4 逆向工程技术分类 对于软件逆向工程技术，可以分为形式化技术和非形式化技术【2 4 】。非形式 化方法是基于代码的词法结构，并依赖于模式匹配及用户驱动的聚集技术的方 法。非形式化技术易于产生结构和功能抽象，模式匹配和聚集技术是非形式的， 因为被构造的设计陈述是非形式化的，并且这些技术缺乏严格方法来验证在源和 设计之间的一致性。形式化技术是基于一些形式化的方法从源代码来导出其规 格，形式化的基础可以归结为数学逻辑，所以每一步都可以形式化的验证。两者 主要的不同是对于形式化规格语言的应用。形式化规格语言有良好定义的句法和 语义，因此形式化技术又可以用来构造证明的关联引用规则，用来严格验证逆向 工程过程的每一步的正确性。 非形式化技术又可以分为基于计划的和基于解析的两种子类型，基于计划的 技术主要依赖用模式匹配来分辨代码中的计划，这是学术界和商业组织的主流。 一个程序计划是程序中承担些抽象功能的一个计算单元所包含的描述，它可以 是连续的或分散的代码段。基于解析的技术是用编程语言的句法结构特点分析一 个程序，用来构造源代码的高层结构抽象。 如果一个逆向工程技术的步骤有一个形式化的数学基础，那么它是形式化 的。它把源程序作为输入，生成一个形式化的规格。形式化的逆向工程技术可以 分为两类：基于知识或转换规则的转换技术和应用推导或翻译规则的翻译技术。 软件转换和软件翻译都是把一个规格从一种形式变换到另一种形式而保持软件 的语义不变，但是它们的自动化程度不同。它们主要的不同是应用域和编程语言 的高层知识结合到转换和翻译规则中的程度不同。对于转换，规则一般涉及转换 编程语句聚集为简单的、等价的语句，或简洁的形式化规格。为处理不同的聚集 组合，需要很多的规则。而翻译涉及许多基于单个原子语句的规则，如赋值、条 件和循环语句。 2 5 逆向工程研究方法 现有的逆向工程分析方法主要有以下几种： ( 1 ) 词法分析和语法分析 该方法直接对程序源码进行分析，已经发展得比较成熟。通过词法分析可以 得到程序信息的多种有用表示，其中最常用的是交叉引用列表。通过语法分析可 以得到两类表示：分析树( p a r s et r e e ) 、抽象语法树a s t ( a b s t r a c ts y n t a xt r e e ) 。其 中，分析树只是指导分析过程，是比较原始的结果。分析树显示了程序语句的分 解过程，包含和程序的实际含义无关的信息。去除分析树的无关信息后得到a s t ， a s t 只包含和程序实际内容相关的细节，是更复杂的程序分析工具的基础。 ( 2 ) 图形化方法 图形化方法包括控制流分析、数据流分析以及程序依赖图。 控制流分析对执行语句的若干可执行路径进行分析，确定程序的控制结构， 建立控制流图。控制流分析有两种形式：过程内分析和过程间分析。过程内分析 通过构建控制流图c f g ( c o n t r o lf l o wg r a p h ) 进行，可确定子程序内语句的执行顺 序。构建c f g 必须先确定子程序的基本块。一个基本块对应c f g 中一个节点， 是一些连续语句的最大集合。在该语句集合中，控制只能从第一条语句开始，也 只能从最后一条语句经条件分支或非条件分支转出。就是说基本块的第一句执 行，基本块中所有语句都会执行。基本块可以直接通过遍历a s t 确定，再用控 制流弧线连接基本块来创建c f g 。过程间控制流分析是确定系统子程序之间可 能的控制流路径的过程，用调用图( c a l lg r a p h ) 表示。调用图给出了一个系统中对 子程序的可能调用。调用图是树、有向无环图还是一般的图由系统结构决定。调 用图中的结点和子程序对应，节点之间的有向弧标识出调用关系。控制流分析对 执行语句的若干可执行路径进行分析，确定程序的控制结构，建立控制流图。 数据流分析是在不执行程序的情况下，收集程序数据的运行时信息，分析程 序中数据对象之间的关系，数据流分析关注于解决程序中从定义到使用的过程的 相关问题，比控制流分析要复杂得多。 程序依赖图是数据流分析的进一步改进，比数据流分析更复杂。在程序依赖 图中，节点表示语句和谓词表达式( 或运算符和操作数) ，边表示该节点的操作所 依赖的数据值和控制条件。程序依赖图将控制流和数据流放在一起处理，清楚地 描述了程序中每个操作的数据依赖和控制依赖。如果同时需要控制流图和数据流 图的相关信息，使用程序依赖图就很方便。 ( 3 ) 程序切片 切片技术是将程序简化为和某个特殊计算相关的语句的技术，来源于数据流 分析方法。切片技术自动将程序分解为较小的称为切片的代码段，使关注点确定 在一个较小范围而不必关注整个程序。一个程序切片是由程序中的一些语句和判 9 定表达式组成的集合。这些语句和判定表达式可能会影响在程序的某个位置( 常 用行号标识) 上所定义或使用的变量的值。切片技术己经成为很多程序理解工具 的基础。 ( 4 ) 抽象解释 抽象解释是对程序语言的语义形式上构建一个保守的近似，用基于语义的分 析来确定程序的动态属性。和程序的语法属性可以用b n f 范式表达类似，程序 的语义属性可由一种数学方法一一指称语义( d e n o t a t i o n a ls e m a n t i c s ) 来描述。在指 称语义中，程序的含义用多种称为语义域的数据类型来表示。基于原始的语义域 来定义替换函数，借助这种方法可以进行静态分析。例如，如果要确定指定变量 的值是否被子程序改变，不必去关心变量可能取的值，可以为变量的赋值语句解 释语义函数，只用一个简单的布尔变量就可以标识变量是否改变，这种再解释的 过程就是抽象解释。 ( 5 ) 动态分析 静态分析是对程序源码进行分析。动态分析则是在程序运行时进行分析，基 本方法是对程序进行植入。程序植入是一种在全局范围内更改源代码以添加额外 操作的过程。这种方法的主要原理是：利用代码的结构信息，依据固定的规则， 将软件触发器添加到代码中。所谓软件触发器，是指在源程序的相应位置添加的 一些代码，运行时由这些代码按特定协议将指定的动态信息传递到指定位置或传 递给动态信息收集机制。对于使用动态绑定和多态的面向对象系统，动态分析是 必需的。 2 6 逆向工程的应用 就逆向工程的现状而言，逆向工程一般是对已有软件系统的源代码进行分 析，以获得系统设计层次上的理解。逆向工程适用于软件生命周期的各个阶段和 各种抽象层次，包括概念、需求、设计和实现。通常系统维护人员并不是系统的 开发人员，所以他们必须对许多源代码进行扩展来检查和学习所维护的系统。逆 向工程工具有助于这些维护活动。在这个背景下，逆向工程是系统维护过程的一 部分，它能帮助维护人员理解系统，使维护人员能对系统做适当的修改。重构和 逆向工程都可以算在软件维护的广泛定义中，但这三个过程在构建新系统和软件 演化开发的背景下又都有自己独立的位置。 图2 1 是一个对逆向工程过程模型的图形描述。这个过程模型由两组三角形 组成，其中三角形的每个部分表示了抽象的不同级别。模型中的高层是概念和需 求，低层包括设计和实现。这个逆向工程处理模型的入口是在系统a 上，其中抽 象( 或逆向工程) 是从适当级别的细节开始进行的。下一步是改造，在不同的抽象 级别上把系统改造成一个新的形式。最后，对新形式进行提取进而完成对新系统 b 的实现。 1 0 改造 - - - - - - - - + a 系统b 系统 图2 1 逆向工程处理模型 逆向工程可以跨越生命周期的各个阶段，涉及广阔的范围，包括从现存的系 统实现重新获得或者建立系统的设计信息，以及解密目标系统实际实现的系统需 求。本文描述的逆向工程方法是适用于实现和设计级别的。在图2 1 中，本文的 研究内容是用虚线的箭头表示的。也就是说，我们主要是说明如何建立低级的设 计规约。在这种实现级别上操作的目的是提供一种在程序源代码和用我们的技术 建立的规约之间的可跟踪性。为了能够有助于形式化方法的技术转换，在充分利 用形式化方法的长处之前，开发人员必须能理解源代码与利用形式化方法建立的 规约之间的关系，因此这种可跟踪性是必须的。 3 1 概述 第三章形式化方法 形式化方法通过严格的、规范化的数学理论来描述软件系统是做什么事情 的，这也称为形式化分析的方法和规格说明的方法。形式化方法所用的语言是严 格的数学语言，其语法和语义都是无二义性的、精确的数学语言。形式化方法用 数学符号的一种精确的、一致性的和完整性的方式来描述软件系统的性质。在形 式化方法中，重要的一点是形式化的说明语言，这种语言主要用来说明和描述系 统的规格。使用形式化方法可以帮助开发者获得对其所描述的系统的深刻而正确 的理解，并通过揭示隐含的不一致性、二义性、不完整性而发现设计中的错误和 缺陷，从而可以及时地更正这些错误和缺陷。而一些非形式化的方法是很难发现 这些错误和缺陷的。形式化方法通过形式规约的语言来对软件系统的各个方面的 性能进行描述，产生系统的形式规约。形式规约为系统设计、实现和验证提供了 准确一致的文档依据，成为用户和设计者之间、设计者和实现者之间进行充分沟 通的可靠桥梁，实现互相理解上的一致性。 形式化方法的形式规格说明是用具有精确语义的形式化语言书写的程序功 能描述，它是论证程序是否正确的依据。程序正确性就是讨论程序的语义和预期 目标的一致性。在逻辑理论中，一阶谓词演算是一个形式逻辑系统，具有一整套 证明技术，采用一阶谓词演算方法进行规范说明是非常合适的。将一阶谓词演算 和程序联系起来，主要需要解决两方面互相转换的问题，即谓词演算转换成程序 和程序转换成谓词的问题。将谓词演算转换成程序的问题也就是程序的自动生成 问题，也称为软件的自动生成问题，而将程序转换成谓词的问题属于程序验证的 问题。 3 2 形式化方法分类和特点 根据说明目标软件系统的方式，形式化方法可以分为两类f 2 5 】：面向模型的 形式化方法和面向属性的形式化方法。面向模型的方法通过构造一个数学模型来 说明系统的行为。面向属性的方法通过描述目标软件系统的各种属性来间接地定 义系统行为。 根据表达能力，形式化方法可以分为以下五类： ( 1 ) 基于模型的方法：通过明确定义状态和操作来建立一个系统模型( 使 系统从一个状态转换到另一个状态) 。用这种方法虽可以表示非功能性需求( 如 时间需求) ，但不能很好地表示并发性。如：z 语言，v d m ，b 方法等。 1 2 ( 2 ) 基于逻辑的方法：用逻辑描述系统预期的性能，包括底层规约、时序 和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具 体的编程构造扩充逻辑从而得到一种广谱形式化方法，通过保持正确性的细化步 骤集来开发系统。如h o a r e 逻辑，模态逻辑，时序逻辑等。本文使用的形式化 方法就是基于h o a r e 逻辑的最强后置条件谓词转换的方法。 ( 3 ) 代数方法：通过将未定义状态下不同的操作行为相联系，给出操作的 显式定义。与基于模型的方法相同的是，没有给出并发的显式表示。如：l a r c h 族 代数规约语言等。 ( 4 ) 过程代数方法：通过限制所有容许的可观察的过程间通信来表示系统 行为。此类方法允许并发过程的显式表示。如通信顺序过程( c s p ) ，通信系统 演算( c c s ) 等。 ( 5 ) 基于网络的方法：由于图形化的表示法易于理解，而且非专业