（计算机应用技术专业论文）与测试相结合的系统安全性验证技术研究.pdf

【一 原创性声明 本人声明：所呈交的学位论文是本人在导师的指导下进行的研究工作及取得的研究成 果。除本文已经注明引用的内容外，论文中不包含其他人已经发表或撰写过的研究成果，也 不包含为获得囱苤直太堂及其他教育机构的学位或证书而使用过的材料。与我一同工作的同 志对本研究所做的任何贡献均已在论文中作了明确的说明并表示谢意。 学位论文作者签名：兰龇指导教师签名： m 茄 日期：2 里! 旦! 多：! 生日期：羔型堡翌多：， 在学期间研究成果使用承诺书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：内蒙古大学有权将 学位论文的全部内容或部分保留并向国家有关机构、部门送交学位论文的复印件和磁盘，允 许编入有关数据库进行检索，也可以采用影印、缩印或其他复制手段保存、汇编学位论文。 为保护学院和导师的知识产权，作者在学期间取得的研究成果( 含计算机软件、程序) 属于 内蒙古大学计算机学院。作者今后使用涉及在学期间主要研究内容或研究成果，须征得内 蒙古大学计算机学院就读期间导师的同意；若用于发表论文，版权单位必须署名为内蒙古大 学计算机学院方可投稿或公开发表。 肭新 日期：璺竺! ! ：里多：1 4日期：基里丝：! 彩，年 计算机学院院长签字： 日期： 0 8唧2m 6删3m，劓iiy _ 矿、 、 目前 件的安全 经过测试 件证实方 术和测试 性缺陷为 局限性所 下几个方 ( 】) 全性的定义；( 2 ) 提出了寻找系统安全性问题的s d r 算法，并利用现有的程序 模型检测工具找到系统中存在的安全性问题；( 3 ) 对所找到的违背系统安全性 的迹，根据其不同的类型实施不同的处理，使得系统的安全性问题最终得到彻 底的解决。 在实验阶段，本文使用咖啡机的例子说明了该软件工程方法的实际流转程 序，并使用上述的软件工程方法对a t m 系统进行了分析并找到了违背安全性的 反例。 关键词：模型检测：软件测试：验证：i o c o 一致性：a t m 与测试相结合的系统安全性验证技术研究 i l 内蒙古人学硕十学位论文 r e s e a r c ho fs y s t e ms e c u r i t yv e r i f i c a t i o n t e c h n o l o g yc o mb i n e dw i t ht e s t i n g a b s t r a c t n o w a d a y s ，t h et e c h n i q u eo fv e r i f i c a t i o na n dt e s t i n ga r el e a r n i n gf r o me a c h o t h e ri nm u t u a le m u l a t i o na n dd ot h e i rb e s tt oi m p r o v et h es a f e t y , r e l i a b i l i t yo ft h e s o f e w a r e o n ek i n do fv e i l f i c a t i o na p p r o a c hw h i c hc a l l e dm o d e lc h e c k i n gn o wc a n b eu s e di nt e s t i n g ，a n dt h ec o n f o r m a n c ec o n c l u s i o nw h i c hd e r i v ef r o mt e s t i n gn o w c a nb eu s e dt oi m p r o v ev e r i f i c a t i o na n dm a k ei tm o r ep e r f e c t s ot e s t i n ga n d v e r i f i c a t i o na r ep l a y i n gac o m p l e m e n t a r yr o l ei nt h ea p p r o a c ho fv a l i d a t i o n ，a n d w i l lb eg e t t i n gm o r ea n dm o r ec l o s e ri nt h ef u t u r e t h i st h e s i ss t a r t sw i t ha n a l y s i n g t h ee x i s t e n c ed e f e c t so fi o c oc o n f o r m a n c e ，t h e ns u c c e s s f u l l yw o r k i n go u tt h e s y s t e ms a f e t yp r o b l e m sw h i c ha r o u s e db yl i m i t a t i o no ft h et e s t i n g ，t h r o u g ht h eu s e o fs o f t w a r em o d e lc h e c k i n ga p p r o a c h t oc o m p l e t et h i sw o r k ，t h ef o l l o w i n gs e v e r a l a s p e c t so ft h er e s e a r c hw o r km a i n l yh a v e b e e nd o n e ： f i r s t ：r e s e a r c ho nt h et w ok i n d so fd e f e c t sw h i c ha r o u s ef r o mi o c o c o n f o r m a n c e ，a n dg i v e nt h ed e f i n i t i o no fv o l a t i n gt h es y s t e ms a f e t yp r o p e r t i e s ； s e c o n d ：i n t r o d u c i n gt h es d ra l g o r i t h m sw h i c hc a nb eu s e df o rf i n d i n go u tt h e p r o b l e m so fs y s t e ms a f e t yp r o b l e m ；t h i r d ：w o r ko u tt h ep r o b l e m ，b yu s i n gt h e d i f f e r e n tw a y st od e a lw i t hd i f f e r e n tt r a c e sw h i c hh a sb e e nf i n do u ta n db e e n c l a s s i f i e da st w ok i n d so ft r a c e s 1 1 1 与测试相结合的系统安全性验证技术研究 d u m i n gt h ee x p e r i m e n t a lp h a s e ，t h em e t h o d o l o g yw h i c hh a sb e e nm e n t i o n e d a b o v ea r eu s e dt oa n a l y s et h es i m u l a t i o ns o f t w a r eo fa t m ，a n ds h o wh o wi tw o r k s w i t ht h ee x a m p l eo fc o f f e em a c h i n e k e y w o r d s ：m o d e lc h e c k i n g ；s o f t w a r et e s t i n g ；v e r i f i c a t i o n ；i o c oc o n f o r m a n c e ； a t m ， 内蒙古人学硕十学位论文 目录 摘要 a b s t r a c t 目录 第一章绪论 1 1 引言 1 2 形式化验证技术 1 2 1 验证技术的研究现状 1 2 2 模型检测 1 2 3 验证技术面临的主要问题和优化技术 1 - 3 测试技术 1 3 1 软件测试、协议测试 1 3 2 测试的缺陷与发展 1 3 3 测试与验证的结合 1 4 主要内容和贡献7 1 5 论文结构8 第二章程序模型检测和i o s t s 系统9 2 1 程序模型检测技术介绍9 2 2 相关工作介绍1 0 2 2 1 程序模型检测的主要工具和方法1 0 2 2 2 程序模型检测的两阶段框架1 2 2 3s p i n p r o m e l a 概述12 2 4c 程序模型检测工具c o p p e r 简介1 3 2 5 测试与验证的模型1 6 2 5 1i o s t s 模型的定义1 6 2 5 2i o s t s 上的基本操作1 7 v 与测试相结合的系统安全性验证技术研究 2 6 本章小结18 第三章i o c o 一致性所存在的问题和系统安全性1 9 3 1i o c o 一致性19 3 1 1i o c o 一致性的概念1 9 3 1 2i o c o 一致性的两类缺陷2 l 3 2 系统安全性2 5 3 2 1 问题回顾2 5 3 2 2 违背安全性的迹以及系统违背安全性的定义2 5 3 3 木章小结2 6 第四章s d r 算法与应用实例介绍2 7 4 1 将c o p p e r 的输出转化为i o s t s 表示2 7 4 2 安全性缺陷补救算法s d r 3 0 4 3 使用s d r 算法弥补i o c o 一致性缺陷3l 4 3 1 工作原理31 4 3 2 技术方法3 3 4 4 使用s d r 算法对a t m 系统进行安全性验证实例3 9 4 5 本章小结4 3 第五章结论和进一步工作4 4 5 1 论文总结一4 4 5 2 进一步工作4 4 参考文献4 6 致谢4 9 附：攻读硕士期间参加的研究项目5 0 v i 内蒙古人学硕+ 学位论文 图表目录 图1 1 模型检测器的结构d 1 图2 1 程序模型检测的两阶段框架i 图2 2p h i l o s o p h e r s p e c 文件 。 图2 3p h i l o s o p h e r p p 文件 图2 4 使用c o p p e r 对某性质进行的检测 图3 1i o c o 一致性的表述0 1 1 1 图3 2i o c o 一致性的第一类缺陷 图3 3i o c o 一致性的第一类缺陷的成因 图3 4i o c o 一致性的第二类缺陷 图3 5i o c o 一致性的第二类缺陷的成因 图4 1c o p p e r 的反例输出可以表示为i o s t s 系统 图4 2c o p p e r 的输出中含有能够表示i o s t s 中的变迁的内容 图4 3 利用s d r 算法弥补i o c o 一致性的原理图 图4 4 咖啡机例子的初始模型 图4 5 咖啡机程序的运行情况 图4 6 咖啡机例子对是否存在吃币现象的检测 图4 7 咖啡机例子中分支结构的检测 图4 8 咖啡机的实现的检测结果 图4 9 对实现进行修改之后 ， 图4 1oa t m 机模型软件的系统模型 图4 1 1 对a t m 机模拟软件的迹包含关系检测4 0 图4 1 2 对a t m 机模拟软件的性质违背检测4 1 图4 13a t m 机模拟软件存在的缺陷演示4 2 v i i 与测试相结合的系统安全性验证技术研究 v i i i 1 1 引言 如今计 备在研制阶 件工程方法 击在网络节 全性预防不 系统安 国驻联合国 件全部扫描 统，可以在 平时正常工 所以迫切需 目前， 所未有的挑 形式化方法 靠的形式化 测试是 的执行需要 示的，实现需要不断调整自己以保持与规格说明的一致性。与之相关的测试就是一致性测 试，通常是先根据规格说明产生测试用例，然后将输入送到被测试的实现中，并接收实现 产生的输出与预期的输出相比较，从而得出实现与规格说明是否一致的结论。比较经典的 一致性关系有i o c o 一致性( i n p u ta n do u t p u tc o n f o r m a n c e ) ，它是j a nt r e t m a n s 于1 9 9 6 年提出的。它所存在的问题是：实现与规格说明的i o c o 一致性只能保证对于规格说明中 规定了的内容，实现与其相一致，并不能对规格说明之外的实现给出任何的约束。而实现 是多样的，多样的实现会在很多方面违背系统本来应该具有的性质，譬如说安全性。所以 如何针对这种现状提出能够避免实现跃出规格说明范围违背系统应具有的性质就成为一个 与测试相结合的系统安全性验证技术研究 研究趋势。 与测试不同，验证是通过检查规格说明是否具有本来应该具有的性质而不断完善规格 说明的方法。目前作为检验一个系统实现是否与它的规格说明相一致的方法，验证和测试 技术正越来越紧密的相互结合起来。通过对实现进行测试可以完善对系统的验证，而许多 验证方法比如说模型检测也逐步应用到了测试领域中。测试与验证方法的不断结合使得越 来越多的难题得到了解决。 如何不断完善系统原有的规格说明，让规格说明更广的覆盖实现，找出规格说明和实 现所违背的性质，并对规格说明和实现进行修改，以确保实现与规格说明相一致，这是本 文所研究主要内容。 1 2 形式化验证技术 1 2 1 验证技术的研究现状 所谓形式化方法原则上就是用数学与逻辑的方法描述和验证系统。调试和测试的局限 在于不能从正面说明软件的正确性和可靠性，所以引入形式化验证方法是想为程序做一些 如同数学为工程所做的工作，即提供能描述和推断计算机程序的符号方法。可以在组成程 序的符号串上定义变换，通过结果能够推断在该程序控制下，计算机将如何工作。如果这 个推断与程序输入数据的特定值无关，则这个推断就变成关于那个程序的一般陈述。如果 能形成一个论证该程序达到其目的的一般陈述，则可用它代替穷举性的测试，并称之为正 确性证明。软件的形式化验证就是对软件进行正确性证明。 现在软件形式化验证主要有两类方法，定理证明和模型检测。定理证明以逻辑推理为 基础，根据公理和形式推演规则来验证设计实现是否满足要求，由于需要人工干预，能处 理的设计规模较小，发展比较缓慢，而模型检验则以穷尽搜索为基础，由于能实现需求和 代码的自动查错而得到迅速发展。心h 1 形式化验证采用穷尽搜索的方法来验证系统，它用数学可证明的形式来验证系统的正 确性，因此成为近年来验证技术的一个研究热点。i n t e l 、i b m 等公司都对形式化验证技术 进行了大量的研究，并把形式化验证技术应用到了它们的芯片或者其他系统的设计中。 2 内蒙占人学硕十学位论文 1 2 2 模型检测 模型检测( m o d e lc h e c k i n g ) 是一种很重要的自动验证技术。它最早由c l a r k e 和e m e r s o n 在1 9 8 1 年分别提出的，主要通过显式状态搜索或隐式不动点计算来验证有穷状态并发系统 的模态命题性质。由于模型检测可以自动执行，并能在系统不满足性质时提供反例路径，因 此在工业界比演绎证明更受推崇。尽管限制在有穷系统上是一个缺点，但模型检查可以应用 于许多非常重要的系统，如硬件控制器和通信协议都是有穷状态系统。 模型检测的概念： 令m ( m o d e l ) 是个k r i p k e 结构( 即一个状态变迁图) ，令f ( f o r m u l a ) 是一个时序逻 辑公式。穷尽的查找m 中的所有状态s ( s t a t e ) ，使得m ，s i = f 。 模型检测方法要确定时序公式f 是否在k r i p k e 结构m 上保持为真，即是否结构m 是公 式f 的一个模型。c l a r k e 和e m e r s o n 给出了模型检测时序逻辑c t l 的多项式时间复杂度算 法。图1 1 显示的就是一个典型的模型检测系统。一个预处理器从一个程序或电路中提取 出状态变迁图，然后由模型检测引擎判定公式f 是否在状态变迁图上保持为真。 下 瓦z 翮lt rue甜falseplrogramc t t c u l t l 钟 ll 竺一l ， - _ _ - - - 。_ _ 。- _ 。- - - 。”_ - _ - 。_ - 畔t 图1 1 模型检测器的结构“1 f i g u r e1 1t h es t r u c t u r eo fm o d e lc h e c k i n g 模型检测的思想是：先建立待测系统的有限状态模型，然后用算法穷尽检测模型的状 态，判断其是否满足待测属性。模型检测方法最早称为状态空间方法，后来为了克服状态 空间爆炸，进入了很多的化简机制，称为模型检测方法。瞄1 模型检测分为三个步骤： ( 1 ) 、系统建模：每个不同的模型检测工具都有各自的建模语言。 ( 2 ) 、建立规范：不同的模型检测工具对规范的描述有不同的要求。 ( 3 ) 、系统验证可能产生三种结果：出错路径指出系统不满足规范，这说明系统模 型或规范不正确，需要修改； 结果显示正确( 表示模型满足性质) ； 与测试相结合的系统安全性验证技术研究 状态爆炸使得检测任务非正常终止。 模型检测的优点瞄3 ：比起自动化定理证明或证明检验等其他验证技术，模型检测技术具 有更多的优点，如下所示： l 、没有证明。使用模型检测器的用户不需要构造正确性证明。用户只需要将想要验证 的程序或电路的描述以及这些程序所需要满足的性质输入到模型检测器中，然后模型检测 器就会给你有关程序或电路是否满足性质的结论，检测的整个过程是完全自动的。 2 、快速。在实践中，模型检测方法比起其他的验证方法( 比如证明检验) 更快速。证 明检验通常要求用户以交互的模式工作几个星期。 3 、反例诊断。如果规格说明不满足性质，模型检测器将牛成一个反例告诉你为什么规 格说明并不保持性质。不能够小瞧这些生成的反例路径，对于调试比较复杂的系统来说， 反例是无价的。一些人之所以使用模型检测方法就是因为模型检测方法具有这个特性。 4 、允许只使用部分的规格说明进行模型检测。不必等整个程序或电路都建成再进行模 型检测。因此模型检测方法可以用于设计复杂的系统，用户不必等到整个设计过程都完成 才开始验证。 5 、时序逻辑可以很容易的表达并发系统的许多性质。这一点非常重要，因为对于并发 系统来说性质的保持通常非常微妙，人工验证所有可能的情况非常困难。 模型检测按照模型及属性的描述方式不同分为两类：自动机模型检测和时序逻辑模型 检测。 模型检测的相关工具和技术有：s m v ( s y m b o l i cm o d e lc h e c k i n g ) ，s p i n ( s i m p l ep r o m e l a i n t e r p r e t e r ) ，s c r ，n i t p i c k ，m u r p h i ，b d d s 等。 模型检验所要检验的性质主要有三种类型，即安全性( s a f e t y ) 、活性( 1 i v e n e s s ) 和公 平性( f a i r n e s s ) 。安全性描述的是坏的事件永不发生，活性描述的是好的事件终将发生， 公平性描述的是某事件必须无限经常地发生。 1 2 3 验证技术面临的主要问题和优化技术 作为验证技术的主要手段，模型检测方法所面临的主要困扰就在于状态空间爆炸问题， 下面主要介绍一下状态空间爆炸问题： 先介绍一下状态爆炸问题的成因，模型检测给予对系统状态空间的穷举搜索，其状态 的数目往往随着并发分量的增加呈指数增长。因此，当一个系统的并发分量较多时，直接 4 内蒙古人学硕+ 学位论文 对其状态空间进行搜索实际上是不可能的。 模型检测中状态爆炸的优化技术和常用的减少和压缩状态空间的方法主要有：二叉决 策图( b d d ) ( b i n a r yd e c i s i o nd i a g r a m s ) 、符号模型检测( s m c ) ( s i g n a lm o d e lc h e c k i n g ) 、 偏序规约、抽象技术、组合逻辑等。下面将对有代表的状态空间优化技术进行简要的描述： 【3 】【剐【6 【7 】 首先介绍二叉判定图( b d d ) 它利用树的结构管理状态空间，还出现了改进的有序二又 判定图( o b d d ) ( o r d e r e db i n a r yd e c i s i o nd i a g r a m s ) 方法作为它的改进方法，能够将b d d 方法的状态空间继续进行压缩。根据化简规则，它是按指数级增长的布尔函数的正则表示， 因此它更简洁。其次是定界模型检验方法，它能解决很多不能由基于b d d 的方法所解决的 问题，但是它并没有解决空间爆炸问题，定界模型检验是基于s a t ( s a t i s f i a b i1 i t y ) 的模型 检验，已证明是n p c o m p l e t e 问题，但在实际应用中却很有效。第三是符号模型检测方法， 可以表示为l t l ( l i n e a rt e m p o r a ll o g i c ) ，和c t l ( c o m p u t a t i o n a lt r e el o g i c ) 时序逻辑 公式，它们用公式将属性表示为：a g ( p a f q ) 。它通过二叉判定图表示系统模型，通过“u 一演算”来计算出满足系统规范的状态集合，从而方便地在超大规模的状态空间中用来验证 系统的性质。此外还有化简并发进程执行次序、减少重复验证路径的偏序规约方法和基于 自动机理论，通过对表示系统模型的自动机和表示规范的补自动机求交来判定系统是否满 足特定属性的o n - t h e - f l y 模型检测方法等等。抽象技术和组合推理也能够在很大的程度上 化简和压缩状态空间，并应用到模型检测技术之中。 模型检测技术最早应用于检测硬件系统，后来由于各种网络协议本身带有明确的规格 说明( 例如r f c 文档) ，才使模型检测技术逐步应用到网络协议验证上来，但是对于软件的 模型检测始终都因为软件中数据的无界性和模型的复杂性而发展缓慢，直到出现t n 词抽 象方法，它通过先给定一个有限的谓词，然后按照这些谓词的值来将一个具体的无限状态 系统的状态映射到抽象状态上来压缩状态空间( 谓词抽象是现有的源代码检测工具中使用 最多的抽象方法) 。 后来出现了使用模型检测方法对程序的源代码进行验证。这种方法目前处于理论研究 水平，其大体过程是先对程序进行控制流提取，最为常用的有使用j a v ap a t hf i n d e r 工具 来提取j a v a 程序的控制流( 以及对c 语言程序进行控制流提取的c o p p e r 工具) ，然后根据 程序所需要满足的性质使用流分析模型检测工具找出程序中违背性质的反例轨迹。 与测试相结合的系统安全性验证技术研究 1 3 测试技术 软件测试作了如下定义：软件测试是使用人工或自动手段来运行或测定某个系统的过 程，检验它是否满足规定的需求或是弄清预期结果与实际结果之间的差别。软件测试是一 项需要经过设计、开发、和维护等完整阶段的软件工程。 测试是一种活动，在该活动中一个系统或组成部分在特定条件下被运行，结果被观察 或记录，并对该系统或组成部分的某些方面进行评估。测试有两个显著的目标：找出故障 或演示软件执行正确。 测试用例是为特定的目的而开发的一组测试输入、执行条件和预期结果。测试用例是 执行的最小实体。相比之下，测试套是为了测试系统的一组测试用例的集合。 在软件开发原则一文中，提出了软件测试应当遵循的六条指导原则用于指导如何 实施测试。 1 3 1 软件测试、协议测试 软件测试一般可以分为黑盒测试( 又称功能测试) 和白盒测试( 又称结构测试) 以及 灰盒测试三种。 协议测试是在软件测试的基础上发展起来的。协议测试包含一致性测试、互操作性测 试和性能测试三种类型。其中，一致性测试是其他两种测试的测试基础。协议测试中的一 致性测试是一种“功能测试”，它依据一个协议的描述对协议的某个实现进行测试。 1 3 2 测试的缺陷与发展 测试是通过实验的方法找出错误的过程。在实验过程中，检查协议实现是否做了要做 的事仅是成功的一半，另一半是要看它是否做了不要它做的事。由于对一个系统进行无穷 无尽的测试是不现实的，所以测试并不能保证一个协议实现的完全正确性，即测试只能表 明实现“存在错误”，而不能证明实现是“正确的”。所以，对非法的和非预期的输入情况， 也要象对合法的、预期的输入一样，编写测试用例。 为了解决无法对软件或协议穷尽测试的缺陷，出现了使用模型检测技术测试软件系统 的方法，因为模型检测的结果能够产生出反例，所以也可以将模型检测技术用于测试理论 中用于发现错误，实现了验证方法与测试方法的相互融会贯通。由于测试和验证走得越来 6 内蒙古人学硕十学位论文 越近，很多验证技术目前都应用到测试领域中了。8 m j n 邮n 2 1 1 3 3 测试与验证的结合 对于系统的证实工作来说，验证和测试起着互补的角色。验证用于确保规格说明 s ( s p e c i f i c a t i o n ) 满足需求r ( r e q u i r e ) 。而测试是用于确保实现i ( i m p l e m e n t a t i o n ) 与规 格说明s 相一致。传统的软件工程方法是：首先，使用模型检测的方法自动验证规格说明s 。 是否满足需求r ；然后，由用户提出需要在实现i 上进行测试的抽象的测试序列( 即测试目 的) ；接下来，使用测试牛成工具根据测试目的从规格说明s 中产牛出测试用例；最后，在 实现i 上执行测试用例，并利用产牛出的判定结果来说明实现i 与规格说明s 之间是否具 有一致性关系。 这种传统的软件工程方法的缺点是：不能够保证在实现i 上被测试的需求就是在规格 说明s 上被验证的需求。这是因为在测试牛成步中使用的测试目的( 用户提出的抽象测试 序列) 是用于一致性测试的，它与需求r 是相互独立的。这代表可能会发生这样一件事情： 如果一些关键的安全性需求r 被测试目的所遗失，最终的实现i 有可能会违背需求，并且 这种违背将是检测不到的。作为证实系统的过程来说，其实主要包括的就是验证和测试者 两个阶段，所以主要专注于对规格说明，需求和实现的形式化研究。在将形式化验证和 一致性测试集成到交互式系统中n 3 1 一文中很好的将形式化验证和一致性测试结合起来对 交互式系统进行了证实工作，并且利用测试的结果完善了验证。其中规格说明s 被定义为 i o s t s 系统，需求r 用观察者o b s e r v e r s 建模，实现使用i o l t s ( i n p u t o u t p u tl a b e l e d t r a n s i t i o ns y s t e m s ) 表示或使用代码级的实现。其中规格说明与实现之间的一致性关系用 i o c o 一致性( 输入输出一致性) 来表示( 在后面我们常写成：ii o c os ) ，测试牛成算法采用与 i o c o 一致性相配套的测试牛成算法。最终实现既能够检测实现是否违背性质又能检测实现 是否违背规格说明的高效率的测试用例，并根据测试的结果完善了验证。哺1 2 侣们n 鲫n 6 邶1 一直以来，对于分析和检测系统的正确性、证实系统来说，测试和验证是互补的技术。 1 4 主要内容和贡献 正是因为验证和测试技术在证实系统的过程中不断的相互借鉴，互相依赖，才使得一 整套的软件工程方法能够确保实现的正确性。本文利用验证的技术完善了测试，并通过测 7 与测试相结合的系统安全性验证技术研究 试的结果反过来了完善了验证。主要的内容和贡献如下： ( 1 )i o c o 一致性关系的研究：主要研究了传统的i o c o 一致性关系的特点和其先天 就具有的两类缺陷，将i o c o 一致性关系的两类缺陷定义为系统违背安全性的两种情况。 ( 2 )弥补i o c o 安全性缺陷的s d r 算法：通过对程序进行模型检测的方法寻找到违背 系统安全性的两类迹，并且根据找到的第一类迹对实现进行修改，根据找到的第二类迹对 模型进行完善，之后修改实现。并将整个过程抽象成弥补i o c o 安全性缺陷的s d r ( s a f e t y d e f e c t sr e p a i r ) 算法。 ( 3 )将对程序进行模型检测的反例输出结果反馈到系统模型中的方法研究：想要从 程序的违背安全性的迹中区分出哪些是存在于规格说明s 中的( 模型错误) ，哪些是只存在 于实现i 中的( 实现错误) ，这就涉及到将模型和反例进行处理，使得反例和模型最好具有 统一的描述形式。 1 ，5 论文结构 论文共五章：第一章绪论，介绍了形式化验证和一致性测试的概念以及目前的发展现状。 第二章程序模型检测和i o s t s ( i n p u t o u t p u ts y m b o l i ct r a n s i t i o ns y s t e m s ) 系统，先介绍 了论文中处理问题的关键手段程序模型检测，然后介绍了验证工作所针对的模型表示 1 0 s t s 系统。第三章i o c o 致性所存在的问题和系统安全性，提出了i o c o 一致性不能 够保持安全性，导致系统存在两类安全性缺陷无法通过i o c o 一致性纠正，并针对这两类安 全性缺陷定义了两类不安全的迹，提出了系统违背安全性的概念。第四章中使用对程序进 行模型检测的测试手段，找到了违背系统安全性的迹，并对模型和实现进行了相应的修改， 最终解决了问题，弥补了i o c o 一致性两种缺陷。第五章对本文进行总结并提出了进一步的 工作。 内蒙占大学硕七! 学位论文 第二章程序模型检测和lo s t s 系统 2 1 程序模型检测技术介绍 形式化方法对开发高可信软件具有重要的意义。模型检测( m o d e lc h e c k i n g ) 是近十几 年来最成功的自动验证技术之一，此技术的成功应用归功于有效验证工具的开发和支持。 模型检测的研究大致涵盖以下内容：模态时序逻辑、模型检测算法及其模型检测工具的 研制。 模型检测是一种强大的自动分析验证有限状态系统的技术，它将所需验证的系统及属 性作为模型检测工具的输入，检测系统所有可能的状态，验证这些状态是否满足用户需要 的性质，如果不满足，将会产生一个反例以便追踪并改正错误。它已经被成功的应用于计 算机硬件、通信协议、控制系统和安全认证协议等方面的分析和验证中，是有限状态验证 ( f i n i t es t a t ev e r i f i c a t i o n ) 的方法之一，另外还有两种分别是流方程( f l o we q u a t i o n s ) 和数据流分析( d a t af l o wa n a l y s i s ) ，迄今为止已开发出多种分析验证工具，如模型检测 的s m v 、s p i n 、流方程的i n c a ( i n t e g e rn e c e s s a r yc o n d i t i o n s ) 以及数据流分析的f l a v e r s ( f l o wa n a l y s i sf o rv e r i f i c a t i o no fs y s t e m s ) 等。 对程序进行模型检测的技术主要有两种：从源程序转化为模型检测工具的输入语言， 利用现有工具进行模型检测；或者是使用现有的编程语言的模型检测工具。论文中采用的 是第二种方法。 时态逻辑l t l 是由p u n e l i 在 p n u 8 1 羽中提出的。他是计算机科学领域中命题线性时 态逻辑最常用到的版本。时序逻辑是在普通的逻辑的基础之上增加了对于时序关系的描述。 使用时序逻辑的验证系统通常是基于状态的，但是基于行为的验证系统也可以使用它，尤 其是那些与进程代数相联系的验证系统对时序逻辑更是适用。时序逻辑的表达能力非常的 强。但是，用它们来书写的规格说明却往往有些含糊。 许多著名大学和研究机构，如i b m 公司、m i c r o s o f t 公司、b e l l 实验室、n a s a 研究中 心、b e r k e l e y 大学、s t a n f o r d 大学、c a r n e g i e - m e li o n 大学和k a n s a s 大学等都在该领域投 入大量资金和人力进行研究工作。其中就包括著名的j a v a 程序模型检测工具j a v a p a t h f i n d e r 和c 程序模型检测工具m a g i c 和c o p p e rn 钔m 2 m 3 m 引。 9 与测试相结合的系统安全性验证技术研究 3 2 2 相关工作介绍 2 2 1 程序模型检测的主要工具和方法 软件程序的模型检测研究主要有三种方法：基于程序语言转换的模型检查方法；基于 程序控制流提取的模型检查方法；基于程序动态执行信息提取的模型检查方法心副。 1 、基于程序语言转换的模型检查方法。 、 该方法是将软件程序转换为现有模型检查工具的输入语言，从而可利用这些模型检查 工具对软件程序进行性质验证。 j a v ap a t h f i n d e r 是n a s a 开发的并发j a v a 程序模型检查工具，可直接将一些j a v a 程 序转化为模型检查工具s p i n 的输入语言，从而实现对并发j a v a 程序的性质验证。特别是 j a v ap a t h f i n d e r 被用于分析著名的火星探路者航天器的控制软件旧5 1 ，成功的分析出了该控 制软件的一些关键错误。 b a n d e r a 是k a n s a s 大学开发的j a v a 程序模型检查工具，在j a v a 程序的切片技术与j a v a 士 ji - 1 d d v 丑i | 八士上上出山| v 上口i 一n悱眦i1 士一口1 矗r i 删tr 、i 州- 、 法仅仅适用于一些特殊的较简单的程序，这种转换过程自动化程度较低，需要进行大量的 人工干预。例如在 j a v a 并发程序的模型提取与模型检测技术研究n 町一文中就是通过实 现自己的工具j 2 s p i n 来帮助使得转换过程可以顺利进行。 2 基于程序控制流提取的模型检查方法是直接分析程序的源代码，构造扩展程序控制 流图( 或控制流自动机) ，利用程序分析技术和抽象技术，构造程序的抽象有限状态模型， 通过模型检查算法对该有限状态模型进行性质验证。一个程序的实际可执行路径必然是其 控制流图中所有路径的子集，控制流图上不存在的路径，就不可能是程序的实际执行路径。 建立程序控制流图涉及到程序的过程调用和并发控制，很难转化为k r i p k e 结构或自动机， 这就需要设计适合于程序特点的模型检查算法。 流分析以程序控制流图为分析对象，可视为对程序在抽象解释下进行的模型检查。流 l o 内蒙古人学硕十学位论文 分析作为一种经典的程序分析技术，丰要用于程序的编译优化，其理论框架是格论中的不 动点理论，而不动点理论是模型检查算法的理论基础。将流分析应用于程序的模型检查是 当前重要的研究方向。 f l a v e r s 构造程序的迹流图( 并发控制流图+ 事件标志) ，采用过程数据流分析技术验 证顺序或并发的a d a 程序或j a v a 程序是否具有基于事件的或基于行为的并发系统的性质。 f l a v e r s 验证的效率高，算法简明，但是由于采用嵌入方式描述程序过程调用，f l a v e r s 无 法分析递归程序，没有采用谓词抽象技术，验证精度不高心7 剀。 。 s l a m 是m i c r o s o f t 公司开发的对c 程序进行模型检查的工具，利用谓词抽象技术，首 次将实际的顺序c 程序转化为一个布尔程序，有效地解决了状态空间爆炸问题，利用过程 间流分析算法( 类似于数据流分析中的定义可达性分析算法) 进行模型检查。s l a m 已成功应 用于验证w i n d o w s 系列操作系统的驱动程序，并发现了一些长期未被发现的复杂错误。s l a m 的缺点是不能分析并发程序心引。 b l a s t 是u cb e r k e l e y 提出的模型检查工具，它像很多j a v a 程序模型检测工具一样作 为e c li p s e 的插件对j a v a 程序进行模型检测。它采用一种反例求精算法进行在线的谓词抽 象，提高谓词抽象的效率，并采用流分析算法进行模型检查。其优点是可以对规模很大的 程序进行模型检测( e g ：三万行的程序) ，有自己的图形界面系统，有e c l i p s e 的插件。其 缺点是它不能分析并发程序跚1 。 m a g i c 和c o p p e r 是c a r n e g i e - m e li o n 大学开发的模型检查工具，采用传统模型检查算 法对程序模型检查，研究对c 程序进行模型检查的方法，该工具支持c 语言的一些并发特 性，可验证互模拟性质，但不能直接分析递归程序，支持的数据类型也比较单一聆。 3 基于程序动态执行信息提取的模型检查方法是通过直接调度程序执行，利用程序动 态执行信息构造有限状态模型，采用模型检查算法验证性质。 c m c 是基于程序动态执行信息提取的模型检查工具，通过调度程序的执行，利用程序动 态执行的信息( 堆、栈和寄存器等等) ，构造状态变迁图进行性质验证，发表的实验结果表 明，c m c 能发现协议软件的许多复杂错误。该方法避免了处理程序复杂的数据结构和控制结 构，类似于软件测试，只能证明程序存在某种错误，而不能证明程序不存在某种错误口2 1 。 高可靠的软件系统往往需要保证某些特殊性质没有逻辑错误，而软件测试技术作为主 要的系统可靠性检验手段，只能说明软件存在某种错误而不能说明软件不存在某种错误。 模型检测是一种对有限状态变迁系统验证其时态逻辑性质的重要方法，由于模型检测过程 完全自动化，所以非常适合于验证复杂系统性质的要求，可以补充测试技术之不足。模型 与测试相结合的系统安全性验证技术研究 检测技术的限制在于需验证的系统必须是有限状态的，并且现有模型检测工具的算法主要 是针对k r i p k e 结构和6 0 自动机设计，软件程序由于其复杂的数据结构和控制结构，使得程 序模型检测成为一个极具挑战性的问题。近年来，随着计算技术的飞速发展和对高可靠性 软件的迫切需求，模型检测技术被直接用于丰流编程语言的程序性质验证“鲫