（计算机软件与理论专业论文）基于spin的网络协议形式化分析与验证.pdf

摘要 随着计算机通信与网络技术的发展，网络协议的稳定性和安全性发挥着越来越重要的作用， 所以对网络协议的研究有重要意义。形式化的方法将成为分析网络协议的重要方法，目前有很多 研究网络协议的理论和方法，比较重要的理论有b a n 逻辑，定理证明和模型检测等，而模型检 测作为形式化分析理论方法中的一种，有着自动化和提供反例等优点，基于此，我们采用形式化 方法和模型检测工具来检测网络协议的漏洞也是很有意义的，从而达到提高网络协议安全性和稳 定性的目的。 本论文首先在介绍网络协议、形式化方法和模型检测工具及其应用的基础上，通过不同的安 装环境对s i p n 工具使用做了介绍，并对形式化描述的几种语言进行比较；其次，介绍了o s p f 路由协议的概念、特性和协议的操作及工作过程，同时采用形式化方法的f s m 分析了o s p f 协 议；接着重点分析了o s p f 网络类型、报文头部、报文处理流程和l s a 处理流程；紧接着通过 s p 玳模璎检测工具对o s p f 协议进行抽象化建模，描述了o s p f 协议的l 1 l 性质，并用x s p i n 模型检测一j ：具进行了检测验证，得到了运行轨迹，在此基础上又采用稳定状态验证的方法从可行 性和止确性等方面验证了o s p f 路由协议；最后总结本文的主要：l 作并对尚需完善的：i ：作进行展 望。 本文采用的主要方法和技术如下： 1 采朋形式化的分析方法，对o s p f 协议分析； 2 s p i n 适墙于并行系统，本文探讨了在w i n d o w s 、j a v a 、c y g w i n 等环境下对s p i n 工具的 安装和使片j ，并详细介绍了s p i n 的图形界面工具x s p i n 的安装过程和功能的使用，并通过a b 协议进行分析、验证，从而得到协议不容易发现错误，模型检测工具的使用作为本文的主要技术 支持。 本文的特色和创新之处在于： 1 采用形式化的方法分析网络协议，并用有限状态系统的描述语言p r o m e l a 对o s p f 协议进 行建模；描述了o s p f 协议的l t l 性质，用x s p i n 模型检测工具进行了检测验证，得到了运行 轨迹： 2 采取稳定状态验证的方法从可行性和正确性等方面验证。 关键词：s p i n ，模型检测，网络协议，o s p f ，p r o m d a ，形式化方法 a b s t r a c t w i t ht h ed e v e l o p m e n to fc o m p u t e rc o m m u n i c a t i o na n dn e t w o r kt e c h n o l o g y , t h es t a b i l i t ya n ds a f e t y o fn e t w o r kp r o t o c o li sp l a y i n gam o r ea n dm o r ei m p o r t a n tr o l e ，s oi ti so fg r e a ts i g n i f i c a n c et or e s e a r c h o nn e t w o r kp r o t o c 0 1 f o r m a lm e t h o d sw i l lb et h ei m p o r t a n tm e t h o dt oa n y l y z et h en e t w o r kp r o t o c 0 1 u p t on o w , t h e r ea l ep l e n to ft h e o r i e sa n dm e t h o d st os t u d yn e t w o r kp r o t o c o l ，a m o n gw h i c hm o r ei m p o r t a n t t h e o r i e sa r eb a nl o g i c ，t h o r e mp r o v i n ga n dm o d e lc h e c k i n g ，e t c t h em o d e lc h e c k i n ga sat h o r e t i c a l m e t h o do ft h ef o r m a la n a l y s i sh a st h ea d v a n t a g eo fa u t o m a t i o na n dp r o v i d i n gc o u n t e r e x a m p l e , e t c a n d b a s e do nt h i s ，w ea d o p tf o r m a lm e t h o da n dt h em o d e lc h e c k i n gt o o l st od e t e c tt h en e t w o r kp r o t o c o l v u l n e r a b i l i t i e s ，w h i c hi sv e r ym 黜l i i l g 凡l ，a n dc a ni m p r o v et h es t a b i l i t ya n ds a f e t yo fn e t w o r kp r o t o c 0 1 t 1 1 i st h e s i sf i r s t l yi n t r o d u c e st h en e t w o r kp r o t o c 0 1 f o r m a l i z e dm e t h o da n dt h em o d e lc h e c k i n g t o o l sa n do nt h eb a s i so fi t sa p p l i c a t i o n ，a n dt h eu s a g eo fs i p nt o o l st h r o u g hd i f f e r e n ti n s t a l l a t i o n e n v i r o n m e n ta n dc o m p a r i s o no ff o r m a l i z a t i o nl a n g u a g e s s e c o n d l y , i ti n t r o d u c e st h ec o n c e p to fo s p f r o u t i n gp r o t o c o l s ，c h a r a c t e r i s t i c sa n do p e r a t i o na n dt h ew o r k i n gp r o c e s so ft h ea g r e e m e n t ，a n d 诵n l f s mf o r m a la n a l y s i sm e t h o dt oa n a l y z et h eo s p et h e na n a l y z e do s p fn e t w o r kt y p e ，m e s s a g e ，h e a d ， m e s s a g ep r o c e s s i n ga n dl s a sp r o c e s s ；t h e ni tc a i t i e so u ta b s t r a c t i o nm o d e l i n gf o ro s p fp r o t o c o l s t h r o u g hs p i nm o d e lc h e c k i n gt o o l s ，d e s c r i b e st h en a t u r eo fo s p fp r o t o c o ll 1 7 l ，x s p i nm o d e l c h e c k i n gt o o l sw e r et e s t e dv e r i f i e db yt h et r a j e c t o r y , b a s e do nt h i sv a l i d a t e so s p fr o u t i n gp r o t o c o l s t h r o u g ht h em e t h o d so ft h es t a b i l i t ys t a t ef r o mt h ea s p e c t so ft h ef e a s i b i l i t ya n dc o r r e c t n e s so ft h et e s t ； f i n a l l y , t h et h e s i ss u m m i z e st h em a i nw o r kd o n ea n ds h o w sp r o s p e c t sf o rt h ew o r kt oi m p r o v e 1 1 1 ep a p e ra d o p t st h em a i nm e t h o d sa n dt e c h n i q u e sa sf o l l o w s ： f i r s t ，i ta n a l y z e st h eo s p fp r o t o c o l sw i t ht h em e t h o do ff o r m a la n a l y s i s s e c o n d ，s p i na p p l i e st op a r a l l e ls y s t e m t h i sp a p e rd i s c u s s e st h ei n s t a l l a t i o na n du s es p i nt o o l si n s u c he n v i r o n m e n tw i n d o w s ，j a v a ，c y g w i n ，e t c 1 1 l ep a p e ri n t r o d u c e st h ei n s t a l l a t i o np r o c e s sa n d f u n c t i o no fu s em o d e lc h e c k i n gt o o l sx s p i ni nd e t a i l ，a n a l y z e sa n dv e r i f i c a t i o nb ya bp r o t o c o lt of i n d t h em i s t a k et h a ti sd i f f i c u l tf o rp r o t o c 0 1 a sw e l la s ，m o d e lt e s t i n gt o o l sa r eu s e da st h em a i nt e c h n i c a l s u p p o r t t h ec h a r a c t e r i s t i c sa n di n n o v a t i o n si nt h ep a p e ra r ea sf o l l o w s ： f i r s t t h ep a p e ra n a l y z e st h en e t w o r kp r o t o c o l s 谢mf o m a lm e t h o da n d c a r r i e so u tm o d e l i n gf o r o s p fu s i n gd e s c r i p t i o nl a n g u a g ep r o m e l ao ff m i t es t a t es y s t e m ，d e s c r i b e st h en a t u r eo fo s p f p r o t o c o l s 【t l x s p i nm o d e lc h e c k i n gt o o l sw e r et e s t e dv e r i f i e db yt h et r a j e c t o r y ； s e c o n d ，t h ep a p e ra d o p t sv a l i d a t e dm e t h o do fs t e a d ys t a t ef r o mt h ea s p e c t so ft h ef e a s i b i l i t ya n d c o r r e c t n e s s k e yw o r d s ：s p i n ，m o d e lc h e c k i i l g ，n e t w o r kp r o t o c o l ，o s p f ，p r o m e l a ，f o r m a lm e t h o d u 独创性声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成 果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发 表或撰写过的研究成果，也不包含为获得宁夏大学或其它教育机构的学位或证书而使 用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的 说明并表示了谢意。 研究生签名：彰砗哮 时间：矽矽年厂月衫日 关于论文使用授权的说明 本人完全了解宁夏大学有关保留、使用学位论文的规定，即：学校有权保留送交 论文的复印件和磁盘，允许论文被查阅和借阅，可以采用影印、缩印或扫描等复制手 段保存、汇编学位论文。同意宁夏大学可以用不同方式在不同媒体上发表、传播学位 论文的全部或部分内容。 ( 保密的学位论文在解密后应遵守此协议) 研究生签名：当蚌埠 时间：少归年罗月“日 导师签名：了意义 时间：2 汐fd 年s 月盈刍 宁夏大学硕十学位论文第一章绪论 1 1 选题背景 第一章绪论弟一早珀t 匕 随着计算机通信与网络技术的发展，协议【啦捌的种类和数量越来越多，其规模也越来越大， 网络协议的复杂性也日益增强，主要从协议开发难度大、周期长、潜在错误多等方面体现出来， 而协议开发过程中任何一点错误和缺陷都将会引起分布系统的稳定性、可靠性、安全性、容错性 和互通性等方面带来危害。网络协议【4 】的主要形式化模型技术有：有限状态机( f s m ) 、p e t r i 网、 时态逻辑、通信进程演算等。典型的网络协议形式语言p l 有：s d l ，e s t e l l e ，p r o m c l a ，l o t o s 等。这些标准语言都建立在严格的形式化数学基础上，为网络协议的定义和描述提供了极大的便 利。主要的形式化验证技术有：模型检验和定理证明。近三十年来，研究“协议工程学”引起了 人们的极大关注与兴趣，现已有很多厂家研制出了支持口v 6 的实验产品，包括o s p f v 3 的实现， o s p f 路由协议是当今使用最为广泛的协议，o s p f 路由协议的安全性一直受到关注，然而，o s p f 安全的相关研究领域涉及多学科多方面知识，包含内容广泛，研究内容广博，所以系统的进行协 议实现和协议验证也成为当今邗常重要的课题。 形式化方法【6 7 】对开发高可信软件具有重要的意义。形式化方法原则上是用数学和逻辑的方法 描述和验证软件或者硬件系统。从描述上说，方面是系统或者程序的描述，另一方面是性质的 描述。从验证方面来讲，主要有两类方法，一种是以逻辑推理为基础，另一种则是以穷尽搜索为 基础。穷尽搜索方法统称为模型检测。模型检测【8 9 】( m o d e lc h e c k i n g ) 是近十年来最成功的自动 验证技术之一，此技术的成功应用归功于有效验证工具的开发和支持。 s p i n 1 0 ，川( s i m p l ep r o m e l ai i l t 删神是适合于并行系统 1 2 , 1 3 1 ，也是一种著名的分析验证并发 系统逻辑一致性的工具，是一个基于计算机科学的“形式化方法”，有良好的算法设计和非凡的 检测能力，将先进的理论验证方法应用于大型复杂的软件系统当中，s p 玳现在被广泛应用于：l ： 业界和学术界，目前没有用s p n 检测工具对o s p f 路由协议进行分析和验证。 1 2 研究历史及国内外研究现状 o s p f 是一种链路状态路由选择协议，该协议也称最短路径优先协议或分布式数据库协议。 第一个链路状态路由选择协议在a r p a 网的报文分组交换网络中使用和发展。这个协议成为所有 其它链路状态协议的起始点。o s p f 使用著名的d i j k s t r a 算法。o s p f 协议的发展经过儿个r f c ， 最初是j o h nt m o y 和o s p f 工作组在1 9 8 9 年1 0 月以r f c l l 3 1 公布的o s p f 版本l 填补了这项 空白，这个版本体现在r f c l 2 4 7 文档中：现在使用r f c 2 3 2 8 描述基于i p v 4 的o s p f 协议版本2 ； 砒c 2 7 4 0 ( 即o s p f 协议版本3 ) 修改了基于m v 4 的o s p f 以支持i p v 6 下的路由选择信息的交换， o s p f v 3 仍然在不断的完善中，而本文就是利用s p i n 模裂检测r ：具在w i n d o w sx p 操作系统下对 宁夏大学硕卜学位论文第一章绪论 皇皇曼曼曼曼舅! 量曼曼曼曼曼曼曼葛曼曼曼曼蔓曼曼曼曼曼曼曼曼曼曼曼曼曼鼍曼鼍i ii_i i m ii i i i i i i ii 曼曼曼曼曼皇曼曼曼曼曼璺 o s p f 路由协议进行分析、验证。 模型检测是最成功的自动验证技术之一，是验证有限状态并发系统的自动化技术。它的操作 过程是在协议的基础上首先建立模型，然后用形式化方法描述系统应拥有的性质，并建立性质的 逻辑表达式，最后通过遍历模型上的所有可达状态，判断系统是否拥有了所期望的性质。现在模 型检测已经应用于复杂软件系统的开发过程，在开发早期发现和纠正错误。c l a r k e 、e m e r s o n 等 在2 0 世纪8 0 年代初提出了运用分支时态逻辑进行模型检测的研究。目前在模型检测方面，国内 外已做出大量工作 1 4 , 1 5 j6 】。模型检测已经被成功地应用于分析与验证计算机硬件、通信协议、网 络协议、控制系统、安全协议等。模型检测面临的挑战是状态空间爆炸问题【1 8 1 。然而模型检测 的工具很多，如：验证实时系统i l9 】的u p p a a l ，验证并发系统的s p 玳等。 s p i n 是由贝尔实验室的形式化方法与验证小组于1 9 8 0 年开始开发的p a n 是现在s p i n 的前 身。1 9 8 9 年s p i n 的0 版本推出主要用于检测一系列的一r e g u l a r 属性。1 9 9 5 年偏序简约和线性 时态逻辑转换的引入使得s p i n 的功能进一步扩大。2 0 0 1 年推出的s p 烈4 0 版本支持c 代码的植 入，应用的灵活性进一步增强。随后2 0 0 3 年推出的s p n l 4 1 版本加入了深度优先搜索算法，2 0 0 9 年连续推出s p 玳5 2 版本，这使得s p 的发展又上一个新台阶。n a s a 使用s p 烈检测在1 9 9 6 年火星探测者所存在的错误，结果发现一些错误是可以在发射之前就可以被改正的。s p i n 从此 就被用来检测土星火箭控制软件和一些应用与外层空间的程序。因s p i n 有良好的算法设计和1 # 凡的检测能力，得到了a c m ( a s s o c i a t i o nf o rc o m p u t i n gm a c h i n e r y ) ( 世界最早的专业计算机协会) 的认可，在2 0 0 1 年授予s p i n 的开发者h o l 力n a n n 享有声望的软件系统奖。迄今为止s p i n 也是 唯一获得a c m 软件系统奖的模型检测： 具。世界最早的专业计算机协会的c e oj o h nr w h i t e 说 道：“g e r a r dh o l z m a n n 的s p i n 系统有着非常聪明的查找技术，因为它不但可以在有限的内存空 间中快速的对软件进行检测，而且它可以保证程序在按照它们原有的工作方式下被检测。” 在国内模型检验方法使用状态空间搜索的办法米全自动地检验一个有穷状态系统是否满足 其设计规范。该方法的优点在于它有全自动化的检测过程且验证速度快、效率高，并且如果一个 性质不满足，它能给出这个性质不满足的理由，据此可对系统描述进行改进。模型检测方法已经 用于对在安全电子商务协议和安全认证协议的分卡斤【2 0 , 2 1 , 2 2 1 。由于s m v t 2 3 2 4 1 e 身的特点，在参考文 献【2 5 j 中不可避免的出现了状态空间爆炸问题；在参考文献【2 6 】中，作者虽然根据协调性原理提出了 一种适用于多主体参加的认证协议的数据结构。 在国外用s p i n 检测_ 丁具旧己经验证的协议有：滑动窗口协议，路由器协议【2 8 】，x 5 0 9 认证 协议，w a p 传输层协议【2 引。n a s a m 厂v 17 软件研究实验室利用s p i n 验证了一个航天容错控制软 件，形式化验证发现了3 个异常。 1 3 选题的意义和目的 今天，p v 6 协议及相关的协议族是下代网络的主导技术，它已经得到了i n t e r n e t 路由器和 主机厂商的广泛承认。o s p f 是一种使增非常广泛的典型的链路状态的路由协议，o s p f v 3 是支持 i p v 6 的o s p f 版本。目前已经有很多厂家研制出了支持i p v 6 的实验产品，包括o s p f v 3 的实现， 然而，p v 6 协议的实现到真正能够成为互联网的主流协议，还需要经过漫长的过程。o s p f 使川 2 宁夏大学硕l ：学位论文第一章绪论 曼i i _ 一_ 一i i i i 一 i n 。； ibm_i i 。皇曼曼皇曼曼曼曼曼曼鼍量 广泛的路由协议，实现的正确性对于口v 6 成为i n t e m e t 的主流协议有着重要的意义。 s p i n 是协议一致性的辅助分析验证工具，以p r o m e l a 为输入语言，可以对网络协议设计中规 格的逻辑一致性进行检验，并报告系统中所出现的死锁、未规定的接收、标记不完全等情况。所 以通过用模型检验工具s p i n 可以有效，并安全的分析和检验o s p f 协议中存在的一些问题，有 一定的研究意义。 用形式化的方法来描述与验证o s p f 协议可以发现网络协议中潜在的错误。形式化地描述和 验证网络协议是整个网络协议设计与实现的基础，对网络协议实现的正确性、完整性和复杂度有 重要的影响。形式化的方法有牢固的数学基础，比一般的软件工程的方法更严格，它使整个网络 协议开发或验证过程一体化和系统化。 1 4 本文工作 本文用形式化的方法对o s p f 路由协议分析，并采用有限状态机对o s p f 协议进行分析，用 模型检验r 具s p i n 对o s p f 路由协议进行建模、属性描述和验证。模型检验能够自动地进行， 当系统模型不满足系统要求时，模型检验器会自动生成不满足系统规格的反例，告诉我们如何进 一步修改模型以满足所需求的属性。本文j i ：作主要从以下几方面来论述： ( 1 )阐述国内外现有的网络协议形式化方法分析和验证的研究现状； ( 2 ) 形式化发展论述，同时采用形式化的有限状态机( f s m ) 方法，对o s p f 协议分析； ( 3 ) s p i n 适用于并行系统，本文探讨了在w i n d o w s 、j a v a 、c y g w i n 等环境下对s p 工具 的安装和使用，并详细介绍了s p i n 的图形界面工具x s p 烈的安装过程和功能的使用，分析了 s p i n 工具的原理，并通过a b 协议进行分析、验证，从而得到协议不容易发现错误； ( 4 ) 利用s p i n 有限状态系统的描述语言p r o m c l a 对o s p f 协议进行建模、属性描述和验证， 并采取稳定状态验证的方法从可行性和正确性等方面验证。 1 5 论文结构 本文共五章，其组织结构如下： 第一章介绍了论文的选题背景和研究历史，展现了国内外对s p 玳模型检测i ：具和网络协议 的研究现状，从而体现出本文的研究意义和目的。 第二章介绍网络协议概念和基本要素的基础上；接着描述了网络协议开发过程的六个阶段， 同时将形式化方法应用到开发的各个阶段，得知网络协议的关键性和重要性；通过介绍形式化方 法的发展、概念、形式化方法的软件开发和形式化描述的好处，进一步为第三章的形式化语言比 较和第四章网络协议形式化分析作铺垫。 第三章首先从模型检测的概述、主要技术、应用和常用模型检测j ：月：做了介绍，并对模型检 测：刊尽的比较和形式化描述的几种语言进行分析，进一步体现出本论文使用s p i n 模型检测i ：具 的特点；接着剖析了s p i n 工具的原理，重点介绍s p i n 的图形界面。i ：具x s p i n 的使用过程，通 3 宁夏大学硕 j 学位论文第一章绪论 过例子展现了x s p i n 的功能，最后用p r o m e l a 语言对a b 协议抽象建模，并在c y g w m 和x s p i n 环境下用s p i n 进行a b 协议模型检测，得到a b 协议的3 0 个不同的全局系统状态存储，有4 1 个状态在搜索中遍历过，运行发现一个错误并得到反例，本章在论文的整体结构中起到了承上起 下的作用。 第四章是论文的核心，首先介绍了o s p f 路由协议的概念、特性、协议的操作和协议工作过 程后；其次用形式化的方法分析了o s p f 协议；接着从o s p f 网络类型、报文头部、报文处理流 程和l s a 处理流程方面分析了o s p f 路由协议；用s p i n p r o m e l a 把o s p f 协议抽象化建模，描 述了o s p f 协议的l t l 性质，并用x s p n 模型检测工具进行了检测验证，得到了运行轨迹，在 此基础上又采用稳定状态验证的方法从可行性和正确性等方面验证了o s p f 路由协议；最后我们 对o s p f 协议建模和验证的结果分析出o s p f 协议所潜在的不安全隐患，并提出用积极主动防护 和检测机制来增加o s p f 协议安全。 第五章对本文的研究工作进行总结和回顾，并指出未来的进一步工作和尚需完善的研究。 4 宁夏人学硕f 学位论文 第二章网络协议和形式化方法 2 1 网络协议 第二章网络协议和形式化方法 2 1 1 网络协议的定义 网络协议 3 0 , j 1 】是网络上所有设备( 网络服务器、路由器、防火墙等) 之间通信规则的集合， 它规定了通信时信息必须采用的格式和这些格式的意义。计算机间数据通信的高度自动化，对网 络协议的功能和性能都提出了非常高的要求。从功能方面来看，网络协议是为进行计算机网络的 数据交换而建立的一系列规则、标准或约定。一种语言和一种标准也是网络协议定义的两种观点。 英国国家物理实验室的r as c a n t l e b u r y 和k a b a r t l e t t 于1 9 6 7 年4 月，在数据通信中首次用 到“协议”这一术语。他们认为：协议是关于分布式系统进行信息交换时的一种约定，协议应该 按照语言的方式进行定义。网络协议就是具有规定文法、语法和语义的语言，其中，文法给出了 有效信息的精确格式，语法描述了数据交换的规则，语义规定了可交换信息的词汇及其含义。 随着标准化网络的发展和广泛使用，人们越米越体会到标准化为计算机之间的数据通信所带 来的便利。网络协议的标准化也随之推到前台。当前j 许多人认为，网络协议就是数据通信的标 准化。为此，出现了数据通信协议的许多标准，协议标准化并不能解决协议设计自身存在的问题， 冈此设计的协议需要有完备性和无错误性判定。 2 1 2 网络协议的基本要素 为了确保计算机网络中数据通信的顺利进行，一个完整的网络协议应该包括五个基本要素： 协议所提供的服务；协议运行环境的假设；实现协议的消息词汇；对该词汇中每个消息的编码； 一致性的过程规则。 我们使用非形式化的描述对网络协议的五个基本要素加以说明。在以后的分析中，指出在设 计中经常可能隐藏的一些错误。由w c l y n c h 于1 9 6 8 年提出的一个点到点的文件传送协议，在 该文件传送的过程中只牵涉到一个发送端和一个接收端。下面将对五个基本要素进行介绍： 1 服务的说明：这个协议的目的是通过电话线以字符序列的形式传输文本文件，传送过程中 要防止传输错误，协议被定义为以全双工方式进行文件传输。在从a 剑b 传送消息后，对该消 息的肯定或否定性确认信号将通过自b 向a 的通道传送。每个消息包括两个部分：数据部分以 及用米在反向通道上传送的控制部分。 2 环境的假没：协议执行的环境主要由两部分组成：参与文件传送的两个用户和传输通道。 其中，假设用户仅仅是简单地提交一个文件传送申请，然后便等待该传送的结束，并假设传输通 道可能会引起任意的消息失真，但不会发生消息丢尖、消息增加、消息重排等情况。同时，我们 假设有一个低层的模型可用米检测出所有的消息失真，并将失真的消息转换成“e r r ”类型的消息。 3 协议的词汇：协议词汇定义了三种不同类别的消息：“a c k ”是加入了肯定确认信号的消息； 5 宁夏大学硕 ：学位论文第一一章网络协议和形式化方法 “n a t ：”是加入了否定性确认信号的消息；“e r r ”是存在传输错误的消息。我们将协议词汇简明地 表示成一个集合如下： v = a c k ，n a k ，e r r 4 消息的编码格式：每一个消息由两部分组成：控制字段和数据字段。其中，控制字段用来 区分消息的类型，数据字段是所传送字符的代码。在本例中，假设数据字段和控制字段的长度是 固定的。现在将每个消息的一般形式表示成一个简单的具有两个字段的结构： c o n t r o lt a g ，d a t a 采用类c 语言，可将其更详细地描述如下： e l l u l n c o n t r o l a c k ，n a k ，e f r s t r u c t m e s s a g e e l l u i nc o n t r o l t a g ； u n s i g n e dc h a rd a t a ； ； 其中，以关键字e n u m 开始的这一行说明了一个名为c o n t r o l 的枚举类型，它有三个可能的取 值，每个消息有且仅有其中的一种。消息结构自身包含两个域：一个是c o n t r o l 类型的t a g 域，另 一个是声明为无符号字符型的d a t a 域。 5 过程规则：该协议的过程规则可以非形式化地描述如下：如果接收端当前收到的信号是正 确的，则在反向通道里为将要传送的下一个消息加上一个“肯定”确认信号：如果刚收剑的信号 是错误的，则在该反馈的消息里加上一个“否定”确认信号。如果发送端当前收剑的信号里携带 有“否定”确认信号，说明对方刚收到的信号出现错误，则重传上一次的消息：否则取出下一个 消息并发送。如图2 1 的简单流程图描述l y n c h 的简单文件传送协议。 图2 ll y n c h 的简单文件传送1 办议 在上图中，椭圆形表示一种状态。标有“r e c e i v e ”的框表示止在等待从通道传米的新消息。 根据所收剑的消息的不同类型，可从三条执行路径中选择一条。输入数据存储在变量“i ”中，有 凹缺的框表示对与标号相匹配的消息进行确认。而凸出的框则表示传送相应类型的消息。标有 “n e x t ：o ”的框表示一个内部操作，该操作取出将要传送的f 一个数据项，并将数据项存储在变 量“o ”里，用于输出操作。例如，“a c k ：o ”表示传送数据项“o ”，并且在该数据项“o ”中己 6 宁夏大学硕l ：学位论文第二章网络协 义和形式化方法 经填入了对刚收到的信号的肯定性确认消息。而“n a l 【：”表示传送数据项“0 ”，并且在该数据项 “0 ”中填入了对刚收到的信号的否定性确认消息。 2 i 3 简单协议的分析 在上面这些描述中还有一些问题需要加以考虑，该简单文件传送协议存在着两个问题： 1 文件传送只是在一个方向上进行，也只有在两个方向的数据传输交替发生的情况下才能完 成，在某一端没有实际数据需要传输时，采用“消息填充”的办法。 2 如何判断数据传送的开始和结束。在过程规则中我们已经规定了一般的数据传送过 程，但没有规定用来建立和终止数据传送的过程。让通信的一端传送一个假的“错误消息”， 以此来建立起数据传送。如果允许通信双方都采用这种方式来开始数据传送，则很难将两端的 程序同步起来。 该协议中还存在的另外一个严重的缺陷是在协议规定中遗漏了一个基本的操作。即当接收 端在正确地接收到一个数据项并暂时存储在变量“i ”中时，它如何判断自己是否应该接收这个数 据项。当再次正确接收到的消息是对先前已经接收到的消息的重传时，接收端是不应该再次接 收的。如果仅仅依靠上面的两个过程规则，这个问题就不能得到解决。 我们用该协议进行消息传送。有两端a 和b ，假没a 希望向b 传送从a 到z 的字符，而b 以相反的顺序向a 传送从z 至l j a 的字符。它们在自己所传送的字符中加上对上一个所收剑的 字符的肯定或否定确认消息，以作为向对方的应答。当某端所收到的消息带有a c k 或n a k 信号时， 说明收到的字符正确，则将其接收下，并在下一个数据中加上a c k 信号；当收剑的消息为e l l 时，说明收到的字符错误，则将其丢弃，并在下一个数据中加上n a k 信号。这个协议会出现接收 重复数据的问题。如：在执行下面的序列时就导致了这种问题。 首先，a 端通过故意传送一个错误消息- 至 i b ，建立起数据传输。从图2 - 2 所示的事件序列图看 出数据的传输过程。图中的两根实线表示两个程序执行的时间轨迹，点线表示成功的消息传送， 虚线表示出现了错误消息。 a c c e p t ”z ” a c c e p t ”z 图2 2 事件序列图 在上图消息传送中，有两个消息被更改了：从a 至i j b 的肯定性确认消息和从b 至i j a 的否定 性确认消息。在上图中传送序列的最后，当a 收到从b 发来的最后一个消息时，它不能判断这 是一个新的消息，或者仅是对已经传送过的消息进行重传。关键原冈在于a 端发出消息a c k “a ” 7 宁夏大学硕l j 学位论丈第二章网络协议和形式化方法 后，接连出现了两次错误，变成了n a k “a ”，从而导致了b 端再次传送字符“z ”。最终，a 错 误地接收了重传的消息。 尽管这个例子很简单，但是要想发现刚才的错误很不容易。因为，在设计和分析过程中通过 手工分析难以发现问题，它只有在两个错误相继发生的这种概率极小的情况下才会出现。如果 仅仅从上面扩充后的描述来看，很少有人会怀疑协议的正确性。这个协议的确是不完整的，任何 对该协议的简单运用都会在数据交换过程中存在轻微错误。 2 2 网络协议开发过程 网络协议的开发也必须经过系统开发的设计、分析、测试、维护等阶段。网络协议的开发 过程可由图2 3 所示的流程图表示，主要包括：协议设计、协议描述、协议验证与性能分析、 协议实现、协议测试、协议维护共六个阶段。在实际开发中，这些阶段往往是多次反复进行。 下面将对各个阶段进行介绍： 1 协议设计：协议的开发过程就是协议设计过程，一个协议只有经过实现、运行、测试， 证明是正确的、可用的，才算完成了没i ；任务( 图2 3 的全部过程) ；也可以说协议经过严格验证和 性能分析之后就已完成了设计任务( 图2 3 的前半部过程) ；还可以说，非形式描述文本提出后就 已完成了设计任务。无论哪种含义的协议没计，都涉及两个共同的技术问题：环境分析和协议 设计。基于分层结构，一个网络协议可以抽象为n 层结构系统。那么，n 层全局系统就是n 层协议的 设计环境，而n 层环境的分析包括的内容为：n 层实体实现哪些功能，总体结构对它提出什么样的 要求；它向n + l 层实体提供什么服务；n 1 层的全局系统映射成通道系统，那么这个通道系统有 什么特性；n 层包括多少实体，它们采取什么工作方式。 i 非形式化规格l l 一 一 i 一一_ j t 转换系统 图2 3 网络协议的开发过程 环境分析是没计的基础，好的协议设计方法是提高协议设计质鼙和效率的保证。协议设计是 有其自身的一些特殊性。协议是一种宝贵的知识，协议设计者凭着白己的智慧和经验已设计了许 8 宁夏犬学硕l j 学位论文第二章网络协议和形式化方法 多高性能的协议，这些协议的积累为更复杂、更高性能的协议设计提供了基础。 2 协议描述：对所设计的协议，一般可以采用三种语言来描述：自然语言、程序设计语言 和形式描述语言。用自然语言来描述协议时，表达能力强，可读性较好，但描述不准确，存在二 义性。用程序设计语言来描述时，便于协议的实现，但可读性差、能力较差。形式描述语言有 严格的语法和语义定义，避免了不明确的问题，可以更准确、更简明地描述系统特征。 3 协议验证与性能分析：协议验证的目的是在协议开发的早期最大限度地检测和纠正协议错 误和缺陷，包括避免死锁、活锁、不可执行的行为、协议外部性能不符合服务要求等问题。协议 验证有非形式验证和形式验证两种。非形式验证往往是基于人工经验，缺乏数学的严密性和科学 性，当然就很难保证验证结果的质量；形式化验证则克服了这些局限性。协议性能分析旨在 改善协议机制，提高执行效率，可基于经验分析、数学分析方法和模拟方法来进行。 4 协议实现：协议不是针对某种机器而设计的，协议实现者总要处理许多协议未说明的技 术问题。目前人们主要在协议实现的半自动化技术上，因为协议实现的完全自动化几乎是不可 能的。这种技术将协议的实现分为两步：第一步利j h j 翻译程序将协议的形式描述文本变成程序 设计语言的与机器无关的源代码，第二步处理协议未说明的技术问题，用手t 编写余下的代码。 5 协议测试：网络协议的测试包括四个方面：一致性测试、性能测试、互操作测试、坚固 性测试。其中，一致性测试是在检测所实现的协议实体与协议规格的符合程度；性能测试是在 检测协议实体或系统的性能指标；互操作测试是在同一类协议的不同实现版本之间互通的能力 和互操作能力；坚同性测试是在检测协议实体或系统在各种恶劣环境下运行的能力。 6 协议维护：是指对己运行的协议的修改、补充等，因此协议的维护可能包含有协议设计、 协议验证和分析、协议测试，以及协议实现等多项任务。在协议设计中经常造成两类错误，设计 了一套不完整的规则，或设计的规则存在冲突。协议的不完善或不完整，将导致整个系统的瘫痪。 随着计算机网络和分布式计算机系统的发展，网络协议的规模和复杂性也在不断增加，对 网络协议的功能和性能提出了更多和更高的要求。协议开发者所面临的基本问题是如何设计一套 庞人的通信控制规则，并且保证信息交换能够逻辑一致、完整、高效地进行。为了更好地解决协 议设计的问题，我们采用“形式化方法”。“形式化方法”主要是指使用形式描述语言来对协议进 行描述，并贯穿协议开发的各个阶段。网络协议的形式化模型技术不仅是形式描述语言的数学基 础，同时也是网络协议的形式分析、验证、测试、综合以及自动化实现的基础。网络协议的形 式化分析和验证，可以严密、科学地完成性能和行为的校验和评判，进而最人限度地确保网络协 议的质量。形式化方法将在卜一节详细介绍。 2 3 形式化方法 2 3 1 形式化方法的发展 形式化方法的研究源于d i j k s t r a 和h o a r e 对程序验证以及s c o t t 、s t r a t c h e y 等人对程序语义的 研究，一般认为形式化方法是始于2 0 世纪6 0 年代木的f l o y d 、h o a r e 和m a n n a 等在计算机程 序正确性证明方面的研究。2 0 世纪8 0 年代末，在计算机硬件设计领域形式化方法在一i ：业界应用 9 宁夏大学硕f j 学位论文第二牵网络协议和形式化方法 曼曼曼曼曼曼皇曼曼曼曼曼曼曼曼曼曼曼曼曼曼曼皇曼曼曼曼曼曼曼曼曼曼曼曼曼曼曼曼鼍, ： _ - - i - 皇皇 取得的成果，掀起了形式化方法的学术研究和工业应用的热潮，并建立了许多较为成熟并进入应 用的形式化方法相关理论、方法和技术。从2 0 世纪9 0 年代开始，计算机学科中工程化方法和形 式化方法的教育引起了欧美计算机教育界的高度重视和关注。在2 0 世纪9 0 年代中期，美国开展 了形式化方法教育研究，并在美国顶尖的3 5 所大学的计算机学科实施了教育实践。难e e c s 和 a c m 联合任务组于2 0 0 4 年5 月提交了计算教程软件工程分册报告，“软件工程的形式化方法” 被列为一门核心课程。计算教程软件工程分册 3 2 , 3 3 1 最终报告的推出对计算机学科相关专业的形式 化方法教育产生了重要的影响 3 4 1 。欧洲形式化方法协会于2 0 0 1 年成立了专门的形式化方法教育 研究分会，并于2 0 0 4 年1 1 月发布了对欧洲1 1 个国家、5 8 所高等院校中的1 1 7 门形式化方法教 育相关课程的调研报掣 j 引。 形式化方法的关键在于形式化的规格说明语言。使用形式化的规格说明语言描述系统及其性 能，可以帮助开发人员获得对所描述系统的深刻理解，有助于发现需求中隐含的不一致性、二义 性、不完整性，在早期发现设计中的错误和缺陷。近年来人们研制出多种形式化语言和半形式化 的规格说明语言用以对系统的状态和行为进行描述和验证，如i o r o s 、b 语言、统一建模型语 言u m l ，并对形式化语言之间的相互转换进行了研究，从而能够对系统的需求给出更深入精确 的形式描述和验证。 许多形式化方法学家研究了形式化方法存在的问题及其发展趋势，指出形式化方法不是万能 的，当前的形式化研究和实践水平还远远没有发挥出形式化方法应有的潜力。它存在一定的弊端： 一方面，现有的形式化技术还不