（计算机软件与理论专业论文）基于jpf的软件模型检测分析与应用.pdf

摘要 摘要 形式化方法是提高并发系统的安全性与可靠性的重要手段。模型检测是一 种对有限状态并行系统进行形式化验证的方法，并已初步应用于各种软件的安 全性和可靠性验证中。软件模型检测过程中最大的问题，是如何缓解状态空间 爆炸问题。 j p f ( j a v ap a t h f i n d e r ) 是一种精确的j a v a 字节码状态模型检测工具。j p f 为j a v a 程序的模型检测提供了很好的实现方法，对并行程序中存在的死锁和数 据竞争等问题，以及未处理异常等与j a v a 运行时相关的程序漏洞，j p f 都可以 有效地进行模型检测。j p f 工作在j a v a 虚拟机之上，通过v m 来对系统状态进行 搜索和管理，使用启发式选择生成器来构建系统的状态转移。j p f 提供了 s e a r c h l i s t e n e r 和v m l i s t e n e r 、m j i 、字节码工厂及报告系统等丰富的扩展方 式。针对j a v a 程序本身的特点，j p f 提供了一系列限制状态空间爆炸的可行性 方案，包括偏序规约、对称规约、谓词抽象等。 本文基于j p f 提出了一种软件模型检测工具的通用设计策略，包括状态管 理、搜索策略和环境模拟等；实现了基于e c li p s e 的j a v a 模型检测平台，使得 程序员可以在编写代码的同时实时检测自己的代码；扩展了j p f 的错误轨迹输 出方式，在只关注系统漏洞位置的情况下，可以通过忽略系统反例细节的方式 来加速程序的模型检测过程。通过多个实例验证，表明了本文提出的软件模型 检测工具设计策略的有效性和基于e c li p s e 的j a v a 模型检测平台的可靠性。 j p f 对提高j a v a 程序软件的安全性、保证软件质量和发掘软件中的漏洞发 挥着重大作用，有着广阔的发展前景，需要进一步的深入研究。 关键词：软件模型检测；j p f ；状态空间爆炸；谓词抽象；字节码工厂 本课题得到江西省自然科学基金项目( 0 6 1 1 0 5 7 、2 0 0 7 g z s l 8 8 4 ) 和江西省研究生创新 专项资金项目( y c 0 8 a 0 3 2 ) 共同资助。 a b s t r a c t a b s t r a c t f o r m a lm e t h o di so n eo ft h em o s ti m p o r t a n tw a y st op r o m o t et h es a f e t ya n d r e l i a b i l i t yo fc o n c u r r e n ts y s t e m m o d e lc h e c k i n gi sam e t h o df o rf o r m a l l yv e r i f y i n g f i n i t e s t a t ec o n c u r r e n ts y s t e m s ，a n dh a sb e e n u s e dt ov e r i f yt h e s a f e t ya n d r e l i a b i l i t yo fv a r i o u ss o f t w a r e t h eb i g g e s tp r o b l e mi ns o f t w a r em o d e lc h e c k i n gi s h o wt oc o n s t r a i nt h es t a t es p a c ee x p l o s i o n j p f ( j a v ap a t h l q n d e oi sak i l l do fe x p l i c i ts t a t em o d e lc h e c k e rf o rj a v ab y t e c o d e i t sag o o dm e t h o du s i n g 伊ft oi m p l e m e n tas o f t w a r em o d e lc h e c k e r , e s p e c i a l l yf o r t h ec o n c u r r e n tp r o g r a m s ，w h e r et h e r ea r es o m ep o t e n t i a ld e f e c t sl i k ed e a d l o c ka n d d a t a - r a c e ，j p fc a nf i n dt h o s ed e f e c t se f f i c i e n t l y m o r e o v e r , t h eu n h a n d l e de x c e p t i o n c a na l s ob ec h e c k e ds u c c e s s f u l l y , w h i c hi sj a v ar u n t i m er e l a t e d a sw ek n o w , j p f w o r k e so nt h ej v mw h i c hc a ns e a r c ha n dm a n a g et h es y s t e ms t a t e s ，a n dp r o d u c e s t r a n s i t o n sb yt h eh e u r i t i cc h o i c eg e n e r a t o r j p f sf l e x i b i l i t yi sa c h i e v e db ya l l a r c h i t e c t u r et h a tp r o v i d e sal a r g en u m b e ro fe x t e n s i o np o i n t s ，o fw h i c ht h em o s t i m p o r t a n to n e s a r es e a r c h l i s t e n e r , v m l i s t e n e r , m j i ，b y t e c o d ef a c t o r i e sa n d p u b l i s h e r s a c c o r d i n gt ot h ef e a t u r e so fj a v ac o d e s ，j p fp r o v i d e sas e r i e so f a v a i l a b l ea p p r o a c h e s ，s u c ha sp a r t i a lo r d e rr e d u c t i o n , s y m m e t r yr e d u c t i o n , p r e d i c a t ea b s t r a c t i o na n ds oo n b a s e do nt h ei n t r o d u c t i o no ft h et h e o r ya n di m p l e m e n to fj p f ，t h i sp a p e r p r o p o s e dag e n e r a lk i n do fs t r a t e g yf o rd e s i g n i n gas o f t w a r em o d e lc h e c k e r , i n c l u d e s t a t em a n a g e m e n t ，s e a r c h i n gs t r a t e g y , e n v i r o n m e n ts i m u l a t i o ne c t a n di td e v e l o p e d av e r i f y i n gp l a t f o r mo ne c l i p s ea saj a v am o d e lc h e c k e r ，w i t hw h i c hp r o g r a m m e r s c a nv e r i f yt h e i rc o d e sw h e nt h e yh a v ef i n i s h e dd e s i g n i n gaj a v a - c l a s s f u t h e rm o r e ， i nt h ec a s eo ff o c o u s i n go n l yo nt h el o c a t i o nw h e r ee r r o r sh a p p e n , h e r ea d da n e x t e n d e df u n c t i o nt ot h ep l a t f o r mb yi g n o r i n gt h ed e t a i l so fac o u n t e r e x a m p l e ，i n o r d e rt os p e e dt h ep r o g r e s so fj a v am o d e lc h e c k i n g t h o u g hv e r i f y i n gas e r i e so f i n s t a n c e so fj a v ap r o g r a m ，t h er e s u l t ss h o w e dt h a tt h eg e n e r a ls t r a t e g yw es u g g e s t e d f o rd e s i g n i n gas o f t w a r em o d e lc h e c k e ri se f f e c t i v e ，a n dt h ej a v am o d e lc h e c k i n g p l a t f o r mm e n t i o n e da b o v ei sq u i tr e l i a b l e j p fh a sp l a y e dav e r yi m p o r tr o l e i ni m p r o v et h e s a f e t y , q u a n l i t ya n d i i a b s t r a c t b u g s f i n d i n go f s o f t w a r ei nj a v a , w h i c hw i l lb ev e r yp o p u l a ri nf u t u r e i t sw o r t h yf o r u st od om o r er e s e a r c ho ni t k e yw o r d s ：s o f t w a r em o d e lc h e c k i n g ；j p f ；s t a t es p a c ee x p l o s i o n ；p r e d i c a t e a b s t r a c t i o n ；b y t e c o d ef a c t o r y ； i i i 学位论文独创性声明 学位论文独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作及取得的 研究成果。据我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表或撰写过的研究成果，也不包含为获得直昌太堂或其他教育 机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何 贡献均已在论文中作了明确的说明并表示谢意。 学位做作者签名c 手写) ：尹谬支签字日期c 2 。乃年刀月细 学位论文版权使用授权书 本学位论文作者完全了解直昌太堂有关保留、使用学位论文的规定，有权 保留并向国家有关部门或机构送交论文的复印件和磁盘，允许论文被查阅和借 阅。本人授权直昌太堂可以将学位论文的全部或部分内容编入有关数据库进行 检索，可以采用影印、缩印或扫描等复制手段保存、汇编本学位论文。同时授 权中国科学技术信息研究所将本学位论文收录到中国学位论文全文数据库， 并通过网络向社会公众提供信息服务。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名c 掏：尹p 乏 签字日期：0 1 口，。年p 月易日 瑁 备，卜 夏k r k夕 年 九 纱 写 听 挈 如 q 0 名 期 签 日 师 字 导 签 第1 章引言 1 1 课题背景 第1 章引言 形式化方法是目前兴起的一种软件验证方法，它能够实现在软件复杂性增 加的情况下仍能构造出正确的系统。使用形式化规范说明语言的推演规则可以 严格分析程序定义以保持其正确性和一致性。传统的软件开发方法由于大量的 使用自然语言和多种图形符号，结果是尽管经历了仔细地复审，最后的系统规约 说明中仍然包含歧义的、含糊的、矛盾的、不完整的需求描述及混乱的抽象层 次。使用形式化方法可以克服这些缺点。形式化方法在软件验证的应用大致从 串行程序验证开始，随后运用于反应式系统( f i n i t e s t a t er e a c t i v es y s t e m ) 、并发系 统、实时系统中。形式化方法以其严密性越来越受到众多领域的重视，在很多 大型软件项目中获得成功应用。 模型检钡q ( m o d e lc h e c k i n g ) 1 1 】是形式化验证方法中的一种，此概念源于上个 世纪8 0 年代，是用于验证有限状态反应系统的一种自动化技术。模型检测中用 来描述系统性质的常见时态逻辑有l t l 、c t l 、c t l * 等。该技术已被广泛应用 于时序电路设计和通信协议设计，并取得了很大的成绩。真正将模型检测技术 引入到软件的验证只有短短的几年历史，该技术目前正处于研究阶段。 随着模型检测技术的发展，陆续出现了一些优秀的模型检测工具，如s m v 、 s p i n 、v e r i s o f t 、s l a m 、b l a s t 、m a g i c 等。j p f 是美国n a s a 军事研究中 心的r o b u s t 软件工程小组开发的，它是一种用来验证j a v a 字节码程序的系统， 可以检测出死锁、未处理异常等性质冲突。早期版本的j p f 的内核是基于s p i n l 2 j 的，相当于个翻译器，将j a v a 翻译成p r o m e l a 引，然后使用s p i n 来进行 验证。现在，j p f 基于s p i n 做了许多改进( 如处理无界数据) ，它可以直接运行 字节码，拥有自己的垃圾回收机制，可以存储访问过的状态和当前路径，给用 户提供了一些方法来优化验证。j p f 与其他调试工具最大的区别在于，它可以 报告产生漏洞整个的执行路径，适用于多线程程序当中难以检测到的并行漏洞。 研究j p f 的内核实现及其功能扩展方法，对软件模型检测技术的实现具有很大 的推动作用。 第1 章引言 1 2 相关技术简介 1 2 1 形式化验证方法 验证一个系统的正确性，传统的方法是通过模拟和测试技术实现的。这些 方法随着设计复杂度的增加，很难保证能找到所有的死角错误。然而，形式化 验证方法具有严密的理论体系，能够在数学上证明具体实现和规范之间的一致 性，而不会错过或忽略任何搜索空间。形式化验证方法主要分为两类：演绎方 法和可达性分析。定理证明属于前一种，模型检测属于第二种。 定理证明的基本思想是使用形式化规格语言( 如v d m 、o b j e c t - z 等) 从形式 规格说明中推理系统应具备的性质，看是否符合需求规格。若能推出应有的性 质，则形式规格说明符合设计需求；否则，形式规格说明不完全或存在不一致 性。定理证明的过程就是在验证者的引导下，不断地对公理、已证明的定理施 加推理规则，产生新的定理，直至推导出所需要的定理。定理证明理论上可以 处理无限状态的系统，但由于是交互式的，因此对使用者的要求较高。 模型检测的基本思想是使用状态迁移系统来表示系统行为，使用时态逻辑 公式来描述系统的性质，然后使用一定的算法来穷举系统的每个状态，并判断 每个状态是否都满足系统给定的性质。对于一个有限状态系统，这个穷举验证 过程是可以实现的。但对于一个复杂的系统而言，如果把并发系统显式地表示 为状态转移系统，其状态数量将随着系统线程的并发数呈指数形式增长，这种 情况下使用穷举系统状态的方法是不可行的。因此，模型检测需要重点解决两 个问题，状态空间爆炸和高效的状态搜索算法。 随着软件模型检测技术的不断发展，以及各种状态空间爆炸缓解方法的应 用，已经在一定程度上解决了上述问题。针对不同的应用，已经开发出很多较 为成熟的软件按模型检测工具，其中一个比较著名的就是由n a s a 研发的j a v a 程序模型检测工具j p f 。 1 2 2j p f j p f 是一种可以验证j a v a 字节码程序的系统。从本质上说，它是一个j a v a 虚拟机( y v m ) ，是一种显式状态的软件模型检测工具。它可以系统地遍历一个 程序所有潜在的执行路径，并能够找出死锁、未处理异常等性质冲突。跟传统 2 第1 章引言 的调试工具不一样，j p f 可以报告导致性质冲突的完整的执行路径。j p f 尤其适 用于发现多线程应用程序中难以检测到并行性质冲突。 软件模型检测在理论是似乎是一种安全而又健全的验证方法，事实表明， 它的扩展实现做得并不尽人意。为了让软件模型检测变得更加实际，一个软件 模型检测工具必须具备很好的启发方式和状态抽象。j p f 的可配置性和可扩展 性是独一无二的，它的强项在于，可以为使用新方法来提高可扩展性提供一个 很好的平台。 j p f 是一个纯j a v a 应用程序，它既可以当做命令行工具使用，也可以像开 发环境一样嵌入到系统中去。它至今仍在n a s a 军队研究中心进行主要的开发 和使用。j p f 作为软件模型检测的一种可行性研究方案，始于1 9 9 9 年，它开创 了一种独有的从学术到工业的实现途径。值得一提的是，它已经在航天器软件 的程序设计中检测到了一些问题。 j p f 由美国宇航局艾姆斯研究中心科a s aa m e sr e s e a r c hc e n t e r ) 的健壮软 件工程小组( r o b u s ts o f t w a r ee n g i n e e r i n gg r o u p ) 主持开发，目前已进入它的第四 个开发周期。表l 描述的是j p f 的版本研发历程。 表lj p f 的版本研发历程 版本开始年份特点 v l1 9 9 9 s p i n p r o m e l a 翻译器 v 22 0 0 0 可回溯的状态匹配j v m v 32 0 0 4 基础功能扩展( 监听器、m j i ) v 4 2 0 0 5 第四季度符号执行、选择生成器 2 0 0 5 年4 月，j p f 以n o s a1 3 的许可证进 行开源，它是美国宇航局首个放在公共网站上进行系统开发的案例。一直以来， 该项目在s o u r c e f o r g e 站点上一直由n a s a 的研究人员负责开发和版本更新， 同时他们也招募一些优秀的软件工程师合作开发，一起推动j p f 的开源推广。 2 0 0 9 年3 月，j p f l 4 版正式在s o u r c e f o r g e 站点上发布。 最近两年，为了使更多的程序员能够更好地使用和推广j p f ，国外的一些研 究人员开发出了一些基于j p f 的e c l i p s e 插件，其中比较具有代表性的有j p f e p 和v i s u a lj - p f ( v j p ) 。 3 第1 章引言 1 3 本文的主要内容 第二章以从上到下的方式介绍模型检测、软件模型检测和j a v a 程序模型检 测。第三章阐述j p f 验证j a v a 程序的工作原理及使用到的关键技术。第四章基 于j p f 提出了一种软件模型检测工具的通用实现方法。第五章主要是介绍在 e c l i o s e 中，基于j p f 的j a v a 模型检测平台的实现。第六章给出一些具体程序实 例进行检测，并进行分析，第七章对全文的工作进行总结，同时展望该领域今 后的研究方向。 4 第2 章基本理论 第2 章基本理论 模型检测是一种强大的、高可靠性技术，用于验证系统的正确性。随着计 算机技术的广泛应用，人们对各种软件的依赖程度也越来越高。在众多的工业 案例中，不乏有不可靠系统的出现。这些系统不仅花费巨大，甚至还会带来生 命威胁。由此，软件模型检测技术应运而生。一个软件模型检测工具，可以通 过遍历程序中的所有有限状态和转移，来验证软件系统性质和检测漏洞。模型 检测技术可将一个实际的系统抽象成一个数学模型、将程序性质抽象成基于时 间的属性、将验证过程抽象成自动验证机，通过检测验证对系统中存在的性质 冲突以反例的形式展现出来，可以大大提高软件的可靠性。 2 1 模型检测 简单地说，模型检测是一套用于判断硬件和软件设计的理论模型是否满足 规范的方法。对于一个给定的有穷状态并发程序( 系统) 和表示系统性质的表 达式( 可以是某种时序逻辑公式，或者自动机等) ，然后利用穷举搜索的方法来 判定系统是否满足给定的一组规范。其核心问题是解决状态空间爆炸问题和寻 求高效的搜索算法。本节将介绍模型检测技术的基本概念、基本思想，及其具 体实施方案。 2 1 1 模型检测过程 一个典型模型检测过程，主要包含图2 1 中给出的几个重要步骤。当然这 只是一个基本过程，后面还会提到一些此过程的改进方案。 图2 1 模型检测过程 5 性质满足 反例 第2 章基本理论 针对上图中的过程描述，下面详细介绍一下各个步骤的具体含义。 ( i ) 系统建模：对于一个系统来说，如果需要使用某个模型检测工具来对 它进行检测，就必须将系统描述成为一个模型检测工具可以接受的输入形式。 一般来说，需要用一种模型检测工具的描述语言来将整个系统等价地描述一遍， 要保证系统描述的完备性。有时可能因为系统过于复杂，还将需要使用到抽象 等手段，在保证系统基本性质不变的情况下，做一个概括性的描述。 ( i i ) 性质规范：为了检测一个系统，首先需要给出系统应该满足的一些性 质规范。这些规范通常是以逻辑表达式的形式给出，可以是逻辑时序公式，或 者是由自动机表示的系统属性。 ( 1 1 1 ) 模型验证：按照模型检测技术的定义，在理想状况下，整个检测过程 应该是完全自动的，不需要任何外界力量的介入。而实际上，人的介入在现有 的模型检测系统中是非常必要的。模型检测系统不仅需要人来提供一个可供检 测的系统模型，在需要提供错误路径例的时候，还需要人来对系统输出的错误 路径进行解释，以帮助设计者跟踪错误产生的地方。 在有限状态系统中，上述方案也许可行。还有一种可能就是验证任务可能 不终止或者不正常终止，这可能是因为模型的大小太大使得计算机内存无法满 足要求，这种情况下，通过附加的抽象调整模型然后重新验证。这也就是后面 即将提到的，以反例引导的抽象求精模型检测方法。 2 1 2 模型表示 模型系统可分为：离散系统、实时系统、混成系统、概率系统和p e t r i 网等， 模型检测中常用k r i p k e 结构来表示状态转移系统。具体定义为：假设彳尸表示 一组原子命题，一个的k r i p k e 结构m 是定义在彳尸上的一个四元组 m = ( s ，s o ，r ，l ) 。其中，s 是一个有限状态集合；s o s 是为初始状态集合； r s s 是一个完全的状态转换关系，对每一个状态s s ，至少存在一个状态 j s 使得r k ) 成立；l ：sj2 胛，是一个标识函数，用来表示每个状态中成 立的原子命题集合。有时不太关注初始状态集s o ，通常可以在定义中忽略掉它。 k r i p k e 结构m 中由状态s 开始的一个无限状态序列万= ，s ，s ，表示m 中的 一条路径，其中= s ，且对于所有f 0 ，关系r ( s ，s ) 都成立。 6 第2 章基本理论 2 1 3 性质描述和l t l 逻辑 描述一个系统的性质可以使用自然语言，更好的设计方案是将其描述成一 种模型检测工具可以识别的性质规范。在反应系统中，最常用的方法是使用时 序上的逻辑表达式来描述系统中的状态迁移情况，这就是通常所说的“时序逻 辑”，它是一种有序的形式化方法。在时序逻辑中，要考虑没有显式涉及的时间； 作为代替，一个公式可能指定最终要到达的指定状态或者一个不会进入的错误 状态，用“最终 或“从不”属性通过时序操作符来指定。这些操作符也能和 布尔连接符连接或任意嵌套。 模型检测中用来描述模型的常用时序逻辑有：c t l * 计算树逻辑、c t l 分支 时序逻辑、l t l 线形时序逻辑等。它们都可以有效地描述基于时间的系统事件， l t l 和c t l 都是c t l * 的严格子集，c t l * 涵盖了l t l 和c t l 的表达能力。l t l 和c t l 的表达能力各有所长，它们的描述功能彼此相交且都有对方无法描述的 属性。由于j p f 中需要检测l t l 性质，这里重点描述一下l t l ，其它时序逻辑 公式的详细资料可以参照【4 j 【引。 线形时序逻辑( m ，l i n e a rt i m el o g i c ) ，和其它时态逻辑一样，常用来表 示基于k r i p k e 结构的系统性质。l t l 的语义描述为：对于p 属于原子命题彳尸， 满足：0i - p 1 1 秒p 】f p ) i g p ) f 岛v 吃i 岛 0 2 1 0 , 一岛协吗l 岛形i 岛尺岛。 其中，、f 、g 、【，、r 等大写字母是时态算子，x 表示属性在路径的 下一个状态满足；，表示属性在路径将来的某个状态上满足；g 表示属性在所 有路径状态都满足；j u g 表示路径上将来的某个状态满足g ，在这之前的所有 状态都满足厂；r 是u 的逻辑对偶。 针对j a v a 程序模型检测，如果研究对象是串行程序，那么l t l 将非常适合 用来表示这类程序的性质。虽然l t l 是c t l * 的子集，但它和c t l 一样的强大， 特别是在描述单一路径事件( 非分支程序，如并行或符号化程序) 的时候，l t l 显得更为简单。 2 1 4 模型检测算法 模型检测算法是模型检测技术的核心，它的好坏直接可影响模型检测过程 的执行效率，也就是发现系统性质违例将要花费的时间、空间上的损耗。任何 一个模型检测算法都是基于一定的模型表示方法，在现有的所有表示方法中大 7 第2 章基本理论 体分为两类方式：显式模型检测和隐式模型检测算法。所谓显式模型检测方法 即为采用直观的方式来表示系统的模型，比如k r i p k e 结构，或者自动机的形式， 这些都是基于图理论的，o i l t h e f l y 方法即可归为此类。所谓隐式方法就是间接 的形式来表示系统的模型，比如o b d d 方式其被称为符号化模型检测技术，或 者不直接来表示系统( 基于s a t 的有界模型检测) 。 在众多的模型检测工具中，用得比较多的模型检测算法有：符号模型检测 ( s i g n a lm o d e lc h e c k i n g ) 、限界模型检澳l j ( b o u n d e dm o d e lc h e c k i n g ) 及o n - t h e f l y 模型检测等。关于它们的详细资料可以参照文献【6 】【7 】【引。 2 2 软件模型检测 对于商用软件，或者科学研究软件，它们面临的主要问题之一是如何确保 系统的正确性和稳定性，形式化方法是解决这个问题的重要途径p j 。现有的各 种形式化方法中，模型检测作为一种重要的自动化验证技术已经在硬件和协议 验证领域取得了巨大的成功。模型检测的主要思想是，对系统状态空间进行穷 举搜索，但从实际角度出发，对无限状态系统、巨大的有限状态系统进行穷举 搜索是不可行的。软件属于无限状态系统，普通的模型检测技术需要通过进一 步的改进，才能实现对软件进行有效的检测。软件模型检测大概可以分为对系 统说明( 需求分析) 的模型检测和面向源代码的模型检测【l0 1 ，在软件模型检测中 用得最多的技术是谓词抽象和基于反例引导的抽象求精算法。 2 2 1 谓词抽象 一个复杂的系统模型，通常使用抽象技术【l l 】【1 2 】【1 3 1 来缩减其状态空间。常见 的抽象技术有状态合并、数据抽象和谓词抽象。其中，谓词抽象是一种创建软 件的抽象模型的技术，经过抽象后的模型系统，可以方便地应用各种模型检测 算法。谓词抽象过程，首先需要定义一个有限集合的谓词，然后按照这些谓词 的值来将一个具体无限状态系统的状态映射到抽象状态上，通常以一个有限的 自动机形式存在，自动机的状态表示被选定的谓词的赋真值情况。谓词抽象是 现有的源代码检测工具中使用的最多的抽象方法。 谓词抽象提供了一种将自动将无穷状态系统映射到有穷状态系统的方法。 8 第2 章基本理论 假设一个原型系统的状态空间为s = k x 圪，选定的谓词集合为 扫。，p ：，p 。 ，同时，假设布尔域为b = t r u e ，f a l s e ) ，则状态空间可被抽象 为s 出= n b 。定义从s 到s a b s 的狭义抽象映射： i = 1 聊 厂( j ) = ( s a t ( s ，p 1 ) ，s a t ( s ，p 。) ) 兀b ( 2 1 ) f = l 肌呻胪冀。， 利用谓词抽象的方法，可以将一个j a v a 源程序转换成为等价的布尔型程序。 对于一个语句s 和谓词p ，令s p ( s ，p ) 表示谓词关于语句s 的最弱前置条件，它 的真值与否能够决定执行语句s 后的真值。令“x = e 是一个赋值语句，同时 它也表示一个谓词，表达式s e ( x = e ，p ) 是指将谓词p 中的x 全部用e 来替代， 结果表示为p e l x 】，则有s p b = p ，p ) = p e x 】。 谓词抽象的主要工作是计算谓词的最弱前置条件。假设语句s 在程序点a 和a 之间执行，谓词集合为尸，对应的布尔变量是b 。通过计算卯( s ，p ) 得出p ， 对应的布尔变量为b ，如果b 在a 处为真，则在程序中的a 和a 之间将b 赋值为 真是安全的。但是，如果计算卵( s ，p ) 得到的谓词不在谓词集合尸中，则很有可 能不存在布尔变量6 。例如：假设一个谓词集合p = ( x 3 l ，b 一1 ) 。将x 赋值 为x + 1 ，计算可得：s e ( x = x + l ，x 3 ) = g 2 ) ，可以看出谓词g 3 ) 不在集合 尸中。因此，需要调用判定程序来加强这个最弱前置条件。 这种加强最弱前置条件的形式化算法描述可为：在集合y 上存在一个集合 体c ，表示为一个合取式c 1 ac t ，其中c f 6 ，- 1 玩 ，6 ，v 。由集合矿上的 所有集合体组成的集合记为c u b e so v e r ( v ) 。对任一个谓词p 和布尔变量集合 y ，令胁( p ) 表示在c u b e sd v p ，( y ) 上满足9 ( c ) 蕴含p 的最大析取式，公式表示 为：胁0 ) = v c i b c u b e s o v e r ( v ) 9 ( c f ) 一p 。若存在变量b f v ，则加f ) 表示6 j 对应的谓词p ，缈( 16 f ) 表示谓词叩。谓词伊洳0 ) ) 就表示在伊缈) 上蕴 含p 的最弱谓词。对于前面的例子，v = b 3 ， x 一1 ) 尸= 戤 3 ) g 一1 ) ， 计算可得：m v ( x 2 ) - - 扛一1 ，缈( 胁g 2 ) ) = g 1 ) 。同理，若定义g v 0 ) 为 9 第2 章基本理论 1 胁h ) ，则可得到妒) 上的被p 蕴含的最强谓词，表示为缈( g v 0 ”。 利用上面的算法可以处理j a v a 中的基本语法结构，包括：赋值语句、条件 语句、循环语句、类对象引用、类成员方法和方法调用等。一个简单的j a v a 程 序的谓词抽象过程如图2 2 所示。 源程序 + 谓词布尔型程序 图2 - 2 谓词抽象 2 2 2 反例引导的抽象求精 基于抽象验证抽象求精的方法是一种通常的软件模型检测方法。这种方 法的般步骤如下： ( 1 ) 抽象：将程序的具体状态以抽象的形式表示，建立给定程序的抽象模型。 ( 2 ) 验证：使用性质属性自动地验证抽象模型，如果给定程序的抽象模型没 有破坏属性，那么给定程序也不会破坏属性，返回“程序正确”；否则，自动产 生一个抽象反例路径，显示导致性质冲突的具体轨迹。 ( 3 ) 抽象求精：自动检测抽象反例路径的真实性，判断其是否对应一个程序 中的具体反例，如果存在具体反例，则表示找到了一个程序错误；否则，表明 程序的抽象模型过于粗糙，缺少证明程序满足被验证属性所需的足够信息。因 此，需要增加信息，以抽象出更精密的抽象模型。跳转到步骤( 1 ) 。 可以看出，抽象求精过程的特点是“运行时改变抽象策略，利用反例的 信息进行抽象模型精化，面向验证目标逐步地自动修正抽象系统。这种基于反 例引导的抽象求精机制，有助于使模型在必要的地方足够精密，在不必要的地 方足够简略，从而提高验证效率。图2 3 描述的是反例引导的抽象求精框架。 l o 第2 章基本理论 图2 3 反例引导的谓词抽象求精框架 2 2 3 面向源代码的软件模型检测 面向源代码的软件模型检测是指直接从源代码的角度提取信息，自动构造 和修正模型的方法【1 4 1 。它本身就是以代码的形式存在，既方便用户省去了传统 方法中手工建模的步骤，又保证模型的准确性和精度，因此具有较高的实用性 和研究价值。该方法需要建立一个变迁系统，确定验证目标，使用谓词抽象方 法来缩减状态空间，其具体验证步骤跟反例引导的抽象求精方法一致： ( 1 ) 初始抽象 初始抽象非常简单，它是基于程序语句结构生成的，只需要考虑最基本的 顺序和分支语句。图2 4 中的左侧的一段源程序，右侧为其对应的初始抽象图。 图2 _ 4 初始抽象 上面的初始抽象图实际上是一个简单的c f a ( c o n t r o lf l o wa u t o m a t o n ，控 制流自动机) 【1 5 】。c f a 可以理解为程序执行流程图，同时它本身也是一个抽象状 ：口 第2 章基本理论 态迁移系统。在没有添加任何谓词的情况下，它的抽象映射形式为： f ：d p c d l d 2 d 月 d 彤 图2 - 4 中的节点7 对应着程序中的错误语句“e r r o r ，它表示返回一个 错误状态。由于当前的谓词集合为空，状态过于抽象而导致迁移不受限，图中 存在一条明显的反例路径，使得节点7 是可达的。为了精化粗糙的初始抽象系 统，需要加入新的谓词。一般情况下，可以利用反例分析计算插值的方法来发 现新谓词。对于尚无谓词的初始抽象系统，可略过反例分析步骤而直接选取一 个或多个初始谓词。通常使用程序中第一条赋值语句或条件语句作为初始谓词。 ( 2 ) 状态搜索验证 选择新谓词的目的，是重新构造或精化抽象系统，使得新抽象的系统比前 者更精细、表达能力更强。对于从语句序列构造的程序模型，之前使用的c f a 图仍然可以用来构造、更新和表达抽象模型。下一步的工作是，基于原有c f a ， 使用新的谓词集合沿执行路径计算和表达各节点的新的抽象状态空间。 抽象的过程，需要建立精确状态空间和抽象状态空间之间的映射关系。面 向源码的模型存在一个重要的特点，它保留了所有有关程序当前运行位置( t i p p c ) 的信息，这对状态映射是非常重要的。假设谓词集合为扫。，p ：，p 肿 ， 则狭义和广义抽象映射关系可分别表示为： j l f ：d m d l d 2 d 。寸d 盯ii 曰 t ：d 盯2 q 加2 。加。专d | p ( 兀b i f f i l 通过前一节点的状态空间s 。和语句s t 的语义，可以计算得出后一个节点 的状态空间s p o , ，。计算后继节点状态的方法分为两步：计算s 朋执行s t 语义 后的精确状态空间s 。耐( 最强后置条件) ；将s 删通过广义抽象映射t 映射到 抽象状态空间d ，丌b - 上。 v 工工 t = l ( 3 ) 反例验证 通过上一步发现的反例路径需要进行分析，以确认它是真反例还是伪反例。 实现该验证过程，可以从反例路径末端的错误节点出发，逆向地沿着反例路径 向上，检验计算可达状态空间的路径。具体步骤为：尽可能大地设置初始状 态空间为 粥d 。，丁，丁 ，然后向上逆向计算前一个节点的最大可能的状态 1 2 第2 章基本理论 空间。每次通过计算得到前一节点的状态空间，和向前搜索得到的状态空间 矽向删求交。若矽向ak = 矽，则说明此反例路径是不可达的( 伪反例) ；若 矽加呦d k ，则再计算上一个节点的状态空间。当搜索到系统的起始节点， 两个状态空间的交仍为空，则可断定此条反例路径是存在于原系统的真反例。 ( 4 ) 抽象求精 导致当前抽象系统过于粗糙的原因，在于抽象过程中存在伪反例路径，需 要通过反例来引导抽象求精工作。从伪反例路径本身寻找隐藏其中的信息来帮 助寻找新谓词，从而对当前抽象系统进行合适和必要的精化。 当后向搜索状态空间k 和前向搜索时的妒觚删在某节点交集为空时，设 从它到错误节点的路径上的语句序列为s t ，s t ，s t 。，则必有 c f o r w a r d s t las t 2 人s t 。不可满足。可利用c r a i g 插值公式 1 2 等方法计算出 若干个插值，并加入到新的谓词集合中。新谓词的发现，关键在于采用何种插 值算法，此内容还有待进一步的深入研究。 2 2 4 软件模型检测工具 随着软件模型检测技术的不断发展，许多非常优秀的软件模型检测工具陆 续出现。其中有很大一部分都采用了谓词抽象技术，s l a m ，m a g i c ，b l a s t 都是基于谓词抽象，但各个工具在具体的细节特点上存在一定的差异。b l a s t 利用了l a z ya b s t r a c t i o n 1 6 】技术，m a g i c 则使用了组合推理来验证组件的规格说 明和c 语言实现的一致性【1 7 】，s l a m 采用的是将程序程序转换成布尔程序 ( b o o l e a np r o g r a m ) 1 1 8 1 后进行迭代求精的技术。j p f 也使用到了谓词抽象技术。 上述这些检测工具都还存在一定的缺陷，比如支持的语言中往往比较单一， 更注重控制流等。软件模型检测还处在起步阶段，距离真正成熟还有许多工作 要做。 2 3j a v a 模型检测 在2 0 0 9 年的t i o b e 编程语言排行上，j a v a 位居第一，这也是它连续五年卫 冕此项殊荣。j a v a 是s u n 公司推出的新一代面向对象程序设计语言，设计它的 初衷是为家用消费电子产品开发一个分布式代码系统，实现与电冰箱、电视机 第2 章基本理论 等家用电器之间的信息交流。现如今，由于j a v a 本身跨平台、易于移植等优点， 它已成为技术人员的一种时尚。无论使用什么开发语言来编写软件，都应该为 软件应具体的可靠性和稳定性负责。作为当前软件编写的主流开发语言之一， 有必要对j a v a 程序本身进行严格地检测，以保证其编写的程序能够给用户带来 更可靠的用户体验。 2 3 1j a v a 程序特点 j a v a 体系结构包括四个独立但相关的技术：1 ) j a v a 程序设计语言；2 ) j a v a c l a s s 文件格式；3 ) j a v a 应用编程接h ( a p i ) i4 ) j a v a 虚拟机【1 9 1 。编写并运行一个 j a v a 程序，首先将它编译成j a v ac l a s s 文件，然后再在j a v a 虚拟机中运行c l a s s 文件。当编写程序时，通过调用类( 这些类实现了j a v a a p i ) q b 的方法来访问系统 资源( 比如i o ) 。当程序运行的时候，它通过调用c l a s s 文件中实现了j a v aa p i 的方法来满足程序的j a v a a p i 调用。这四者之间的联系如图2 5 所示。 图2 - 5j a v a 编程环境 j a v a 虚拟机( m ) 和j a v aa p i 一起组成了一个“平台 ，所有j a v a 程序 都在这上面编译。j a v a 编写程序都运行在j v m 中，在m 的内部，程序的多 任务是通过线程来实现的。每用j a v a 命令启动一个j a v a 应用程序，就会启动一 个m 进程。在同一个m 进程中，有且只有一个进程，就是它自己。在这 个m 环境中，所有程序代码的运行都是以线程来运行。 每一个线程都有一个保存帧的栈。在每一个方法调用的时候创建一个帧。 一个帧包括了三个部分：操作栈，局部变量数组，和一个对当前方法所属类的 常量池的引用。 局部变量数组也被称之为局部变量表，它包含了方法的参数，也用于保存 1 4 第2 章基本理论 一些局部变量的值。参数值得存放总是在局部变量数组的i n d e x o 开始的。如果 当前帧是由构造函数或者实例方法创建的，那么该对象引用将会存放在 l o c a t i o n o 处，然后才开始存放其余的参数。 局部变量表的大小由编译时决定，同时也依赖于局部变量的数量和一些方 法的大小。操作栈是一个( l i f o ) 栈，用于压入和取出值，其大小也在编译时 决定。某些o p c o d e 指令将值压入操作栈，其余的o p c o d e 指令将操作数取出栈。 使用它们后再把结果压入栈。操作栈也用于接收从方法中返回的值。 垃圾收集器( g c ) 会自动释放在j a v a 虚拟机的堆里不再被程序所使用的对 象，可以帮助程序保持完整性，防止j a v a 程序员因失误( 或者故意) 错误地释放 内存而导致j a v a 虚拟机崩溃。使用垃圾收集，有一个潜在的缺陷是它加大了程 序负担，可能影响程序性能。j a