（计算机系统结构专业论文）无线安全协议测试方法研究与系统设计.pdf

摘要 迄今为止，协议测试领域所进行的工作主要集中在通信协议的一致性测试方 面。对通信协议的一致性测试已经有一套相对完整的自动化检测技术，但其理论 在具体实践中还存在很大差距。作为网络协议子类的无线安全协议，却没有一套 简单可行的测试方法。 因此，本文在分析无线安全协议特点的基础上，提出对其进行测试的重点应为 一致性和安全性。一致性测试主要检测所实现的安全协议是否符合协议规范，为 协议能够正常运行和抵御攻击提供基础保障，安全性测试主要检测所实现的安全 协议是否违反了安全性，进而判断其安全指标。 一致性测试方面，本文根据项目需求，提出了针对无线安全协议的一致性测 试流程。其中，改进的测试序列自动生成算法具有针对性、高效性、完备性等优 点。并提出了基于帧字段分析的方法来唯一确定符号集中的所有符号，从而达到 状态和迁移确认的目的。安全性测试方面，本文研究了传统与最新的研究方法， 分析它们的利弊。在协议工程学的层面上，对基于黑盒测试理论与自学习算法的 安全性测试流程进行扩展，给出了具有检测安全错误引入阶段的测试流程。为了 整合研究成果，本文设计了无线安全协议测试系统，该系统具有易用性、高效性、 可扩充性等优点。 关键词：无线安全协议一致性测试安全性测试测试系统 a b s t r a c t t h er e s e a r c ho fp r o t o c o l s t e s t i n g s t i l lf o c u so nt h ec o n f o n n a n c et e s t o f c o m m u n i c a t i o np r o t o c o l sn o w t h e r ei sar e l a t i v e l yc o m p l e t ea n da 吡t o m a t i cs u i t o f t e s t i n gt e c h n i q u eo nt h ec o n f o r m a n c et e s to fc o m m u n i c a t i o np r o t o c o l s ，b u tn l et h e o r y i ss t i l lf a ra w a yf r o mp r a c t i c a lu s e h o w e v e r , a sa s u b t y p eo fn e t w o r kp r o t o c o l s ，t h e w i r e l e s ss e c u r i t yp r o t o c o l sd on o th a v ea s i m p l ya n df e a s i b l et e s t i n gm e t h o dy e t t h e r e f o r e ，b ya n a l y z i n gt h ec h a r a c t e r i s t i c so ft h ew i r e l e s ss e c u r i t y t h ep a p e r m g a r d st h a tt h ek e yp o i n t so ft e s t i n gs h o u l db ec o n f o r m a n c et e s ta n d s e c u r i t yt e s t t h e c o n f o r m a n c et e s ti sm a i n l yc h e c kt h ec o n s i s t e n c yb e t w e e nt h e i m p l e m e n t a t i o na n dt 1 1 e s p e c i t i c a t i o n s ，e n s u n n gt h ec o r r e c tf u n c t i o n i n go ft h ei m p l e m e n t a t i o n w h i l et h e s e c u r i t yt e s ti sm a i n l yc h e c kw h e t h e rt h e r ei s a n ys e c u r i t yv i o l a t i o n ，e s t i m a t i n 2t h e s e c u r i t yp e r f o r m a n c e o nt h ec o n f o r m a n c e t e s t i n gp a r t ，ap r o c e d u r ea i ma tt e s t i n gt h ec o n s i s t e n c yo ft h e w i r e l e s s s e c u r i t yp r o t o c o l si sp u tf o r w a r dt om e e tt h ed e m a n do ft h ed r o j e c t t h e m o d i f i e da l g o r i t h mo f a u t o m a t i c a l l yp r o d u c i n gt e s ts e q u e n c e si sp e r t i n e n c e ，e 缅c i e n t a n dm a t u r e t oc o n f i r mt h es t a t e sa n dt r a n s i t i o n s ，am e t h o di s p r e s e n t e d 。w h i c hc a l l u n i q u e l yi d e n t i f ya l lt h es y m b o l si nt h ei n p u t o u t p u ts e tb a s e do nf i e l d sa n a l 、，z i n g o nt h es e c u r i t yt e s t i n gp a r t , c l a s s i c a la n dl a t e s tr e s e a r c hm e a n sa r ei n v e s t i g a t e d 、 t h e i rs t r o n ga n dw e a kp o i n t sa r ea l s os u m m a r i z e d a n dt h ep r o c e d u r eo fs e 谢t v t e s t i n gb a s e do nb l a c k - b o xc h e c k i n gt h e o r ya n dl e a r n i n g a l g o r i t h mi se x t e n d e dt o d e t e c tw h i c h p e r i o db r i n g si ns e c u r i t yf l a w sd u r i n gt h ep r o t o c o l se n g i n e e r i n g f i n a l l y a t e s t i n gs y s t e mw h i c hi se a s yt ou s e ，e f f i c i e n ta n de x t e n s i b l ei sd e s i g n e dt oi n t e 毋a t ea l l t h er e s e a r c ha c c o m p l i s h m e n t k e y w o r d ：w i r e l e s ss e c u r i t yp r o t o c o l s c o n f o r m a n c et e s t s e c u r i t yt e s t t e s t i n gs y s t e m 西安电子科技大学 学位论文创新性声明 秉承学校严谨的学风和优良的科学道德，本人声明所呈交的论文是我个人在 导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标 注和致谢中所罗列的内容以外，论文中不包含其他人已经发表或撰写过的研究成 果；也不包含为获得西安电子科技大学或其它教育机构的学位或证书而使用过的 材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说 明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切的法律责任。 本人签名：日期垒丝：兰：仝 西安电子科技大学 关于论文使用授权的说明 本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究 生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。学校有权保 留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分内 容，可以允许采用影印、缩印或其它复制手段保存论文。同时本人保证，毕业后 结合学位论文研究课题再撰写的文章一律署名单位为西安电子科技大学。 ( 保密的论文在解密后遵守此规定) 本学位论文属于保密，在一年解密后适用本授权书。 本人签名：瑾羞壬日期垫兰：圣：2 导师签名：e l 期麴墨：兰：皇 第一章绪论 第一章绪论 1 1引言 在计算机网络的发展历程中，协议一直处于核心地位，它是计算机网络和分 布式系统中通信实体之间相互交换信息所必须遵守的一组规则。 协议软件作为软件的一种特殊形式，自2 0 世纪8 0 年代以来，其开发和检测 方法已经得到了快速的发展，并形成了一个崭新的学科协议工程学，它的研 究范围包括：协议规范( p r o t o c o ls p e c i f i c a t i o n ) 、协议证实( p r o t o c o lv a l i d a t i o n ) 、协 议验证( p r o t o c o lv e r i f i c a t i o n ) 、协议综合( p r o t o c o ls y n t h e s i s ) 、协议转换( p r o t o c o l c o n v e r s i o n ) 、协议性能分析( p r o t o c o la n a l y s i s ) 、协议自动实现( p r o t o c o la u t o m a t i c i m p l e m e n t a t i o n ) 和协议测试( p r o t o c o lt e s t i n g ) 。 目前的协议多是以自然语言描述的文本。实现者对于协议文本的不同理解和 可选的协议属性以及实现过程中的非形式化因素都会导致不同的协议实现，有时 甚至是错误的协议实现。何况有些没有进行完备详尽描述的协议，最容易出现不 同协议实现之间的不兼容情况。即便不同的实现各自都符合协议标准，也不能保 证它们彼此之间能够准确无误地通信。同一协议的不同实现还存在着性能差别。 对于目前的数据通信领域中，通信协议日趋复杂，数据通讯涉及到越来越多的设 备供应商和服务提供商。在这种情况下，需要一种有效的方法对协议实现进行评 价，这就是“协议测试”。 协议测试是在软件测试的基础上发展起来的。根据对被测软件的控制观察方 式，软件测试方法【1 】分为三种：白盒测试、黑盒测试和灰盒测试。协议测试是一种 黑盒测试，它按照协议标准，通过控制观察被测协议实现的外部行为对其进行评 价。 1 2研究现状 1 2 1 一致性测试研究现状 协议测试已经不仅仅是产品开发研制过程中一个简单的检测支持过程，而是发 展成为计算机网络技术的一个重要分支和协议工程学的一个重要组成部分。对协 议测试技术的研究将直接影响到计算机网络技术的进步和世界网络市场的竞争与 2 无线安全协议测试方法研究与系统设计 发展。所以很多国家都投入了大量的人力物力从事协议测试的研究工作。例如： 英国的国家物理实验室n p l ，法国国家通信研究中心、德国国家通信研究局g m d 、 美国国家标准化研究局、美国新罕布什尔大学互操作研究实验室、清华大学计算 机科学与技术系的网络和协议测试实验室和中科院计算所的网络测试实验室等单 位都在这个领域投入了大量的研究力量。 目前，协议测试研究领域已经取得了以下两点共识： 第一，理顺了协议一致性测试的过程； 第二，将形式化技术引入了协议测试领域，力图用严格的数学语言清晰、无二 义性地研究协议测试的概念和方法。 但是，同时也发现这种方法存在着很多不足，其中最明显的就是这些理论研究 与实际应用之间还存在着巨大的差距【2 j 。 1 2 2 安全性测试研究现状 随着网络环境的日益恶化和人们安全意识的不断提高，测试网络协议的安全性 成为一个相对较新的研究课题。相对于一致性测试，安全性测试并没有可供参考 的国际标准。一些早期的测试工作【2 4 】【33 1 ，使用人工观察的方法，针对特定的漏洞 生成测试案例来测试协议的安全性。虽然这些启发式的方法对部分的有限的协议 和属性有效，但并不能系统地全面地识别所有协议实现的安全错误。文献【3 4 j 研究 了协议实现的安全错误，使其在特定的执行环境下能曝露出来，并提出一种变异 方法来检测之。文献【2 4 】提出了被动监听和主动检测的方法来测试安全协议的消息 机密性。 传统的一致性测试并不能检测到超出协议规范的行为，而且由于未知协议实现 模型的复杂度，使得传统的协议校验和一致性测试的大量研究成果并没有直接应 用到安全性测试方面。因此，文献【27 】提出了一种自学习的主动测试方法，系统地 并自动地检测协议实现的安全属性。该测试方法应用了黑盒测试1 a c k - b o x ) 理论【2 0 】 和监督学习( s u p c r v i s e al e a r n i n g ) 算法【2 1 1 ，模拟了能产生一致性测试序列的导师，从 而探测待测协议实现的结构，再进一步检测协议实现的消息安全性。 1 3研究目的和方案 本课题来源于“十一五”通信装备预先研究项目网络动态安全防护技术 抗无线网络攻击技术，需要设计并实现新的无线安全协议，为了检测实现的新的 无线安全协议是否符合规范标准、安全性能是否达到要求，需要对无线安全协议 的设计及实现进行严格的测试。 第一章绪论 3 如上1 2 节所述，虽然通信协议的一致性测试已经有一套可供参考的自动化测 试标准，但与实际应用还存在相当大的差距。而且由于无线安全协议自身的特点， 安全性与一致性具有同等的重要性。 本文根据项目的需求，首先探索了如何实现针对无线安全协议的一致性测试， 解决了许多实现上的细节问题。在研究的过程中，首先使用形式化的方法对协议 规范、协议实现进行建模，给出一致性的判定条件。然后，对8 0 2 1 1 b 协议的客户 端实现进行完整的一致性测试，得出可供参考的测试流程，改进了测试序列的自 动生成算法，并解决了状态确认问题。 在安全性测试中，本文介绍了传统的和当前的研究方法，对于传统的基于测试 库的检测思想，总结了协议运行平台的漏洞；对于当前的研究思路，介绍了一种 新的测试体系与涉及的算法，给出分析与改进方案，提出与之前的研究结果整合 的构想。 最后，本文设计了安全协议测试系统，整合了之前研究的成果。 1 4 研究内容和论文结构 第一章： 介绍了协议测试的重要性、研究现状和课题背景，根据项目的需求，阐述了 研究的目的和使用的方案。 第二章： 在分析无线安全协议特点的基础上，提出了具有针对性的测试框架。介绍了 不同的测试方法并分析其利弊。最后给出了测试的流程示意图，总体上给读者一 个认识。 第三章： 介绍了有限状态机模型的基本概念和一些扩展模型，接着介绍了基于有限状态 机模型的主动测试的四种基本测试方法，最后介绍了被动测试的错误检测算法思 想。 第四章： 对8 0 2 1 1 b 协议进行了一致性测试的具体实践。首先对一般协议进行了形式化 建模，给出了一致性的判定原理，接着针对无线认证过程，提出了改进的测试序 列自动生成算法，对该算法进行了描述和分析，给出了实验结果。针对原始算法 状态检测能力不足的问题，给出了基于帧字段分析的状态确认方法。 第五章： 介绍了传统的与当前的安全性测试研究思路与测试方法。对于基于测试库的 传统思想，总结归纳了基于8 0 2 1 1 体系的漏洞，根据这些漏洞可以生成测试脚本。 4 无线安全协议测试方法研究与系统设计 对于自学习的测试方法，详细分析了其流程并对其中的不足提出了改进方案。最 后，分析了传统与当前研究方法的利弊。 第六章： 集成之前的研究成果，整合成一个系统，给出了系统的构架，具体模块的设 计，涉及的关键技术，进行了实验测试。 第七章： 对本文的工作进行小结，分析其优缺点，并提出今后努力的方向。 第二章无线安全协议测试框架 第二章无线安全协议测试框架 2 1无线安全协议测试框架 迄今为止，协议测试领域所进行的工作主要集中在路由协议方面。针对路由协 议的协议测试有三种：一致性测试、互操作性测试和性能测试。一致性测试是基 础，它是通过观察具体实现在不同的环境和条件下的反应行为来验证协议实现与 相应的协议标准是否一致的；要保证不同的协议实现在实际网络中能成功的通讯， 还需要检测某一协议实现与其它系统之间的交互过程是否正常，这就是互操作性 测试；另外还要对协议的性能进行测试，如健壮性、吞吐量等。 无线安全协议作为网络协议的一个子类，与路由协议工作的协议层次不同。在 不考虑物理层的情况下，路由协议工作在口层，需要数据链路层提供的服务才能完 成任务，因此有协议层间的交互。而无线协议仅工作在数据链路层，没有协议层 间的交互。不同路由协议之间不可避免地要进行交互，安全协议作为相对独立的 消息交换协议，一般不与其他协议交互。因此，互操作性测试在安全协议中可以 简化。路由协议交换的是关于网络拓扑结构的信息，需要及时更新，其信息量远 远大于安全协议通信实体间的消息交换量，因此，性能测试对路由协议的测试是 必不可少的，而对安全协议则是可以通过仿真等其他形式完成。但是，安全协议 通过密码技术实现通信中的身份认证和密钥分发与管理，从而保证网络通信的安 全性，对其安全性能的测试是必需并具有积极意义的。 6 无线安全协议测试方法研究与系统设计 2 2测试方法 按照测试系统是否与待测实体有交互信息，在测试方法上可以分为主动测试和 被动测试【3 】。主动测试是由测试者主动执行己设计好的一些测试序列，通过观察待 测实体的输出是否和预期的输出一致来判定待测协议实现( i m p l e m e n t a t i o nu n d e r t e s t ，i u t ) 是否存在错误。被动测试不向通信实体发送任何报文，而只是“被动” 地监听通信实体之间的输入输出行为，通过分析监听到的数据，来推断协议实现 中是否存在错误。 2 2 1 主动测试方法 主动测试最核心的一个问题是测试序列的生成方法。测试序列来源于协议标准 所应实现的功能，所以它可以从协议规范中推导出来。由于协议本身可以抽象成 数据描述以及作用在这些数据上的行为描述，因此协议一致性测试可以分为对控 制流的测试以及对数据流的测试。 控制流的测试相对容易一点，测试技术相对成熟一些，目前常用的控制流的测 试序列生成方法都是基于有限状态机( f i n i t es t a t em a c h i n e ，f s m ) 模型【4 】，主要有： 转换回路( t r a n s i t i o nt o u r ，简称t ) 方法【5 】，可区分序y l j ( d i s t i n g u i s h i n gs e q u e n c e s ，简 称d 或d s ) 方法【6 】，唯一输入输出序y u ( u n i q u ei n p u t o u t p u ts e q u e n c e s ，简称u 或u i o ) 方法【7 】和特征集合( c h a r a c t e r i z i n gs e t ，简称w ) 方法【8 1 。在3 2 节会有这些方法更详 细的介绍。 现有的数据流的测试都可以归结为：分割测试和定义一使用。分割测试是通过 某种分割式，将输入空间划分成若干子域，然后通过测试假设从子域中选取一些 元素进行测试。 2 2 2 被动测试方法 被动测试通过监听来采集数据，通过分析数据来发现协议实现中存在的错误， 它不影响网络系统的正常工作，特别适用于发现正在运行的网络上的潜在错误。 和主动测试相比较，被动测试并不需要考虑如何生成测试序列，但需要设计检测 错误的算法。文献 9 】中在f s m 模型上给出了一个基于逻辑推理的错误检测算法，并 将其推广到了非确定有限状态机( n o n d e t e r m i n i s t i cf i n i t es t a t em a c h i n e ：n f s m ) 上。 第二章无线安全协议测试框架 7 2 2 3 测试方法比较 被动测试方法和主动测试方法的区别在于：主动测试需要自己设计测试例，而 被动测试则不用。主动测试是一种非常有效的测试手段，但由于测试程序要与t 直接通信，因此做主动测试时m t 一般要与网络分离，而且目前协议越来越复杂， 用主动测试的话，在测试程序编写和测试序列构造等方面面临着很大的困难。被 动测试比较简单，不需要构造测试集，支持在线测试，且可以长时间进行测试而 无需人工干预。尽管被动测试具有上述优点，但由于它不控制测试过程，所以不 能保证测试的完备性。 主动测试方法只能用来发现错误而并不能保证协议实现是没错的，也就是说即 使协议实现通过了主动测试，在实际运行中还是可能会出错，因此被动测试成为 必然的选择。主动测试和被动测试被用来测试协议时各有利弊，如果能将二者结 合起来，使其优势互补，可以取得更好的测试效果，因此本文提出了将被动测试 和主动测试相结合的思想，将被动测试作为主动测试的补充，对待测实体进行全 面测试，提高整个测试的效率和质量。 2 3 一致性测试结构 本部分先介绍o s i 国际标准的一致性测试的框架和方法，再根据2 1 节中归纳的 无线安全协议的特点，阐述本文提出的针对无线安全协议的一致性测试结构和方 法。 2 3 1 一致性测试框架和方法 协议一致性测试是协议工程学的一个重要分支，其目的是通过实验的方法发现 待测协议实体在功能和逻辑方面的错误。研究协议一致性测试的原因在于协议标 准通常都是比较复杂的，实现者对其不同的理解会导致不同的协议实现，有时甚 至会是错误的实现，因此要一种有效的方法来对协议实现进行验证和判别，对于 测试人员而言，其内部的逻辑结构是不可知的，但是测试人员可以控制外界对被 测协议实现的输入、也可以观察被测协议实现的输出，因此协议一致性测试是采 用黑盒测试的方式进行。i s o i e c9 6 4 6 定义了一个国际标准o s i 的一致性测试 的方法和框架【l0 1 ，用于测试实现了某一o s i 协议的产品与其协议标准的一致性。 图2 2 为协议一致性测试的基本结构，其中t 为待测协议实体，它通过观察控 制点p c o ( p o i n t so f c o n t r o la n do b s e r v a t i o n ) 与外部环境交互，u t ( u p p e r t e s t e r ) 为上 层测试体，通过在p c o 上调用i u t 提供的抽象服务原语( a b s t r a c t s e r v i c ep r i m i t i v e s ： 无线安全协议测试方法研究与系统设计 a s p ) 检测r l j t 的行为，l t ( l o w e r t e s t e r ) 为下层测试体，它通过p c o 并经由n 1 层服 务提供者( s e r v i c e pr o v i d e r ) 发送n 一1 层a s p 给i u t ，以支持i u t 的行动，u t 和l t 通常 是一个完整的测试系统或者是一个测试系统的一部分。在a s p 中可能承载协议数据 单元( p r o t o c o ld a t au n i t ：p d u ) 。在测试期间l t 和u t 通过测试协调过程( t e s t c o o r d i n a t i o np r o c e d u r e s ：t c p ) 相互通讯。 图2 2o s i 一致性测试框架 一致性测试通过观察待测协议实体的输出来判定其是否按照协议标准正确实 现了某项功能，按照协议标准，能够验证某项功能的输出只能在输入满足一定的 条件时才能出现。一致性测试正是通过测试系统和被测系统之间的通信来实现的。 测试协议实现的某项功能，可以分两个阶段进行： ( 1 ) 测试系统向被测系统发送一系列的数据，这称为一致性测试的控制阶段。 ( 2 ) 测试系统监控被测系统返回的数据，与预期的返回数据进行比较，并做出 判定，这是一致性测试的观察阶段。 2 3 2 无线安全协议的一致性测试结构 由2 1 节对无线安全协议的特点分析，可知无线安全协议相对独立，在运作过 程中并不需要下层或上层提供服务，因此，其一致性测试框架可简化为图2 3 。 测试系统 篓兰! ! 堕! 篓至塑：! - _ j ：砌剃试f 智毪下c ) 待测协议 图2 3 无线安全协议一致性测试框架 在具体实现中，无线安全协议的一致性测试，分为认证交互测试与数据交互 测试。认证交互测试主要检测协议实现的客户端与服务器端在接入认证过程中的 第二章无线安全协议测试框架 9 身份确认程序是否符合协议规定，该过程属于对控制流的测试。数据交互测试主 要检测接入成功之后，通信方数据交换过程中发现错误，纠正错误的能力，该过 程属于对数据流的测试。对待测协议进行控制流测试或数据流测试，可以根据需 求采用主动测试或被动测试的方法。 对待测实体进行认证交互测试，为了达到测试的完备性和测试过程的可控性， 可以采用主动测试的方法，首先使用有限状态机模型对安全协议进行形式化描述， 生成协议中所有通信实体的状态转换图，然后根据状态转换图生成测试序列，即 测试集的构造；接着使用这些测试序列进行测试，即测试集的执行；最后，对测 试结果进行评估，给出待测实体一致性分析的结果。或者采用被动测试的思想， 监听通信实体间的消息交换，分析后判定其一致性。其流程如图2 4 所示。 图2 4 认证交互测试流程 对待测实体进行数据交互测试。考虑数据流量较大，可以采用被动测试的方 法，首先对数据流( 通信使用的所有数据帧) 进行筛选分类，得到需要进行测试 的关键数据帧，然后把数据帧中的域分为三种类型的字段：重要且必须的字段、 重要但可选的字段、不重要但必须的字段。接着设计针对关键数据帧的数据帧序 列( 测试集) ，并向待测实体发送，扑获待测实体回应的关键数据帧，作匹配分析 来判断是否存在错误。其流程如图2 5 所示。 图2 5 数据交互测试流程 1 0 无线安全协议测试方法研究与系统设计 2 4安全性测试结构 对于安全性测试，国际上并没有统一的国际标准。 本文在对安全协议的分析研究基础上，根据传统的测试方法，把无线安全协 议的安全性测试，分为平台安全测试与认证安全测试。平台安全测试主要检测协 议实现抵御干扰或破坏正常通信攻击的能力，如缓冲区溢出、拒绝服务等攻击。 认证安全测试主要检测安全协议认证与密钥协商过程是否存在安全威胁或漏洞。 对安全协议进行平台安全测试，首先根据安全协议普遍运行的载体如8 0 2 1 1 体系 i ，本身存在的不足与漏洞，设计针对该运行体系的攻击测试集，然后对协 议载体进行攻击测试，评价具体协议实现的平台安全。 对安全协议进行认证安全测试，首先根据特定安全协议认证过程或密钥协商中 存在的漏洞，设计针对特定协议的攻击方案，并形成攻击测试集( 测试脚本) ，接 着对运行的协议进行攻击，评价其抵抗攻击的能力。 第三章一致性测试的一般理论 第三章一致性测试的一般理论 协议的形式化方法，目前己经研究并开发出多种形式的模型，主要有以下几 种：有限状态机( f i n i t es t a t em a c h i n e ) 、p e t r i 网( p e t r in e t ) 、时序逻辑( t e m p o r a l l o g i c ) 、通信系统演算( c a l c u l a t i o n so fc o m m u n i c a t i o ns y s t e m ) 、形式文法( f o r m a l g r a m m a r ) 、过程语言( p r o c e d u r a ll a n g u a g e ) 等数学模型和逻辑模型。在广泛使用于 协议实现的形式化规范的方法中，主要有标号迁移系统l t s ( l a b e l l e dt r a n s i t i o n s y s t e m s ) ，和有限状态机f s m ( f i n i t es t a t em a c h i n e ) 。 3 1f s m 的基本概念及其扩展模型 有限状态机模型在协议工程中是最重要的一个模型，本节给出f s m 的定义，错 误模型及f s m 的一些扩展模型的介绍。 3 1 1 基本的f s m 模型 定义3 1 有限状态机( f i n i t es t a t em a c h i n e ：f s m ) 一个有限状态机是一个六元组：m = ( ，o ，s ，s o ，万，旯) ，其中，是输入符号集， d 是输出符号集，s 是状态符集，、d 、s 均为非空集合；s 。是初始状态； 艿：s x io s 是状态转移函数；a ：s 1 一o 是输出函数。f s m 对于每一个状态迁 移，一个输入对应一个或者几个( 也包括零个) 不同的输出。 状态转移函数万和输出函数允共同定义了状态的转换集合t ( 因此，有限状态 机也可以看作是一个五元组m = ( ，o ，s ，t ) ) 。t 中的每个元素可以表示为一个 三元组t - - ，其中s i s 称为转换t 的头状态，f 1 和o = , z ( s i ，f ) 0 分 别称为转换t 的输入和输出，s ，= a ( s ，f ) s 称为转换t 的末状态。我们用 马丝一5 ，表示有限状态机m 处于状态蜀时接受输入f 使状态转移到s ，并且产生 输出o 。 当使用有限状态机模型描述一个协议规范时，状态是协议实体能停留的稳定条 件，输入是协议实体从外界接收到的报文激励或者内部产生的事件激励，输出是 协议实体对外界的响应。 定义3 2 等价状态 令m 是一个有限状态机m = ( 7 0 ，s ，s 。，6 ，a ) ，如果存在状态s i s ，s ，s ，使 得这两个状态对于任意的输入序列都产生相同的输出序列，则称状态s ，和s ，等价。 1 2 无线安全协议测试方法研究与系统设计 定义3 3 完全定义的状态机 令膨是一个有限状态机m = ( 7 ，o ，s ，万，旯) ，如果对任意状态i s 和任意的 输入f i ，都存在转换t = ，则称状态机m 是完全定义的状态机，反之 则称m 是非完全定义的状态机。 一般协议实体对应的状态机都是非完全定义的状态机，但我们可以通过添加头 状态和尾状态相同，且输出为空的自循环转换来将非完全定义的状态机补齐为完 全定义的状态机，一般将这种添加的自循环转换称为非核心转换，其他的称为核 心转换。 定义3 4 最小化的状态机 令m 是一个有限状态机m = ( ，0 ，s ，s 。，万，五) ，如果m 中不存在等价的状态， 则称状态机膨是最小化的状态机。 定义3 5 路径 令m 是一个有限状态机m = ( ，0 ，s ，艿，兄) ，对状态s i s ，s ，s ，如果存在 转换序列t it 2 ，f 。，使得 ( 1 ) s ，为转换t ，的头状态； ( 2 ) 对于2 k 咒，转换t 。的头状态是转换t 的尾状态； ( 3 ) s ，为转换f 。的尾状态； 则称转换序列，乞，t 。，是一条从s ，到s ，的路径。 定义3 6 强连通有限状态机 令m 是一个有限状态机m = ( ，o ，s ，s o ，艿，旯) ，对任意状态曼s ，s ，s ，如果 均存在从s ，到s ，的路径，则称m 是一个强连通的有限状态机。 一般将有限状态蝴一个图c ( v ，e ) 来表示，图的顶点集合v 代表状态机m 的状态集，图中的边集合代表m 的转换集合，边上的标号是对应转换的输入输出。 图3 1 给出了一个例子，该状态机是一个最小化的完全定义的状态机。 图3 i 最小化的完全定义的状态机 定义3 7 非确定有限状态机( n o n d e t e r m i n i s t i cf i n i t es t a t em a c h i n e ：n f s m ) 令m 是一个有限状态机m = ( ，0 ，s ，s 。，万，旯) ，如果存在状态s s 和输入f i ， 使得转换集合中存在两个或者以上的转换的头状态均为s ，输入均为f ，形式化表 第三章一致性测试的一般理论 示为，s s ，i ，使得( i 万( 5 ，o l - - 2 ) v ( 陋( s ，z ) l 2 ) 则称m 为非确定的状态机，反 之膨为确定的状态机。 可以将一个非确定的状态机转换为一个确定的状态机 8 4 ，所以本文中如未特 别指明，一般的状态机都指的是确定的状态机。 3 1 2f s m 的一些扩展模型 定义3 8 通信有限状态机( c o m m u n i c a t i n gf i n i t es t a t em a c h i n e ：c f s m l 一个通信有限状态机是由状态机集合膨和通信通道集合c 组成的， n = ( m ，c ) ，其中： ( 1 ) m = m ，m 2 ，m 。) 是有限个数的有限状态机集合； ( 2 ) c = c f ，：f ，n f t f 办是有限个数的通道集合； ( 3 ) 对每一个0 c 代表一个从所，到m ，的通信通道，其行为类似于一个先进先 出( f if o ) 的队列，m ，从队列头部取消息作为输入而m ，则将产生的消息放在队列 的尾部。 如上定义的c f s m 模型能够很好的描述实际协议当中的交互行为，可以将集合 m 理解成参与协议交互行为的实体集合，通道集合c 则是由实体之间交互的网络 连接通道组成。 基本f s m 只反映了协议事件和协议状态之间的关系，它们不能表述其他重要的 协议元素：协议变量和协议行为。扩展有限状态机e f s m 力图弥补这个不足。下 面对e f s m 的基本概念进行介绍。 定义3 9 扩展有限状态机( e x t e n d e df i n i t es t a t em a c h i n e ：e f s m ) 一个扩展有限状态机m 是一个八元组m = ( ，0 ，s ，t ，s 。，v ，p ，a ) ，其中： ( 1 ) s 表示状态的集合，s 。s 表示初始状态； ( 2 ) 丁表示转换的集合； ( 3 ) y 表示环境变量的集合； ( 4 ) p 表示作用于环境变量和输入输出参数的谓词的集合； ( 5 ) a 表示作用于环境变量和输入输出参数的行为的集合。 在状态s ，下，对环境变量y 中所有变量的一个赋值，称为状态s ，的一个环境配 置，记为s i ( 矿) 。转换集合r 的每个元素是一个五元组t = ，其中 8 i s 称为转换t 的头状态，f 1 和0 0 分别称为转换的输入和输出，s ，s 称为 转换的尾状态，p 表示执行转换t 时必须满足的条件，a 表示执行转换f 时的动作， 只有转换条件p 为真值的情况下，转换t 才可以执行。 当使用扩展有限状态机模型描述一个协议规范时，状态是协议实体能够停留的 稳定条件；输入是协议实体接收到的外界激励或者内部产生的事件激励( 可能包 1 4 无线安全协议测试方法研究与系统设计 含一些输入参数) ；输出是协议实体对外界的响应( 可能包含一些输出参数) ；转 换执行条件是关于输入参数和当前环境变量的条件表达式；转换执行动作包含对 输出参数的设置，以及对环境变量的改变。转换t = 表示当协议实 体处于状态s 时，接收到外界输入激励或者内部事件f ，如果在当前的环境配置 s ，( y ) 下条件p 能够满足，则执行动作a 来修改环境变量，设置输出参数，对外界 产生响应o ( 包含输出参数) 并进入状态s ，。对于转换t = 和状态的 一个环境配置s ，( y ) ，如果存在输入f 满足条件p ，则称转换t 在该环境配置s ，( 矿) 下 可执行。 定义3 1 0 可执行路径 假设m 是一个扩展有限状态机，如果存在转换序列t it 2 ，t 。，使得： ( 1 ) 假定量为转换t 。的头状态，则转换在某个环境配置s ，( 矿) 下可执行； ( 2 ) 对于2 k n ，转换t 。的头状态是转换气一，的尾状态，并且转换气在执行完 转换t 后的环境配置s ，( y ) 下是可执行的； 则称转换序列，f ：，t 。是一条可执行路径。 定义3 1 1 事件驱动的扩展有限状态机( e v e n t d r i v e ne x t e n d e df i n i t es t a t e m a c h i n e ：e e f s m ) 一个事件驱动的扩展有限状态机m 是一个五元组m = ( s ，s 。，工，t ) ，其中： ( 1 ) s = ，s l ，s 川) 是状态集合，s o s 是初始状态； ( 2 ) 是事件集合，对任意事件e ( y ) ，p 代表事件名称，y = ( y l ，y ：，y 。) 是 事件的参数向量； ( 3 ) x 是一系列内部变量组成的向量； ( 4 ) 丁是转换集合，其中的任意元素是一个五元组 t = ，其中s 称为转换r 的头状态，sv 称为转换t 的尾状态， p ( x 。，歹) 是作用在输入参数向量y 和内部变量向量x 上的转换条件，而a ( x ，y ) 则是 一系列的赋值操作，根据x 和y 的当前值来更新向量x 。 该模型将通常的e f s m 模型中的输入、输出事件统一起来用事件来表示，表达 更清晰。 3 1 3f s m 的错误模型 对于状态机模型而言，一致性测试就是比较协议规范确定的有限状态机 m = ( j ，o ，s ，s o ，万，旯) ，是否和待测实体实现的状态机m = ( ，o ，s ，s o ，万，a ) 一 致，其中由于理论上m 个数是无穷的，所以为保证测试的顺利进行，有必要对m 的错误建模以限定测试范围。 首先假设m 和膨都是最简的有限状态机，由定义3 1 知，一个有限状态机主 第三章一致性测试的一般理论 要由三个集合、两个函数构成，因此其错误类型也与这五部分相关。具体有下面 几类错误。 ( 1 ) 集合s 、，、d 中元素个数的错误，包括个数的增加和减少 对于m 来说，在这种类型的错误中，最可能发生的错误是s 集合元素的增加 或减少，这主要是因为对协议规范的理解不同造成的。理论上陋| 的取值范围可以 是【o ，o o ) ，但显然这样的取值使测试无法进行，因为无论怎样测试都有更大的陋t f 使 得一些状态没有被测试到。因此在建立错误模型时通常对i 刮设置一个上限聊，即 0 l s l m ，而且由于初始状态的特殊性，一般都假定待测实体中一定正确的实现 了初始状态，亦即s 。= s ：。由于通常不会发生输入输出集合的错误，所以下面的讨 论都假设i = i 和d = d 。 ( 2 ) 关于转移函数的错误尾状态错 对于给定的两个状态s 和s ，其中s sns ，以及一个输入f i ，如果 8 ( s ，f ) = s 但万( s ，f ) s ，则m 中存在一个尾状态错误。在实际测试中，尾状态错 误可能并不能即时的反应在这个转移对应的输出中。 ( 3 ) 关于输出函数的错误尾状态错 对于给定的状态j ，其中s sns ，以及一个输入f i 和一个输出o o ，如 果a ( s ，f ) = o 但允( s ，f ) o ，则中存在一个输出错误。该错误在实际测试中是可以被 即时检测到的。 ( 4 ) 关于输入的错误 对于完全定义的有限状态机而言，这种类型的错误可以转化成输出错、尾状态 错或者二者的结合，因此一般都不予考虑。 ( 5 ) 转移条件错误 该错误仅在扩展有限状态机中才有，实现中的转换条件布尔表达式和描述不一 致。 ( 6 ) 转移动作错误 该错误也仅在扩展有限状态机中才有，实现中的转换动作序列和描述不一致。 3 2基于f s m 的协议主动测试方法 实施协议一致性测试时，测试系统向i u t 施加输入事件序列，接收校验输出事 件序列，检查状态转换，根据输出事件和状态的转移，判定砌t 的行为是否符合协 议规范的描述，这种测试方法称为主动测试方法，其中的输入、输出事件序列叫 做测试序列。测试序列说明i u t 所应该表现的逻辑行为，因此它可以从协议模型中 推导出来。目前，大部分协议测试序列的生成算法是基于f s m 模型的。主动测试 方法中最主要的工作就是生成测试序列，下面针对基于有限状态机的测试序列生 1 6 无线安全协议测试方法研究与系统设计 成方法进行介绍。 3 2 1t 方法 在一个有限状态机中，最直观的一种测试方法就是从初始状态出发，将其中所 有的转换至少遍历一次，最终回到初始状态。这样的一次遍历，就是有限状态机 的一个回路。转换回路方法一种最简单的实现是将随机的输入激励作用在有限状 态机上( 无错的情况下) ，直至所有的转换都被遍历至少一次为止。但是这样生成 的测试序列可能包含很多重复冗余的转换。另一种实现是借助于中国邮递员回路【1 2 】 的求解，求解转换回路就是在对应有限状态机的有向图中求解一类特殊的中国邮 递员回路( 即，每条转换至少出现一次) 。 转换回路方法相对于其他基于有限状态机的测试序列生成方法具有简单、生成 测试序列长度短( 使用中国邮递员回路问题求解) 的优点，并且这种方法仅要求 有限状态机是强连通的，而不必完全定义。但是，这种方法在测试过程中只检查 了转换的输出情况，没有对转换到达的状态进行检查，因而错误检测能力较低。 3 2 2 基于特征序列的方法 目前一致性测试方法都是在