（计算机软件与理论专业论文）基于状态转换容侵系统模型的smv分析与改进.pdf

基于状态转换容侵系统模犁的s m v 分析与改进 基于状态转换容侵系统模型的s m v 分析与改进 专业：计算机软件与理论 颤生：赵扶欣 导师：苏开乐 摘要 容馒技零是力强太型嬲络缀务器在受到攻击磊，戆继续提供羧务( 葳提供舞 级服务) 的一项网络安全技术。本文介绍了基于状态转换的容侵系统模型，同时 根据现在网络攻击的类獭，构造出了攻击者的有限状态转换模型。通过容侵系统 模篓与攻拳者模黧懿耪互俸瘸，菠瘸s m v 涞对容侵系统进行分掌厅。分耩结聚表 明，容侵系统模型著不通用于所有的嗣络攻击。在此论文中对容侵系统模型逃行 了改进，同时对改进后的模型进行了s m v 分析，最后对此模型的每一个改谶都 给出了稻应的实镄。 关键诃：模聱检溅；容侵系统；s m v ；d d o s 基于状惫转攘吝寝系统模型魏s m v 分辑魏速 s m v a n a l y s i so fi n t r u s i o nt o l e r a n ts y s t e ms t a t e t r a n s i t i o nm o d e la n di m p r o v i n g m a j o r：c o m p u t e rs o f t w a r ea n dt h e o r y n a m e：z h a oc o n g x i n s u p e r v i s o r ：s uk a i l e a b s t r a c t i n t r u s i o nt o l e r a n c ei sa ne m e r g i n gn e t w o r ks e c u r i t yt e c h n i q u e ，w h i c h e n a b l e st h ev i c t i ms e r v e r s y s t e m s t oc o n t i n u e o f f e r i n gs e r v i c e s ( o r d e g r a d e ds e r v i c e s ) a f t e rb e i n ga t t a c k e d + as t a t et r a n s i t i o nm o d e lh a sb e e n p r e s e n t e dt od e s c r i b et h ed y n a m i cb e h a v i o ro fi n t r u s i o nt o l e r a n ts y s t e m s i nt h i sp a p e r ，w eb u i l da na t t a c kf i n i t es t a t es y s t e mb a s e do nt h er e c e n t n e t w o r ka t t a c k s ，a n du s es m v ，am o d e l c h e c k i n gt o o l ，t o a n a l y z et h e i n t r u s i o nt o l e r a n ts y s t e mb yt h ei n t e r a c t i o no ft h e s y s t e mm o d e la n dt h e a t t a c km o d e l t h ea n a l y s i sr e s u l t sd e m o n s t r a t et h a tn o ta l lt y p e so fa t t a c k s c a nb em a p p e dt ot h es y s t e mm o d e l w ei m p r o v et h i s s t a t et r a n s i t i o n m o d e la n du s es m vt op r o v et h ec o r r e c t n e s so ft h e i m p r o v e dm o d e l ， m o r e o v e r ，w eg i v et w oa t t a c ki n s t a n c e sm a p p e dt oo u r i m p r o v e dm o d e l k e yw o r d s ： m o d e lc h e c k i n g ；i n t r u s i o nt o l e r a n c es y s t e m ；s m v ；d d o s l i 基于状态转换容侵系统模型的s m v 分析与改进 1 1研究背景 第一章引言 网络的诞生，极大地方便了人们地沟通和交流，人们在日常生活和工作环境 日渐依赖信息系统。然而网络诞生之日起，网络安全问题就一商如影随形，蠕虫 病毒，分布式拒绝服务攻击。随着网络技术地飞速发展，新的威胁和脆弱点不断 出现，从而对网络信息安全技术提出了更高地要求。 计算机网络安全涉及计算机科学、通信技术、密码技术、信息论等多种学科。 其中包括人的恶意行为可能导致的资源( 包括信息资源、计算资源、通信资源等) 被破坏、信息泄漏、篡改、滥用和拒绝服务，包括一f 四个方而： 1 破坏资源的保密性。即泄密，对信息资源，指信息的语义、存在性等属 性在存键或妻乏瑗过程中被来援投的实体瓣获矮。 2 破坏系统或信息的完整性。在程序或数据的存储、传输过程中通过熊改、 插入、删除、熏发的方式，改变数据的语义或系统的功能。 3 。玻坏系统或馈惑戆霹弱j 鏊。逶过一定懿攻毒手段建褥系统无法提供有效 的服务甚至停止服务，进而使合法用户对信息资源、计算资源或通信资 源的合法访问无法进行。 4 。来授投弱矮爨资源。薅患资源、活冀资源或逶信炎源羧未授衩蕊实俸谴 用，这一威胁不破坏信息域系统的保密性、完整性和可用性，但怒可能 绘资源的所有精带来损失，如流黾盗用。 模蘩检溅鼓术跫一门鑫动纯羧零，这l 、l 技零验蠢e 骞藤毛爰态并行系统。羧垄检 测系统有两个输入：一个系统，我们需要验证这个系统的正确性；规格，系统具 有的属性：模型检测中主要的挑战就是状态空间的爆炸问题。这个问题足因为系 统中青许多穗互作竭滟因素或者密 二系缝中有餐杂戆数据结梅，蠢这些数攥结构 可以取许多不同的值。在这样一种情况下系统状态的数目会变得非常大。 模型检测技术的一个优点就熄它能够进行自动化的验证。程序通常使用一 耱对系绞豹状态空闻穷举援索豹过疆决定菜些麓格是否为真。给予足够的资源， 程序将总是以y e s n o 同答终结。 基t 状态转换容侵系统横型的s m v 分析与改进 模型柃测技术是一种检测有限状态并发系统的自动化检测技术，它主要用来 捡测i 鬲时态遥辑c t l ( c o m p u t a ti o nt r e el o g i c ) 或l t l ( l i n e a rt i m el o g i c ) 描述 | ! 勺规范。模型检测的工具主要有c m u 的s m v 1 ，b e l l 实验室的s p i n 2 等。 模型检测 3 ，4 ，5 是熄模型检验问题转化为检验趣动枧或转换系统礁是否滤 怒逻辑公式s ，鄙赫| = s 愁否成立的一种形式化验证技术。模型稔验已在硬搀电 路、安全协议的验证 6 ，7 、软件系统规格与分析、分布式系统验证中 8 中得别 了成功的应滕。 但是早期对有限状态系统进行模型捡验，系统的状态用显示表示的。验证进 行穷尽验证，但随着所耍验证的系统的增大，就出现r 状态爆炸的问题，为了解 决这个问题如现。r 符号化模型捡验。符号化模型检验对系统的状态用布尔函数进 行隐式表示，闽时搜索算法的改进，使褥在状态空间缮到了摄大麴改进。符号 模型检测工具s m v ( s y m b o l i cm o d e lc h e c k i n g ) 可以使得模型检测在机器上自动 运行。 援镪实验察在对援爨梭测对安全按议、分枣式系绞等憋建模霸验证中已经暇 了大量的研究，并取褥了一些成果 7 ，8 ，9 ，1 0 。 1 。2察侵系统模型的研究 随着i n t e r n e t 的飞速发鼷，耐络的安全性受到了臼益严羹的挑酸。一方澍 潮络攻击行为日益呈现复杂化帮自动化的趋势，拒绝服务攻击已经成为网络运行 的主要隐患。另一方面，由于网络中系统软件和应用软件的快速升级换代，各种 系统漏洞不断地祓发现，黼络带宽的迅速增长也使得信息的潞测变得更加困难。 这些挑战或需求搬动嘲络安全技术的发展。 容侵技术 儿 是近些年出现的新型网络安全技术，主要针对网络服务器受到 攻击后，服务器魑否能继续提供服务提出来的。现在犬型软件系统不可避免的存 在一些安全漏洞，和攻击者采取攻击的方法秘手段是不可预知的，对服务器来说， 确定受到攻击后能否继续提供服务比确定是受到的什么样攻击的类型更加重要。 对服务器的攻击类型可以分为：未授权使用瓷源，破坏服务器上资源的机密性， 破甥：系统或信息的完整性、可用性。攻击鳆类型不同，容镘系绞保护鲍对象逛苓 基于状态转接吝媛系缝摸警黪s m v 分援每教避 棚同。容侵系统就是在服务器受到攻击后，采取的一熄相应的措施，使服务器继 续提供鞭务，必要时提供臻级骚务。 容侵理论研究是网络系统安全研究地重要组成部分，国外也罴刚冈i 起步。美 围国防部目前关于容侵的资助项目有s i t a r ( s c a l a b l ei n t r u s i o nt o l e r a n c e a r c h i t e c t u r e ) 【1 l 】 、 i t t c i n t r u s i o nt o l e r a n c ev i at h r e s h 0 1d c r y p t o g r a p h y ) 1 2 、i t u a ( i n t r u s i o nt o l e r a n c eb yu n p r e d i c t a b i l i t ya n d a d a p t a t i o n ) 1 3 等，欧洲的项目( 2 0 0 0 - 2 0 0 3 ) 有m a f t i a ( m a l i c i o u sa n d a c c i d e n t a lf a u l tt o l e r a n c ef o ri n t e r n e ta p p l i c a t i o n s ) 1 4 】等。这些项蘸 主要从容侵理论和密码技术等方面出发，研究容侵技术和容侵系统地体系结构。 在这些项目地支持下，西方潮家在与容侵技术相关地领域内取得了许多显著地进 袋。 在重内，对容绳技术的磷究进行懿较少。骞侵技术关注的焦点怒，在入侵存 在的情况下系统是否可以正常的提供服务，系统所提供的服务是否舆有连续性， 数据地安全髓楚否能得到僳征。它要求系统即使在面稿入侵时，尽可能地保持提 供关键黢务瓣能力，并且尽餮傺涯关键臻崽的安全。 容侵技术作为新一代的信息安全技术，结合密码披术、容错计算技术和网络 安全控术，着眼于在人侵绝对存在的情况下，它通过摅供时间、空间地数据冗余 以及凌源酶耄秘寒据供一定懿服务矮量，叛藏提裹象缝懿安全毪。攘甸疆淀，容 侵技术旨在提高系统自身的免疫力，使得系绒对于非关键的入侵都可以保持信息 的究戆性、百用性和秘密性，从而提高信怠系统的安全性。 k a t e r i a ng o s e v a - p o p s t o j a n o v a 毒秘f e i y iw a n g 等人裁震竣态转移圈模型绘 出了容侵系统的动态行为( 1 5 。这个模型有助于描述已知的和未知的安全攻击。 遮篇论文超因于以下谍题：国际上出现的对容侵技术的系统化研究中，已经 敬褥了虢土掰讨论麓熬分畿桊。但是，还没有对系统送 子形式讫静骚涯，不麓鸯 定系统实现或系统模型是否满足系统规约的要求。 在本文中介绍了基于状态转换的容侵系统模型 1 5 】，同时根据现在网络攻击 熬类麓，穆造& 了敬击者的有黻状态转换篌黧。给出了系统要满足的躐麴。通过 察侵系统模型与段潦者模型的相互作用，使用s m v 来对客经系统进行分析。分析 结果表明， 1 5 中的容侵系统横裂并不邂用予所有的阈络攻击。本文对容侵系统 蓝r 桃态转换容侵系统镆型的s m v 升析与改进 模型进行了改进，并对改避后的模型遴行了s m v 分褥，最后对此模型的每一个改 进都给出了相应静实例。 1 3研究的动机和鼠的 1 3 1 动机 根据藏蠢i | = 戆讨论，容缓系统是在暇务器受至攻壹缒靖嚣下缝继续提供服务藏 降级服务，嗣时现在我们已经很清楚对服务器进 j = 网络攻击的方式，这样我们就 可以给出容侵系统模型要满足的系统规约以及可以构造出攻击辫进行攻击的状 态转接模登。簿号化模燮捡测是对系绞瓣菝态爱蠢尔交数遘嚣爨式表示，霹时羧 索算法的茂进，使得在状态空间上得到了很大的改进。符号模型检测工具s m v 可以使得模飘检测在机器上自动运行。文献 1 5 中的撼于状态转换的容侵模型的 羧态转换楚数嚣是有疆熬，我翻稳逡瓣攻壹者敬状态转换横蝥鹃获悫龟是有戮 的，这两个模型之间消息的传递可以看作是有限状态的转移，这样就使得此模裂 可以通过s m v 来进行验证。 本论文鹣瓣翡羲楚对一个套 受系绫援鍪进孝子符争沲模型验疆。篱先对客经系 绕基于状态转换懿模登避行穷缨，横援臻在弼络攻击豹类型梅逑出攻壶耆状态转 换模型，同时给出了容侵系统模型要满足的一些规则。通过容侵系统模型和攻击 誊系统禳鍪豹籀豆释；雳，在s 孵上遴行验涯，验证豹绣祭表稿寮僚系统模型著不 蹙完备靛，在本论文中疆出了改遂懿模登，著聪改进露麴模型漆孬了形式化懿验 舐，给出旗子改进后模型的实例。以上的容侵系统模型、构造的攻击者模型、对 系统进行的糕麴、整个辍证过程、验证络鬃、改遂焉酌摸墅和实铡分祈将会嬲深 辩鸯馒系统秘对系绞邈褥镑号倦验证靛谈谖，筑巍可勰会薄整令容橙技术器茨蕊 鞠i 符号化验证谯网络安全中的应用有所价值。 基丁状态转换容侵系统模型的s m v 分析与改进 1 4论文组织 在第二章中介绍了模型检测技术，其中包括进行模型检测的过程、如何模拟 系统、符号化模型检测和c t l 的语法和语义。 第三章详细介绍了基于状态转换容侵系统模型，建立此模型上的系统可以允 许多个容侵策略并存并且支持不同级别的安全需要。同时，由于此状态模型是根 据攻击对系统服务所造成的影响，不是攻击过程本身，只要某种攻击对服务器产 生的破坏的效果和此模型中已知的攻击所产生的效果类似，就可以根据此模型来 处理这种攻击。在本章中根据现在唰络攻击的类型构造出了攻击者模型，对每一 个状态和每一个状态转移都进行了详细的说明。 第四章对系统进行s m v 分析，其中包括如何在s m v 上针对此容侵系统的模型 建立系统模型、以及给出系统性质的描述和分析其验证结果。根据验证结果对原 模型进行了改进，对改进后的模型也同样进行了s m v 分析，表明它的完备性。 第五章根据现在非常流行的攻击，给出了相应改进后模型的如何进行状态转 移的实例。 第八章对繁篇论文的工作做了总结，归纳了本片论文所作的主要贡献，并对 未来的工作提出了建议和想法。 基u 状态转换窖侵蕞统模型的s m v 分析与改进 第二章模型检测技术 模型检测技术足一门自动化技术，遮门技术验证有限状态并行系统。这种方 法已经成功瘸予许多复杂豹电鼹设诗秘逶信强波验证。模型捡溅系绫有嚣个输 入：一个系统，我们想要验证的系统：规格，系统具有的属性。模酗检测中j e 骚 的挑战就是状态空间的爆炸问题。这个问题足因为系统中有许多相互作用的因索 或者出 系统孛有复杂懿数攥结秘，蕊这些数摆缝褥霹敬取诲多不霹瓣值；在这 样一种情况下系统状态的数目会变得非常大。 模型检测技术的一个优点就是它能够进行自动化的验证。检测程序通常使用 一耱霹系绕瓣状态空藏雾举搜索熬过程决定菜弩戴戆跫否为卖。缀定我嚣j 麓诗舞 机足够强大，检测程序将总是以y e s n o 回答终结。 2 。l 模型检测的过糕 把模型检测技术应用于澄汁由几项任务组成 1 6 。 模拟 模型检测王具都蠢定魄输入格式，瓣以第一项任务藏是恕个设计或系统 转化成模型检测工具能够接受的形式。在许多情况下，遮仅仅是一项编译工作。 在其他愤况下，建于时间积内存的局限，一个设计的模拟可能要求搜用抽象去减 少不楣关或不重要躲纲警。 给定规格 在验证之前，必须提宠设讨或系绞必须瀵足的性藤。这个溉掺逮豢以逻矮公 式鸵形式给出，遴常楚c t l ( c o m p u t a t i o nt r e el o g i c ) 或l t l ( l i n e a rt r e el o g i c ) 公式的形式出现。这聪荦申逻辑公式熊够燃述系绕隧骜对闻变化舱麟性。本文将要 考感恩c t l 公式来表暴系绞要潢足熬趣捂。 验证 在理想黪 冤f 验诞楚完全曩动化灼。键是，在实际中经零霪要有人豹参譬。 耱人工熟活裁憝验 委结聚豹分毒厅。为了游盘番定鑫冬结聚，出缮熬路径经常星巍 给蠲户。窑麓够禳作为溺试震往的反铡并勰帮韵设计者跟踪到出链鹊穗方。在这 6 基于状态转换容侵系统模型的s m v 分析与改进 种情况f ，分析错误路径可能要求修改系统和重写模型检测的算法。 j 一：生错误的路径也可能是因为不正确的系统模拟或是不正确的规格要求。错 误路径能用于发现和修补这两类问题。最后一种可能是验证任务可能会不能i _ f 常 地终止，因为模型规模大到不能装进计算机内存的原因。在这种情况下，可能需要 在更改模型检测器的参数或调整模型后重新验证。 2 2模拟系统 一个状态是系统中的变量在一个特定的时间的一个快照或怒一个现时的描 述。 我稠还需要翔遂系统熬 壹螽箭逮蕊系统静动佟燹纯。可疆遴遭绘定系缓褒动 作发生前和发生后的状态来描述系统的改变。这样的状态对决定了系统状态的迁 移。在这壁，在模拟系统时可以使用k r i p k e 结构来描述系统的行为 1 6 。 一个k r i p k e 结秘密：一令妖态集合，状态之润的迁移关系，一个标号函数 组成。标母函数用一些在这个状态f 为真的命题标识这个状态。路径是一个 k r i p k e 结构在模拟系统汁算的状态系列。虽然这榉的模型非常简单，但它们有 足够的表遮箍力对系统遂行猿理。 下面让我们来看看如何用k r i p k e 结构模拟系统。 假设a p 海一个原孑命题的集合。一个在a p 上躲k r i p k e 结褥鹾是一个四元 组 m = ( s ，s 。，r ，l ) s 是有隈状态集合 s 。是s 的一个子集，它是系统秘贻状态的集合 r 是s s 的一个传递关系，r 必须是完全的，也就是对于每一个s s ，有一 个状态s ，满足r ( s ，s ) l ：s 一 2 ”是一个函数，这个函数撼每一个状态弼在这个状态成立的原子命题 集合标识。 有时我键霹殴不蘑关心拐始状态爽合s 。在这葶孛壤凝下，可以挺这个状态集 合从k r i p k e 结构的定义中删除。在结构m 中，从一个状态s 歼始的一条路径是 7 鏊，状态转换窖餐系统模型的s m v 分析与改进 状态的一个无穷序列 r = s o s i s 2 在这里s o = s 并且r ( s 。，s ，。) 对所有的i o 成立。 2 。3 霆一除公式表示系统 可以便刷一阶公式来描述系统。在这些公式里丽出现的谓词和函数符号将有 了预先绘定瓣定义。逶零，这耱意义获上下文寒番怒缓麓确豹。 假设v 。 v l ，v n 是系统变量的集合。在描述系统时同时假设在v 中的变 最的取值范围是有限集合d 。一个对v 的赋值把在v 中的变量v 联系到d 中的一 令篷。 通过对v 中所有的窝鼙给定毽就熊够积系统的一个状态描述潞来。也就砖说 个状态赣楚个斌 ! 蓬：s ；￥ d 。给定一个斌髓，我们能够写出一个为真的 公式来表示这个斌值。倒懿给定： v = v l ，v 2 ，v 3 和斌 鬣 v l 一2 ，v 2 2 ”鼗霆义藏l ( $ 麓艨有杰s 中为粪夔簸子公式瓣予囊。 如果v 是一个布尔域上的变爨，那么v l ( 8 ) 表示s ( v ) = t r u e ，并尉v 不属于l ( s ) 表示s ( v ) = f a l s e 。 出予要求懿k r i p k e 蓊鞫懿迁移关系总楚完全夔。当状态s 没有后继时宓矮 扩充关系r 。在这种情况下修改r 使r ( s ，s ) 成立。 2 4二进决定圈 遄过符号亿淡示获态转移凿【i 7 】，缀多燹大静系统帮缝鞍验证。灏的符号纯 表示是基于b r y a n t 的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 ) 。o b d d 为布尔 公式掇供了一种标准的表示方式，这种表示方式通常比台取范式或卡厅取范式更紧 凑，褥虽也有非鬻有效的方法对它们进行搽佟。由于符号纯袭示缀紧凑童氇箍述了 凼电路或协议决定的状态空间的规律性，所以有可能验 正状态空间非常大的系 统。 下面播述怎榉掰二迸决定图符号纯的袭示霄# 琵状态系统。首先讨论二进决定 阁怎样被用来液示稚尔函数。布尔函数被定义为在0 和lt 丽，0 代表f a l s e ，t 代表t r u e 。二进决定图的大小跟变量的顺序露很大的关系。使用这种袭达方式 番种逻辑操作能有效的实现。随磁讨论使掰二滋决定图怎样编码k r i p k e 结构， 遮样就能准确的表示搪述的系统了。 2 唾+ l 瘸o b d d 淡示蠢笨公式 有序布尔确定蕊( o b d d ) 怒表示布尔公式的一种标凇。他们通常比传统的合墩 基于状态转换容经系统模型的s m v 分j 扦与改进 范式或橱墩范式更紧凑的多，而且它们搡作起来也嚣常有效。因此它们广泛使瘸 在计算枫辅鼢漫诗的各种应用中，包括信号模拟，缀合逻辑验谨，和最近的一些 应用于有限状态并发系统的验证。 我们露先考虑二进决定树。二遘决定楗是一个有缀蛉，有囱褥，它由两类缀 点组成，终端结点和非终端结点。每一个非终端结点v 被一个变掇v a r ( v ) 标识， 它有两个后继结点：l o w ( v ) 对应变量v 被赋值成为0 的情况，h i g h ( v ) 对应变懋 v 被赋值为l 懿情漫。每一个终端结点v 被表示为v a l u e ( v ) ，v a l u e ( v ) 不是0 裁 是1 。对于一个由公式f ( a l ，a 2 ，b l ，b 2 ) = ( a l h b l ) ( a 2 h b 2 ) 表示的二位比较 器的二进决定树( 如图2 - 1 ) 。 图2 - 1 ( a l b 1 ) f a 2 h b 2 黪= 遴凌定褥 通过从聿霹载摄结点出发爨终端结点我们能够确定一个对变餐瓣特定载囊毽 赋值是否使那个公式为真或为假。如果变蓬v 被赋值为0 ，那么从根结点到终端 臻点翡爨经上豹下一个缭患懑是l o w ( v ) 。磐果v 蔹簸镶受1 黔么路经巴豹下 个缝点撂楚h i g h ( v ) 。标识终溃结点拣篷垮会是这个溪数在这次赋德f 鳃德。溅 如，赋值 邋嶷栋琴为0 戆时予绥点；因此这令公式在这 个赋僮下为假。 二邈决定褥并没有为布尔函数援供菲常简萌豹表示，实际上，它们跟真德表 的大小是网样的。幸运的是，在这样的树鼹通常有许多冗余。例如猩图2 一l 的那 棵树，有八棵报结点标识兔b 2 的子树，但只有三棵予树是不榍同豹。因此，邋 过合并嗣态的予橱，能够缁到布尔公式韵爨简练的表示。合并的结梁是被稼为= ： i o 基于献杰转换褰接系缝攘瓤鹣s m v 分撬与敬进 = i i ： 决定图的有向无环图。更凇确的说，一个：二进决定图撼个有根的有向无环图， 它有髑季申结点，终端结点和j 黪警端结点。像= 进决定树攫的情况一样，每一个非 终端结点v 被标号为一个变餐v a r ( v ) ，育两个后继结点，l o w ( v ) 和h i g h ( v ) 。每 一个终端结点被标号为0 或1 。每个以v 为根的二进决定图决定一个布尔函数 f 。( x “，x 。) ，方式壹 下： 如果v 是个终端结点 ( a ) 如果v a l u e ( v ) = 1 那么f ，( x ”，x 。) = l 。 ( b ) 妻g 果v a l u e v ) = 0 勇s 么f ，( x ，x 。) = o 。 如果v 是一个非终端结点，v a r ( v ) = x 。那么f ，是一个函数 ( x ，x 。) = ( 一x ，a f 。) ( x ，x 。) ) v ( x a f , m h ，) ( x 一，x 。) ) 。 猩实际的应用中想要得到布尔公式的标准农示。这样一种表示必须具有这样 一种性质：两个布尔公式逻辑耀簿当且仅当它们有同态的表示。这个性艨使一些 任务筒化了，铡细捡窿两个公式的相等秘决定一个给定的公式是否可以满足。如 巢两个二进决定圈满足下面的情况，那么两个二进决定图愁陌态：如果存在一个 一对一的函数h ，遮个函数把一个终端结点映射到另个终端结点上，一个非终 端结点映射到另一个非终端绦点上，对于每一个终端结点v ， v a l u e ( v ) = v a t u e ( h ( v ) ) 和对于每一个非终端结点v ，v a t ( v ) = v a r ( h ( v ) ) ， h ( 1 0 w ( v ) ) = 1 0 w ( h ( v ) ) ，并且h ( h i g h ( v ) ) = h i g h ( h ( v ) ) 。 给二进决定树加上两个约柬就可以得到布尔公式的标凇表示。第一个约束： 对于每一条从椴结点到终端结点的路径，变量都以相同的次序出现。第二个约束： 在图中没有圆态秘冗余的结点存程。第一令约柬通过绘标识二进决定霆缝点的变 量一个全序，并魁要求对于撼一个图中的结点u ，如果u 有一个非终端的后继v ， 那么v a t ( u ) v a r ( v ) 。第二个约束通过重复运用三条转换规则达到，这些转换娥 剿并不修改这个隧联表示蛉毒零滠数： 删除重复的终端结点对于一个给定的标号删除至只有一个终端结点，并且 把所有盼到被删除缩点的弧惹定向至那个剩余的结点。 测狳重复懿终溱结点对予蘸个终撩终点u 帮v 有r a g ( h ) = v s r ( v ) ， l o w ( u ) = l o w ) 和h i g h ( u ) = h i g h ( v ) ，那么把u 或v 删除，并把所有的入弧重 定向至另一个结点。 基于状态转换容侵系统挺型麓s m v 分析与改避 删除冗余的测试如果对于非终端的结点v 有l o w ( v ) = h i g h ( v ) ，那么删除v 并蔓重定淘所有潦入孤至l o w ( v ) 。 从二进决定图满足有序这个性质开始，通过不断应用转换规则直到图的大小 不再变小，得到标准形式。b r y a n t 1 8 展示了以一j 神囊底向上方式以一个被称为 “妇约”的程序实现转换规则。这个程序运行静时间与二进决定灏大小成线性荚 系。通过这种方式得到的图称为有序= 进决定图( o b d d ) 。例如，如果对于二位比 较函数使用顺序口l b l a 2 b 2 ，就可以餐到如图2 - 2 的o b d d 。 图2 2 ( a l b 1 ) ( a 2 b 2 ) 的二遴决定燃 磐巢o b d d 被耀予袭示农尔函数瓣挺溅形式，那么梭查两个公式枢等就会被 舰约为检查两个二进决定图怒否同态。相似的，可满足性可以通过检蛮是否与只 懋捂一个被稼号为0 豹终端结点靛o b d d 稿同来薅定。 随后姆麓释怎撵爨o b d d 实褒重簦黪逻辑掇圣挈。怒一些东尔公式中蛉一避参 数x 。限定在常墩b 的这个函数。这个函数由f ix 。 一b 表示，并且满足 f j x ， - b ( x ”，x 。) = f ( x i ”，x h ，b ，x ，x 。) 。 鳃鬃f 被表示藏一令o b d d ，逶过深凄线先遮历f 瓣o b d d ，黢铡fx ； - b 黪o b d d 能够很容易的计算出来。如果结点v 有个指针指向结点w ，并且v a r ( w ) = x 。， 如粟b 楚0 ，把指针两l o w ( w ) 代替，如采b 怒t 孢稽针用h i g h ( w ) 代替。这 群褥到黪潮珂熊不是稼灌形式懿，为了褥弱表示i x 。 - b 鲍o b d d ，对这个图应溺 1 2 基于捩惑转按窖幔系统模型拣s m v 分橱号敬述 规约函数。 对于所有具有巍个参数的十六个逻辑擞 筝，能够缀容易的用表示戏o b d d 的 布尔函数来实观。实际上搽作是两个o b d d 参数的线性笈杂度。有激实现这些操 作的的关键思想是s h a n n o n 扩展。 f = ( 一x a f ! x ； 一0 ) v & a f x ， 一1 ) b r y a n t 为计算所有的1 6 个逻辑操作给定了一个统一的被称为a p p l y 的算 法。骰设率是任惑静其有两个参数麓逻辑操律，f 帮f 为两个布尔瀚数。为了简 化算法的扩展我j i 、j 引入下面的符号： v j nv 分另u 怒0 b d df 着口f 的 良 x m v a r ( v ) 并且x = v a r ( v ) 取决于v 和v 关系的几种情况： 如果v 和v 都是终端结点，那么f * f = v a l u e ( v ) * v a l u e ( v ) 如粟x = x ，郡么使用s h a n n o n 扩震 f * f = ( 一x ( f l x ； 一o 球f i x i 一0 ) ) v ( x a ( f x 、 一1 术f ! x t 1 ) ) 把这 个问题分解成魂个子闻题。这个阀题被遴归的解决。最后就可以褥到的0 b d d 的 板结点将是一个新缝点宵，v a t ( w ) = x ，l o w ( w ) 将是表示( f jx t ( 一0 球f7 | x ； 一0 ) 的 0 b d d ，h i g h ( w ) 将是袭示( f 旧 l 冰f x ； 一1 ) 的o b d d 。 如聚x ( x ，那么f x l 0 = f lx ； l = f ，因为f 并不袄赖予x 。在这雄 情况下s h a n n o n 扩展简化为： f * f = ( 一x a ( f ix i 一o 牢f ) ) v ( x a ( f x 、 一1 冰f ) ) f * f 鲍o b d d 像第二穆情况下一样被递归计算。 如果x s 为把布尔向量映射到状态的函数。出于每个斌傻跫s 中一个状态的编码，袭 示s 的特蔹蕊数是表示值为i 静o b d d 。需要两个布尔变量翡集合，一个表示开 始状态，另1 个表示一个迁移后的状态。如果迁移函数被编码成布尔关系 r ( x ，j ( ) ，粥么r 被表示戏特征函数致。最后，考感映射乙，尽管l ，被定义为扶 状态到原子命题子集的浃射，耙它看成从原子命题副状态子集的映射将更方便。 原子命题p 烧被映射到满足( s ip l ( s ) 的状态的集合。称这些状态的集合l p ； 使鼹像上蘑彤一样的编码我们也能够表示b 。雳这荦孛方式分别表示每个原子命 题。 图2 3 状态迁移圈 为了黼鞠o b d d 怎样能被羽来表示一个k r i p k e 绪构，考虑图2 3 表示静两 个状态的系统。在这种情况下这里有两个变量，a 和b 。引入两个附加的变量，a 剐b 。因此，可以使用含取 a a b a a a b 表示从状态s 1 到s 2 的迁移。整个迁移函数由以下布尔公式蝓定： 妇a b a a a b ) v ( a a b a 8 a b ) v ( a a b a a 八 b ) 在这个公式里有三个析取因为k r i p k e 结构有三个迁移。现在这个公式转化 为一爪0 b d d ，藏霹噬鸯这个迁移关系霉到一个篱沽的裘示。 基于获态转换吝爱系统摸掣黪s m v 分辑与改避 2 5符号模型检测和s m v 符号模型检测楚缓o b d d 为工具、投据不动点理论t 算出潢足时态逻辑描述 的规范的状态聚合。 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 ) 为布尔公式提供了一羊申标准的表 示方式，这； 申表示方式通常比台较范式或祈敦范式更紧凑，丽且也有非常有效的 方法对它们进行操作。由于符号化表示很紧凑地描述了内电路或协议决定的状态 空间的规律性，鼹戳有可能验证状态空闻 # 鬻大的系统。 符号优模螫徐测技术酶鏊本步骤一般分为三步： l + 建立模整，对掰要检验静系统避行籀象，将其攒逐为有穷获态迁移系统。 2 用c t l 表示绘出所要验证的状态迁移系统性质的描述。 3 。在s m v 上检验系统是否满足规范。如聚满足就输出t r u e ，镒则就输出 f a l s e 辩潮辩箍示系统不满是蕊范鹣反铡。 s m v 是在1 9 8 7 年秋天由卡内基一梅隆大学在读博士生m c m i l l a n 研发韵模型检 测系统 1 9 。它的主要思想鼹采用符号模型算法检验系统怒否满足用 e 我( e o 戳p h t a t i 。nt r e el o g i c ) 愈麓时态滋辑攒述熬燕菠。s m v 在复杂电鼹设计 的验证 2 0 、安全协议验证 2 1 中得到了广泛的应用。 用s m v 验证系统时，系统说明嚣用s m v 规定躺语言编程，系统属性部分爝c t l 逻辑袭达。s m v 工作服理图如图2 4 所示。 豳2 4s m v 工作原理圈 2 6c t l 的语法和语义 c t l 公式戆语法： 个c t l 公式由两部分构成，一部分魑路径辍词a ( 对于所有的路径) ，e ( 存 在某些路径) ，努一部分是时态量词x ( 下一个状态) 、f ( 将来的某个状态) 、g ( 所 基于状态转换容侵系统模型的s m v 分析与改进 有状态) 和u ( 直到某个状态) 。路径量词和时态量词不能分开来单独使用。 ( 1 ) 每个原子公式是一个c t l 公式： ( 2 ) 如果f ，g 是c t l 公式，则 ，( f g ) ，正伍e x f , , 爿删，f 倒 是c t l 公式： ( 3 ) 只有有限次应用( 1 ) ，( 2 ) 得到的公式是c t l 公式。 除了定义形成c t l 语言的公式之外，在实际中经常用剑其它c t l 公式，这些 公式可以按下列规则得到： f vg = 一 ， 一1 9 ) ：a f g = 4 ( t r u eu je f g = e ( t r u eu ? a c f = - ，e ( t r u e ，1 ，) ：r g f = 诅( f p u 1 厂) c t l 公式的语义 c t l 公式鹃语义疑鬏据符号状态转投强定义的。符号状态转换黼是一个5 元 缌氍= ( a p ，s ，l ，n ，s 。) ，其中a p 是原子命题的集合，s 是状态f 咚有限集合， l 是以原子命题标记集合的函数，n s s 是转换关系，s o 是初始状态集合。 “计算路径”定义为状态穿列s 。，s 。，s 。，其中对于任一n ( s ，s m ) 为真。 m ，sbp i f f p p ( s ) m ，s 净叫 例，s 降f m ，s 眵f a g 彬，s 巨f m ，s | _ g m ，s i = a x ( f ) o t ( ( s ，f ) r a m ，t i x f ) m ，s 滓e x ( f ) i j 扫t ( ( s ，t ) 仨r m ，t 仁f ) m ，s a f u g ( f ) 阿x ( x = ( s o ，s l ，。) ( s o = s ，3 i ( i o a m ，s i g w e j ( s e r v e r s t a t e = a c t i v e _ a t t a c k ) ) e ：a s s e r tg ( ( s e r v e r s t a t e = a c t i v ea t t a c k ) 一 f ( s e r v e r 。s t a t e = g o o d ) ) d ：a s s e r tg ( ( a t t a c k s t a t o = a t t a c k i n g ) 一 f ( ( a t t a c k s t a t e = s p y i n g ) ( a t t a c k ，s t a t e = p a r t l y s u c c e s s ) ) ) 基于状态转换容缓系统模型翦s m v 分搬萼教避 4 2系统的性质描述 骞侵系统摸型兹系绞擐绞遵过骚务器彝攻击者菠令方嚣亲表瑷出来。 第一个方预是：容侵系统要能对所有的攻击都能够进行处理，也就是容侵系 绫模型对攻毒瓣建蒺完备瞧。 另外一个方面是：根嘏容侵系统模烈的性质，系统要在受到攻击后，能够继 续提供服务，或提供降级服务。 这嚣方甏戆幢矮在骚务器移攻击羲貔模型至表示为： 如果服务器受到了攻击，表明攻击者正在进行攻击。用c t l 表示为： a g ( ( s e r v e r s t a t e = a c t i v e a t t a c k ) 一 ( a t t a c k s t a t e = a t t a e k i n g ) )( 1 ) 要验证模鳖是不是筑够搐述掰有翡竣击粪蘩，露热栗攻击者遗灭竣击状 态时，服务器也耍进入受到攻击状态。用c t l 表示为： a g ( ( a t t a c k s t a t e = a t t a c k i n g ) 一 ( s e r v e r s t a t e = a c t i v e a t t a c k ) ) ( 2 ) 整个c t l 逻辑表达式( 2 ) 懿含义为：在系统横爱静嚣毒静鼹径上，只要 a t t a c k 进入攻击态，那么s e r v e r 就要进入豫到攻击的状态。 对于熬个窑侵系统，如果服务器受到了攻击，鄹么都会转换到正常服务 状态。 a g ( ( s e r v e r s t a t e = a c ti v e a tt a c k ) 一 a f ( s e r v e r s t a t e = g o o d ) ) ( 3 ) 对予玻击者的状态转移图来说，只要攻击者发动了攻击，对予这些攻击， 骚务器采用稿应瓣容侵措施，可以提供竞全服务，或者提供降级服务。 用攻潞者的状态转换模型来表示，所有攻击成功，最后都璎转到部分成 功鲍状态或者c s 状态。用c t l 表示为： a g ( ( a t t a c k s t a t e = a t t a c k i n g ) 一 a f ( ( a t t a c k s t a t e = s p y i n g ) l ( a t t a c k ，s t a t e = p a r t l y _ s u c c e s s ) ) )( 4 ) 所有黢务器豹提供黪级缀务的状态，最后都熬转换裂匆始状态g 。爱玫 壁下状态转换容侵系统模型的s m v 分析与改进 击者的状态转换模型来表示，即为所有攻击部分成功的状态，最后都要 转换到c s 状态。 a g ( ( a t t a c k s t a t e = p a r t l y s u c c e s s ) 一 a f ( a t t a c k s t a t e = s p y i n g ) ) ( 5 ) 4