（计算机软件与理论专业论文）基于uml安全协议的建模和自动检测.pdf

华南师范大学硕士学位论文答辩合格证明 学位申请人型互搔向本学位论文答辩委员会提交 题为盘型盟立垒堕墼垡啦鱼堑趔9的硕士论文， 经答辩委员会审议，本论文答辩合格，特此证明。 学位论文答辩委员会委员( 签名) 揣起趁 论文指导老师( 签名) ： 伽多彩日 华南师范大学硕士学位论文 f ：5 3 1 8 基于u m l 安全协议的建模和自动检测 摘要 网络安全是目前人们关注的一个热点，而安全协议的安全性却是网络安全的 关键。安全协议应用于网络上传送文件和进行各种交易以及对计算机系统的访问 等。人们已通过不同的方法证明一些已存在的安全协议并不如它们所声明的那样 安全。对安全协议的安全性进行验证成为国内外研究的热点。 本文主要研究安全协议的可视化建模，以及自动检测。论文首先介绍了安全 协议，接着介绍安全协议的形式化方法和自动检测方法，并着重介绍模型检测工 具s p i n 的原理和它的建模语言p r o m e l a 。接着提出了安全协议的u m l 建模规则和 过程，并讨论了安全协议的u m l 模型转化成p r o m e l a 语言的过程以及如何自动产 生攻击者模型。为了实现安全协议的可视化设计与自动验证，开发了自动转化工 具来实现这一日标。 关键词：安全协议，s p i n 。模型检测，u m l 。 第1 页麸7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检测 a b s t r a c t t h en e t w o r k s e c u r i t yi s af o c u sw h i c h p e o p l ep a yc l o s ea t t e n t i o nt o a tp r e s e n t ，a n dt h es a f e t yo fs e c u r i t yp r o t o c o li st h ek e yt ot h en e t w o r k s e c u r i t y t h es e c u r i t yp r o t o c o la p p l i e s t o c o n v e y i n gt h ef i l e ，c a r r y i n go n v a r i o u sk i n d so ft r a d ei nt h en e t w o r ka n d v i s i t i n gt oc o m p u t e rs y s t e me t c p e o p l eh a v ea l r e a d yp r o v e dt h a ts o m es e c u r i t yp r o t o c o l sa r en o ta ss a f ea s t h e yh a v eb e e nd e c l a r e dt h r o u g hd i f f e r e n tm e t h o d s s ov e r i f y i n gs a f eo f s e c u r i t yp r o t o c o lb e c o m e s t h e h o t s p o t t h em a i nt a s ko ft h et h e s i si st oi n v e s t i g a t et h ev i s u a lm o d e l i n ga n d a u t o m a t i c a l l yv e r i f y i n g o f s e c u r i t yp r o t o c 0 1 t h ep a p e r i n t r o d u c e st h e s e c u r i t yp r o t o c o l a t f i r s t ，a n d i n t r o d u c e st h ef o r m a l i z e dm e t h o d ea n d a u t o m a t i c a l l yv e r i f y i n g o f s e c u r i t yp r o t o c o l ，i t a l s oi n t r o d u c e st h e p r i n c i p l e s ，c h a r a c t e r i s t i c s o fm o d e lc h e c k i n gt o o ls p i na n di t s m o d e l i n g l a n g u a g ep r o m e l ae m p h a t i c a l l y t h e nt h ep a p e rp r o p o s e st h er u l ea n d c o u r s eo fu m lm o d e l i n go f s e c u r i t yp r o t o c o l ，a n d t h e p r o c e s s o f t r a n s f o r m i n gu m l m o d e lo f s e c u r i t yp r o c o t o l t op r o m e l a p r o g r a m sa n d h o wt op r o d u c ea t t a c k e rm o d e la u t o m a t i c a l l ya r e p r e s e n t e d i no r d e rt o c o m b i n et h e v i s u a l d e s i g n o f s e c u r i t yp r o t o c o l w i t hi t s a u t o m a t i c a l l y v e r i f y i n g t h e a u t o m a t i cv e r i f i c a t i o nt o o lf o ru m lm o d e lo f s e c u r i t y p r o c o t o lh a sb e e nd e s i g n e d a n d d e v e l o p e d k e yw o r d s ：s e c u r i t yp r o c o t o l ，s p i n ，m o d e lc h e c k i n g ，u m l 第2 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检测 i i 课题背景 第一章绪论 随着网络技术的应用与发展，特别是政府、军事机构，以及电子商务的兴起 与广泛应用，信息安全问题成为学术界和工业界共同关注的关键问题，在网络体 系的各个层次上，各种保障加密通信而制定的安全协议正在许多对信息安全敏感 的领域中发挥着重要的作用。一个安全协议在出台以前和发布之后，需要从多方 面对其安全性进行验证，已有的安全协议往往被证实并不如它们所声明的那样安 全。因此，安全协议的安全性成为网络安全的关键。 由于安全协议的重要性。近十几年来，世界各国学者对其设计和分析进行了 较为广泛和深入的研究。早期的研究人员主要是根据应用的具体需求设计了大量 的安全协议，并且基于经验和单纯软件测试来分析其安全性，大多安全协议的设 计方法是通过分析已有协议的有效性和安全性，结合具体应用需求进行改进、完 善，从而设计出新的安全协议。由于根据经验和软件测试方法来设计和分析安全 协议是非常脆弱、危险的，远不能满足新的安全应用需求。因此出现了许多形式 化研究方法。其中模型检验是一种很重要的自动分析和验证技术，其实质是利用 计算机的快速计算能力，通过穷举系统模型的有穷状态空间中的每个状态来验证 该系统是否满足特定的形式规约。相对于传统的形式化证明方法而言，模型检验 方法具有快速、全自动的优点。模型检测已经在硬件电路、协议验证、软件系统 规范与分析中得到成功的应用。而且出现了许多检测工具，如用于并发系统工具 s m v 、s p i n 等，其中s p i n 是贝尔实验室开发的一种通用验证系统，它支持分布式 系统( 如数据通信协议分布式0 s 、数据库系统等) 的设计和验证，它采用 p r o m e l a ( p r o c e s sm e t al a n g u a g e ) 作为建模语言，主要通过进程和消息来描述分 系统模型。 为了把自动检测结合至4 设计阶段，人们提出了许多针对u m l 自动模型检测的方 第5 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检测 法，并开发出了许多针对不同应用的工具，比如自动转化u m l 状态图到s p i n 的方 法嘲。”，自动转化u m l 活动图的方法，用于自动验证可视化建模语言的工具旧， 转换u m l 状态图到s p i n 的v u m l 工具旧等。 1 2 本文的主要工作和目标 在安全协议的设计阶段，如果能结合可视化的方法来对安全协议进行建模， 以直观、形象的方法来描述安全协议的通信过程，这样，可以使设计人员能更进 一步分析协议的性质和可能存在的错误。在可视化建模的基础上进一步对安全协 议模型进行形式化的检测将保证设计的协议更具有安全的需求。通过可视化和形 式化的方法来保证设计协议的安全性和准确性。 统一建模语言u m l ( u n i f i e dm o d e l i n gl a n g u a g e ) 是一种描述能力强大且含 义直观的可视化建模语言，基于u m l 的开发方法和软件建模环境已经广泛应用于 各种软件开发过程。它已经成为面向对象软件开发的标准建模语言，它提供多种 图元从不同角度和应用层次刻画系统特性以及复杂的运行环境0 1 。u m l 的可视化描 述能力正是降低安全协议设计过程中复杂性的有效方法，然而，由于u m l 是一种 半形式化的建模语言，满足不了安全协议对高安全性的需求。另一方面，虽然对 安全协议的验证有严格证明的形式化，却要求设计人员必须具备高的形式化描述 能力。取长补短，本文正是结合上面提出的方法的长处来降低安全协议的设计难 度，本课题研究的具体内容和方法如下： l 、研究安全协议的特性和模型检测的方法和原理：通过分析安全协议的性质， 以便建立合法主体的通信模型以及攻击者的模型。对s p i n 检测工具进行研究，着 重研究其检测原理以及建模语言p r o m e l a 的特点。 2 、采用u m l 对安全协议进行建模：采用u m l 类图来描述安全协议的基本信息， 并采用顺序图来描述安全协议的通信过程，并提出建模的规则。 3 、工具实现：开发一个堋l 到s p i n 建模语言p r o m e l a 的转换器，实现安全协 议的u m l 模型的自动检测，验证是否满足所需要的安全需求。 通过本课题，得出通过u m l 对安全协议的建模过程，着重建立攻击者模型，并 第6 页麸7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议台建模和自动检秘 开发一个转换工具对i j m l 产生雕x m i 文件进行转换，得至) j s p i n 的输入语言p r o m e l a ， 从而实现可视化建模和进行自动检测的功能。 i 3 论文的结构 论文分成8 章，第1 章绪论，介绍了课题的背景，并分析现在存在的问题，提 出课题的主要内容和要实现的目标。第2 章安全协议，主要分析了安全协议的特 点以及形式化方法。第3 章模型检测，主要介绍了时态逻辑以及模型检测工具s p i n 。 第4 章统一建模语言u m l ，主要分析其建模方法，以及本课题主要运用的类图以及 顺序图。第5 章安全协议的建模，主要提出采用u m l 对安全协议进行建模的方法， 其中采用类图来描述协议的基本信息，用顺序图来描述协议的通信过程。第6 章 自动验证，分析了怎样自动产生攻击者模型，给出了自动转换工具的原理和实例 研究。第7 章自动验证工具的设计与实现。第8 章结束语，对本课题进行总结， 给出研究成果和将进一步研究的工作。 第7 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检测 第二章安全协议 2 1 安全协议的类别和性质 所谓协议，就是两个或者两个以上的参与者为完成某项特定的任务而采取的一 系列步骤“1 。这个定义包含三层含义： ( 1 ) 、协议自始至终是有序的过程，每一个步骤必须执行，在前一步没有执行 完之前，后面的步骤不可能执行； ( 2 ) 、协议至少需要两个参与者； ( 3 ) 、通过协议必须能够完成某项任务。 安全协议是建立在密码体制基础上的一种交互通信协议，它运行在计算机通信 网或分布式系统中，为安全需求和各方提供一系列步骤，借助于密码算法来达到 密钥分配、身份认证、信息保密以及安全地完成电子交易等目的。协议的参与者 可能是可以信任的人，也可能是攻击者和完全不信任的人。安全协议包含某种密 码算法，在网络通信中最常用的、基本的安全协议按照其完成的功能可以分成以 下三类： ( 1 ) 、密钥交换协议 一般情况下是在参与协议的两个或者多个实体之间建立共享的秘密，通常用于 建立在一次通信中所使用的会话密钥。协议可以采用对称密码体制，也可以采用 非对称密码体制，例如d i f f i e h e l l m a n 密钥交换协议。 ( 2 ) 、认证协议 认证协议中包括实体认证( 身份认证) 协议、消息认证协议、数据源认证和数 据目的认证协议等，用来防止假冒、篡改、否认等攻击。 ( 3 ) 、认证和密钥交换协议 这类协议将认证和密钥交换协议结合在一起，是网络通信中最普遍应用的安全 踟议。常见的有n e e d h a m - s c h r o e d e r 协议、分布认证安全服务( d a s s ) 协议、i t u t 第8 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检测 x 5 0 9 认证协议等等。 ( 4 ) 、电子商务协议 这类协议中主体往往代表交易的双方，其利益i f l 标是不一致的，或者根本就是 矛盾的，电子商务协议关注的就是公平性，即保证交易双方都不能通过损害对方 利益而得到不应得到的利益。常见的电子商务协议有s e t 协议等”3 。 安全协议的主要目的在于通过协议消息的传递来达成通信主体身份的识别与 认证，并在此基础上为下一步的秘密通信分配所使用的会话密钥，因此，对通信 主体双方身份的认证是基础，是前提，而且在认证的过程中，对关键信息的秘密 性及完整性的要求也是十分必要的。对于安全协议，一般有下面的一些性质要求： ( 1 ) 、认证性 认证是最重要的安全性质之一，所有其他安全性质的实现都依赖于此性质的实 现。安全协议的认证的实现是基于密码的，一般通过对称密码或非对称密码来实 现。在协议的实体认证中可以是单向的，也可以是双向的。认证过程除了通信双 方参与的情况之外，也可以借助第三方来证明其身份。 ( 2 ) 、保密性 通信内容不向非授权拥有此消息的人泄露，就算被截取，也没有方法从中得到 任何有用的消息。保密性一般由加密来完成。在安全协议中，一般不考虑具体的 密码算法的执行细节，并且假设加密算法能达到理想的状况，即没有密钥就不可 能对该加密的消息进行破解。 ( 3 ) 、完整性 为了保护协议消息不被非法篡改、删除和替代，安全协议必须具有完整性。为 使安全协议具有完整性，可以通过对消息进行封装和签名来实现。 ( 4 ) 、不可否认性 在某些安全协议中，不可否认性是一项重要的性质，比如电予商务协议，为了 保证参与双方的利益，实现公平性，不可否认性能为交易双方提供证据，以防止 出现事后否认的情况。 安全协议是网络通信和分布式系统安全的基础，确保协议的安全运行是极为重 要的。虽然协议一般只由几条消息组成，但由于其运行环境的复杂性，攻击者处 第9 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检测 处存在，而且对攻击者进行建模也是很复杂的过程，难以估计攻击者的能力。另 一方面，安全协议本身也具有高并发性的特点，因而使得对安全协议的设计和分 析变得更加复杂和困难哪。 2 2 安全攻击 安全协议的实际执行环境一般是不安全的，即可能存在着消息通道阻塞，消息 可能丢失的情况，还可能存在着恶意的攻击者。在设计安全协议时，必须对攻击 者有全面和深刻的认识，这样才可能设计出能够抵抗己知的各种攻击， 由于我们所执行安全协议翰环境十分复杂和不安全，因此，我们应当假定攻击 者具有可以控制整个通信网络的知识和能力。比如，我们应当假定攻击者除了可 以窃听、阻止、截获所有经过网络的消息之外，还应具备以下知识和能力： ( 1 ) 、熟悉加密、解密、散列等密码运算，拥有自己的加密密钥和解密密钥。 ( 2 ) 、熟悉参与协议的主体标识符及其公钥。 ( 3 ) 、具有密码分析的知识和能力，攻击者能通过分析有用的消息来增加它的 知识库。 ( 4 ) 、具有进行各种攻击，比如重放攻击的知识和能力，攻击者能依据它的知 识库产生消息并发送给协议的合法主体的能力。 ( 5 ) 、清楚协议的执行过程。 为了建立攻击者模型，必须对攻击者的攻击方法和能力做充分的假设。 2 3 形式化方法 近十几年来，世界各国学者对安全协议的设计和分析进行了较为广泛和深入的 研究例。早期的研究主要根据应用的具体需求设计了大量的安全协议，并且基于经 验和单纯软件测试来分析其安全性，大多数安全是通迸分析已有协议的有效性和 安全性。结合具体应用嚣求进彳亍改进、完善，两设计出新的安全协议。目前，对 安全协议进行分析的方法主要有两大类：一类是攻击检验方法；另类是形式化 第l o 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检测 的分析方法“1 。 攻击检验方法是通过搜集使用目前对协议的有效攻击方法，逐一对安全协议进 行攻击，检验安全协议是否具有抵抗这些攻击的能力。在分析的过程中主要使用 自然语言和示意图，对安全协议所交换的消息进行剖析。这种分析方法往往是非 常有效的，关键在于攻击方法的选择。 形式化的分析方法是采用各种形式化的语言或者模型，为安全协议建立模型， 并按照规定的假设和分析，验证或证明协议的安全性。目前，形式化的分析方法 是研究的热点，但是就其实用性来说，还没有什么突破性的进展。总的来说，形 式化方法可以分成四类： ( 1 ) 、使用通用的、不是为分析安全协议专门设计的形式化描述语言和协议校 验工具，来建立安全协议的模型并进行校验。其主要思想是将安全协议看成一般 的协议，并试图证明协议的正确性。采用的工具和模型与验证一般协议的类似， 例如使用有限状态图、p e t r i 网模型、l o t o s 语言等等。这种方法的一个主要缺点 是仅证明协议的正确性而不是安全性。 ( 2 ) 、安全协议的设计者设计专门的专家系统来制定协议的校验方案并进行协 议检验，从而对协议的安全性做出结论。其主要思想是根据协议的设计开发专用 的专家系统，使用专家系统发现协议是不是能够达到不合理的状态。这种技术能 够很好的识别缺陷，但是不能证明协议的安全性，也不可能发现未知的缺陷。 ( 3 ) 、使用基于知识和信念的逻辑来建立所分析的协议的安全需求模型。这种 方法是目前为止使用最广泛的一种方法，最著名的是b a n 逻辑。b a n 逻辑是一个形 式逻辑模型，进行基于知识和信任的分析。b a n 逻辑假设认证是完整性和新鲜度的 函数，使用逻辑规则来对协议的属性进行跟踪和分析。一般b a n 逻辑只能推出认 证的结果，而不能对一般安全性进行证明。 ( 4 ) 、基于密码学系统的代数特性开发协议的形式化模型，这种方法是将安全 协议系统当作一个代数系统模型，表示协议的参与者的各种状态，然后分析某种 状态的可达性。m i c h a e lm e r r i t t 已经证明了代数模型可以用来分析安全协议。 美国海军研究实验室( n a y y r e s e a r c hl a b ) 开发的协议分析器是这种方法中 最成功的一个应用，可以用来在各种协议中寻找新的和已知的缺陷。 第1 i 页共7 2 页 华南师范大学硕士学位论文基于u m l 安全协议的建模和自动检测 一直以来，更多的研究专注于使用形式化方法对现有的协议进行分析与验证。 对于现存的很多协议，现有的一些形式化工具是否可以证明一个已知的协议是正 确，仍存在诸多问题。因此，更为审慎的成熟的方法是设计专用的方法及执行工 具以有助于安全协议的初始设计。 第1 2 页共7 2 页 华南师范大学硕士学位论文 基千u m l 安全协议的建模和自动检测 3 1 模型检测简介 第三章模型检测 近来，出现软件和硬件系统的需求验证方厦的许多强有力的工具，因为越来越 多的i t 行业认识到设计和检测中进行需求验证的重要。在一些主要的大型公司， 比如：i n t e l ，西门子公司，b t ，a t t 和i b m 等，它们把检测工具的研究作为公司 发展计划中的一部分，并且投入大量的人力和物力“。 作为众多的形式化方法中的一种，模型检测主要采用搜索给定的系统模型的所 有状态，并验证每一个状态是否符合所要验证的需求规约。模型检测与其它形式 化方法相比，具有以下两个优点： ( 1 ) 、模型检测具有全自动的性质，它的验证过程不需要任何人进行观察或者 需要具备逻辑推理的专家的指导。同时，它也能作为一次运行的模拟工具，这能 使检测人员及早发现错误。 ( 2 ) 、当系统不满足所需求规约时，模型检测总会给出一个导致系统失败的运 行路径，通过这一路径，设计人员可以找到失败的原因，加以修改后再进行检测， 直至满足。 模型检测主要通过对建立的系统模型的状态空间进行搜索来进行需求规约的 验证。检测一个系统，需要先建立系统的模型，这需要对描述的系统进行一些形 式化的处理以符合形式化验证工具的输入语言。有时候出于对时间和资源的考虑， 必须对系统模型进行抽象来压缩模型的状态空间。建立系统模型后，在验证之前 应该给出所要满足的需求规约，需求规约一般使用时态逻辑来表示，当前主要采 用计算树时态逻辑( c t l ) 和线性时态逻辑( l t l ) 来表示需求规约的“。最后，运用 模型检测工具来验证所给的系统模型是否满足需求规约。如果用m 来表示系统模 型，用t 来表示需求规约，那么模型检测就可以表示为： m i t 如果m 中的每一个状态都满足t ，那么m 满足所需求的规约，反而，检测工具 第1 3 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检测 将给出一条导致m 不满足t 的运行路径。 3 2 时态逻辑 模型检测是基于时态逻辑，在模型检测中，主要采用时态逻辑来描述系统所要 满足的需示规约。也就是在m | = t 中，t 就是用一些时态逻辑表示的公式。时态逻 辑是在命题逻辑基础上演变而来的，通过引入适当的时态算子来描述和解释断言 随时间的变化。它与命题逻辑和谓语逻辑不同的是，时态逻辑公式不是那种静态 的为真或者为假的逻辑公式，因为时态逻辑的模型可能由几个状态构成，时态逻 辑公式可能在一些状态为真，在其它为假，因此，该公式的值随着状态的变化而 变化。依据对系统状态的时间路径的不同刻画，时态逻辑可以分成两大类：计算 树时态逻辑( c t l ) 和线性时态逻辑( l t l ) 。 3 2 1 c t l ( 计算树逻辑) c t l 是由c l a r k e 和e m e r s o n 提出的。它的运算符具有简单的性质，可以有效 地计算某一公式在有穷状态模型处于某一状态时是否满足。由它的名称可以想象， 它是一种时间模型采用树的方式、具有多个分支的不确定状态路径构成。c t l 的路 径公式由以下规则产生： ( 1 ) 、每一个原子命题是一个c t l 公式； ( 2 ) 、如果f 和g 是c t l 公式，那么下面的公式也是c t l 公式 一f ，t a g ，f v g ，k x f ，e x f ，a f f ，e f f ，a g f e g f ，h ( f u g ) ，e ( n j 勤 c t l 的路径公式中，主要由五个时态算子组成：a 、e 、x 、f 、b 、u ，时态算子 都是成对出现的，以a 或者e 开关，后面跟着x 、f 、g 、u ，一般有下面的配对a x ， e x ，a g ，e g ，a u ，e u ，a f ，e f 。下面将介绍各时态算子的含义。 _ a ( a l o n ga l lp a t h s ) 的含义为：沿着全部的状态路径。 一e ( t h e r ee x i s t s ) 的含义为：存在着至少一条状态路径。 - x ( n e x ts t a t e ) 的含义为：当前状态的下一个状态。 第1 4 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和白动检测 一 f ( s o m ef u t u r es t a t e ) 的含义为：当前状态之后的某些状态。 g ( a l lf u t u r es t a t e s ) 的含义为：当前状态起的所有状态。 下面用f 表示路径公式，那么c t l 的路径公式e f f 的含义为至少存在着一条状 态路径上的某些状态上使得公式f 为真时才为真，假设顶点状态为当前状态，图 3 - 2 1 表示该公 图3 - 2 一l 同e f f 相比，e g f 表示至少存在着一个路径，从当前状态起，该路径上的所有 状态都使得公式f 为真时，e g f 为真，如图3 2 2 所示： 对于a g f ， 真。如图3 - 2 图3 - 2 2 第1 5 页共7 2 页 足f 为真时才为 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检测 对于公式a u 和e u ，首先说明一下时态算子u ，对于公式p u q 表示在一条路径 上，存在着某状态，从该状态起，公式p 都保持为真一直到出现q 为真的状态为 止，那么p u q 就为直，如3 - 2 3 图所示： s os 1s 2s 3s 4 s 5s 6s 7s 8s 9 、 q p 图3 - 2 - 3 因而对于公式a ( p u q ) 表示如果所有的路径都满足使p u q 为真，那么公式a ( p u q ) 为真。同样对于公式e ( p u q ) 表示，如果至少存在着一条路径使得公式p u q 为真， 那么公式e ( p u q ) 为真。 c t l 公式之间存在着下面这些恒等式： a x f = 一e x ( 、f ) _ e f f = e t r u e u f a g f = 1e f ( _ 1f ) 一a f f = 、e g ( 一f ) _ a f u g = 一e 一g u ( 一f a g ) 八1e g lg 3 2 2 l t l ( 线性时态逻辑) l t l 只用来描单一的计算路径，时间是线性顺序的，即对于任意的状态s 和t ， 它们满足s t 中的一种。路径公式由以下规则产生： ( 1 ) 、如果p 是原子命露公式，那么p 是一个路径公式。 ( 2 ) 、如果f 和g 是路径公式，那么 、f ，f a g ，f v g ，x f ，f f ，g f ，f u g 都是路径公式。 第1 6 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建模和自动检溅 3 3 模型检测工具s p i n 3 3 1 s p i n 工具 s p i n ( s i m p l ep r o m e l ai n t e r p r e t e r ) 作为模型检测中的一种被广泛应用的、 具有通用的验证工具，它是由贝尔实验室开发的。它不仅能对分布式系统的设计 进行系统的逻辑一致性验证，最近还用来对安全协议的安全性进行验证。s p i n 主 要采用模拟异步进程全部的执行方式来验证系统的执行过程，现实中，s p i n 通过 模拟系统的执行并产生包括系统所有的执行路径的c 程序来搜索系统模型的状态 空间。在s p i n 的验证之前，需要输入以l t l 公式表示的需求规约“”。 在进行系统的验证之前，需要对系统进行建模，s p i n 采用p r o m e l a ( p r o c e s s m e t al a n g u a g e ) 语言来描述系统的模型，p r o m e l a 语言将在下一节进行详细的介绍。 p r o m e l a 程序的固有并发性及消息传递的通信机制很适合于描述分布式、并发系 统，它能模拟在分布式异步环境中协议实际运行的各种可能情况。s p i n 工具就是 基于这一语言的自动检测工具，它通过把p r o m e l a 语言所写的程序转化成有限状 态自动机，并和需求规约( l t l 公式) 所构成的自动机的补相乘，断定得到的自动 机所识别的语言是否为空。从而可以验证系统模型是否满足需求规约，是否有出 现设计错误。s p i n 为了方便人们的使用，推出了图形界面x s p i n “，如果验证过 程产生一个反例，用户可以在x s p i n 图形界面上看到这一反例的执行路径的图形 表示。 3 3 2 s p i n 状态优化技术 s p i n 为了提高有效的验证，提供了许多可以选择的优化算法“”。这些算法主 要包括状态压缩、状态向量压缩、数据流分析、o n - t h e f l y “”技术、偏序( p a r t i a l o r d e r ) 压缩、状态的比特哈希表表示法“、状态的最小自动机编码和切片算法。 在对系统自动机与需求规约自动机的补进行相乘判空时，s p i n 采用了 第1 7 页共7 2 页 华南师范大学项士学位论文 基于u m l 安全协议的建模和自动检测 o i l t h e f l y 技术来减小产生的状态空间，只有在需要的时候才生成系统的自动机 状态，当找到反例时，s p i n 就终止，这样就有可能不用产生完全的系统状态空间， 这样就可以缩减系统需要产生的结点数。 在状态空间的管理上，s p i n 采用了状态的比特哈希表表示法，在传统的状 态空间管理上，一般是采用了哈希法( h a s h i n g ) 来管理状态的，哈希法可以快速 的定位状态在内存中的位置，即用一个与状态相关的索引值作为哈希函数的变量， 然后哈希函数计算这一状态的哈希值。假设哈希表中有h 个空间用来存放状态， 那么哈希函数能返回从0 到h - l 的值，如果状态空间集为a ，那么当a h 时，将出 现不同的状态值返回相同的哈希值，即出现哈希冲突问题。为了解决这一问题， 可以把具有相同哈希值的状态存放在一条链表中，但因此增加了存放指示下一状 态节点指针的开销，对于数目巨大的状态空间来说，这一开销经常能导致机器内 存的不足，从而搜索的状态空间受限。另一方面，用于存放一个状态节点的空间 也需不少的内存，这样就把检测的系统的状态空间的大小限制在一个小数量级上。 为了解决上述问题，采用了新的状态空间管理方法。主要思想：由于在搜索的过 程中，只要知道当前状态是否已经被检测过就足够了，因此可以用1 比特的内存 空间标记一个状态。这样，如果机器有m 字节的内存，那么可以容纳8 m 的状态空 间。如有i o m 的内存，状态空间可达8 千万之多。这样就可以大大提高状态空间 的数量级。另外，用于定位的哈希空间也就大大的提高，这样出现哈希冲突的机 率就大大的减小了。当然，这一方法同样存在着哈希冲突的问题，当出现冲突时， 即如果新搜索的状态的比特位被标识为已访问，那么算法就认为这一新的状态已 经被访问，从而忽略对这一状态的检测。随着所检测系统的状态空间增加，在传 统内存管理方法上，搜索的覆盖度就呈数量级的下降。而新算法只出现微量的下 降。传统的内存管理方式还存在另一个问题，那就是，它受状态存取单元的影响， 但新的方法却不会。 s p i n 还采用了偏序压缩方法来减小系统的状态空间。这是一种解决并发系 统出现的状态空间爆炸的有效方法，它能对并发系统中运行的并发事件交替执行 的各种顺序迸行删减。如果两事件按不同的交替顺序执行所到达的结果都一样， 那么就称这两件事件相互独立。并发系统中的事件是并发进行的，因而存在着事 第1 8 页共7 2 页 华南师范大学硕士学位论文 基于u n l 安全协议的建楱和自动检潞 件的交替运行所形成的大量执行顺序，对这些执行顺序都进行检测，很大可能就 会出现状态爆炸问题。另一方面，由于独立事件的存在，它们执行的一条路线将 等价于全部的执行路线，因此，只对一条执行路线进行检测就可以达到目的，也 即可以删除多余的执行路线。从而可以大大的减小状态空间的大小。 3 。3 3 p r o m e l a 语言 s p i n 检测工具采用p r o m e l a ( p r o c e s sm e t al a n g u a g e ) 语言作为系统建模的 语言。它是一种类似于c 的语言，主要采用进程的异步执行来模拟系统，并通过 消息通道在进程之间进行通信。消息可以是同步消息，也可以定义为异步消息， 因此p r o m e l a 很适合于描述并发系统、分布式系统和协议。 p r o m e l a 语言主要由进程、消息通道和状态变量三种对象组成。进程用来指明 系统的行为，消息通道和全局变量用来定义这些进程的交互方式和运行的环境。 一个p r o m e l a 程序主要由下面几部分组成“： 1 、m t y p e 类型 p r o m e l a 中的数据类型用m t y p e 来声明，比如程序3 - 3 一l 中的 m t y p e = n a ，a ，n b ，b ，它就象其它语言中的常量声明一样，这里声明四个常量，这 些常量将在进程中使用。也可以用m t y p e 来声明变量，比如程序3 3 1 中的m t y p e v n a 语句声明v n a 为m t y p e 类型，它的值可为 n a ，a ，n b ，b ) 中的任何值。 2 、变量类型 在p r o m e l a 中的基本数据类型包括：b i t 、b 0 0 1 、b y t e 、s h o r t 、和i n t ，它们 声明一次只能存储一个值的对象。类型声明的形式为 ，比如b i t t u r n = l ，那么变量t u r n 被定义为b i t 类型。每一种类型都有它表示值的范围： b i t 0 1 b o o l o 1 b y t e 0 2 5 5 s h o r t 一2 ”一l 2 1 l 1 i n t 一2 扎1 2 ”1 第1 9 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安全协议的建楱和自动检测 除了声明单个变量之外，还可以声明数组，比如：b y t ea 2 7 ，b i tf l a g s 4 。 3 、语句 在p r o m e l a 语言中，语句或者是可执行的，或者是阻塞的，取决于变量的当前 值和消息通道的当前内容。比如语句3 + x ，当变量x 的值不为一3 时，该语句将被 执行。 p r o m e l a 语言中的语句除了基本的表达式之外，还包括s k i p 表达式，它总是 执行语句，但该语句不执行任何操作。除此之外，还包括r u n 语句，它也是总是 执行语句。 由于p r o m e l a 语言中的进程交替执行，为了表示一些语句按整体执行，p r o m e l a 定义了一些原子语句来表示原予动作，这些原子语句包括a t o m i c 和d _ s t e p 两种。 如果需要声明几个语句按原子性执行，可以用a t o m i c 来声明，比如 a t o m i c s t a t l ：s t a t 2 ；s t a t n ，当其中的语句都为可执行语句时，它们将按原 子顺序执行，当它们执行完成后才有可能执行其它进程的语句，即不会存在其它 语句在这些语句之问执行，但当这些语句s t a t i 存在着阻塞状态时，将执行其它 进程的语句，这样就可能出现a t o m i c 不是原子性的情况。语句d _ s t e p 是a t o m i c 的更有效的版本，它不出现a t o m i c 不是原子性的情况，它声明的语句不产生中间 状或存储这些中间状态，因而更有效率。在p r o m e l a 中采用原子语句可以在一定 程度上减小系统的状态空间。 4 、控制流程 选择语句：p r o m e l a 语言通过i f f i 语句来表示选择，比如 i f ：c h o i c e l 一 s t a t i ： ：c h o i c e 2 一 s t a t 2 ： ： ：c h o i c e n 一 s t a t n ： f i ： 如果条件c h o i c e i ( i = l n ) 中有不止一个条件为真的时候，程序将进行不确 定的选择一个分支执行。另一方面，如果没有一个条为真，那么i f 语句将被阻塞， 第2 0 页共7 2 页 兰塑墅蔓查兰塑圭堂垡堡奎 苎王望坠室全些坚箜塞堡塑量i 塑墨 直至有条件为真为止。 循环语句：p r o m e l a 语言通过d o o d 语句来表示循环，比如 d o ：c h o i c e l 一 s t a t l ： ：c h o i c e 2 一 s t a t 2 ： ： ：c h o i c e n 一 s t a t n ： o d ： 与选择语句只执行一次不同，循环语句将循环执行，直到遇到b r e a k 语句或者 其它的转移语句，比如g o t o 语句，才能跳出该循环。循环语句除了执行次数与选 择语句不同之外，其执行方式与选择语句相同。即有多个条件为真时采用不确定 的选择方法。 5 、消息通道 p r o m e l a 语言主要通过消息通道来实现从一个进程到另一个进程传递数据，其 声明形式为c h a n = o ff ， ，( t n ；其中c h a n 为 消息通道声明的关键字，c h a n n a m e 为消息通道名，d i m 为消息通道可以缓存的消 息的条数，不同的值将使消息通道对应不同的类型，当d i m = o 为时，那么该消息 通道将会是同步方式来通信，如果d i m o 时，那么消息通道将会是异步方式来通 信。比如程序3 3 一l 中的消息通道t o s 为同步方式的通道，而t o r 为可以缓存一 条消息的异步通道。 当要向一条消息通道发送消息m s g 时，可以采用这样的方式c h a n n a m e ! m s g ， 那么就向消息通道c h a n n a m e 发送消息m s g ，另一方面，如果要消息通道中接收消 息时，可以采用变量来存放消息的值，比如c h a n n a m e ? v a r ，表示从消息通道 c h a n n a m e 中接收消息，并放入v s r 中。发送消息的通道只有在消息通道不为满时 发送消息才不是阻塞的，而接收消息的通道只有当消息通道中消息不为空时才不 是阻塞。当要保证所接收的消息的值为定值时，可以采用这样的方法 c h a n n a m e ? e v a l ( n a ) ：这里，e v a l 表示相等的语句，当消息通道c h a n n a m e 中的消 息值为n a 时，该消息通道语句才被执行。因此可以采用这种方法来保证所期望要 第2 1 页共7 2 页 华南师范大学硕士学位论文基于u m l 安全协议的建模和自动检测 接收到的消息值。 6 、进程类型 为了执行一个进程，用户必须先对它进行声明，进程通过关键字p r o c t y p e 来 声明。一个进程的声明主要包括下面几个方面： 进程的名称：用户必须为每一个进程命名。 进程传递的参数列表：为了能从外界传递数值给该进程，需要声明要传递的数 据的类型，比如程序3 - 3 - 1 中的p r o c t y p es e n d e r ( m t y p en o n c e ：m t y p es e l f ；m t y p e p a r t y ) 进程的声明中，为进程声明了三个m t y p e 类型的参数。当然如果进程不需 要外界传递数值给它时，可以设置参数列表为空。 局部变量：进程为了处理数值的需要，可以定义局部变量，比如，进程需要用 局部变量来为消息通道存放接收的数值，可以声明一个局部变量m t y p ev a r ：并在 消息中应用，t o r ? v a r ；该变量将用来存放从消息通道t o r 中传递来的第一个m t y p e 类型的数值。 进程主体：进程的主体部分主要包括消息的收发和一些控制流程。 一个进程主要通过两种方式来与其它进程进行交互，一种是通过进程之间共享 的全局变量的访问和操作来进行交互，另外可以通过消息通道来与其它进程进行 交互。 7 、i n i t 进程 每一个程序都有它的启动入口，在c 语言中，程序的入口点为m a i n 函数，而 在p r o m e l a 语言中，程序的入口点为i n i t 进程，在一个程序中，有且只有一个i n i t 进程，在i n i t 进程中，将通过进程创建关键字r u n 来启动其它进程的执行。比如 在程序3 3 1 中，i n i t 进程将启动s e n d e r 进程和r e c e i v e r 进程，并为它们传递 它们所需要的参数数值，这时s e n d e r 进程和r e c e i v e r 进程将异步执行。 m t y p e = n a ，a ，n b ，b ) ： c h a nt o s = 0 o f m t y p e ，m t y p e ，m t y p e ) ： c h a nt o r = 1 o f m t y p e ，m t y p e ，m t y p e ： b o o lf l a g ： p r o c t y p es e n d e r ( m t y p en o n c e ；m t y p e s e l f ；m t y p ep a r t y ) 第2 2 页共7 2 页 华南师范大学硕士学位论文 基于u m l 安垒协议的建摸和自动检测 b i tk _ a = o ： 进程主体内容 p r o c t y p e