[2017年整理]5 协议验证技术 (ok)

《[2017年整理]5 协议验证技术 (ok)》由会员分享，可在线阅读，更多相关《[2017年整理]5 协议验证技术 (ok)（53页珍藏版）》请在金锄头文库上搜索。

1、第五章 协议验证（分析）技术5.1 概述对协议本身的逻辑正确性进行校验的过程称之为协议验证 （protocol verification）. 协议验证有两种途径： （1）协议分析（protocol analysis） （2）协议综合（protocol synthesis）通常所说的协议验证指的是前者。协议综合（将在第六章 讨论）将协议设计过程和协议验证(分析)过程融合在一起，它通 过一组能确保所设计的协议是正确的规则，从一些基本协议模 块中（这些基本模块已证明是正确的）产生所希望的目标协议 。协议分析的目的是：对已设计的协议进行分析和校验（这 些已设计的协议大都是采用非形式化设计方法产生的 ）

2、第五章 协议验证技术协议分析包括许多方法，例如， （1）可达性分析（reachability analysis） （2）不变性分析（invariance analysis） （3）等价性分析（equivalence analysis） （4）符号执行（symbol execution）、模拟（simulation）等等。 这些分析工作可以手动完成。协议有多种表达形式，这包括：用自然语言描述的非形式化协议文本 ；用形式描述语言（ESTELLE，LOTOS,SDL等）描述的协议规范；用协 议模型技术（FSM，Petrinet，CCS等）表达的协议模型；以及用程序设计 语言（C，Pascal等）描述

3、的协议代码。协议分析可在任何一种表达形式上 进行，一般地说，上述所有方法都可在这几种表达形式上进行（手工或软 件工具）。然而，除符号执行之外，人们都在协议模型上进行协议分析（ 简单，容易形成确定算法）。 本章讨论三种分析方法，它们是可达性分析、不变性分析和等价分析。第五章 协议验证技术5.2 可达性分析 可达性分析（基于FSM模型技术）试图产生和检查协议所有 或部分可达状态。所谓可达状态指协议从初始状态开始经历 有限次转换之后可达到的状态，所有可达状态构成可达图（ reachability graph）.可达性分析的最重要工作是产生和检查 可达图，判定是否存在死锁，活锁等协议错误。可达性分析

4、涉及三个重要技术： （1）怎样找到所有可达状态，构成可达图； （2）怎样检测死锁、活锁等协议错误； （3）怎样解决状态爆炸问题。第五章 协议验证技术5.2.1 穷尽可达性分析穷尽（exhaustive）可达性分析产生和检查 所有协议状态。算法5.1描述了穷尽可达性分析 的基本算法，该算法假定计算机的存储空间足 够大，计算速度足够高。 第五章 协议验证技术算法5.1：exhaustive reachability analysis start() W=initial state;/工作集；将被分析的状态 A=;/被分析过的状态 analyze();/穷尽分析 analyze() if (W= =

5、empty) return; q=last element from W;集合W包含未被分析的协议状态，A包含已分析和正在分析中的协议状态 , 算法执行之前，W包含initial state, A为空，算法执行完毕之后,W为空，A包 含协议的所有可达状态。该算法简单明了，然而要将它付诸实施时,我们还必 须解决以下一些问题。add q to A; find all successors s of q; if (q= =error_state) report_error(); else for each successor state s of qif (s is not in A or W)ad

6、d s to W;analyze();delete q from W; 第五章 协议验证技术1.状态表示方法 协议状态用状态矩阵表示为:这里E1，E2，En，为n层协议的几个协议实体的局部状态， Cij为协议实体i到协议实体j的通道的状态。当所有通道可处 理成空通道时，协议状态可用数组E1,E2,En表示（因为 空通道只有一种状态）。第五章 协议验证技术2.怎样找到所有可达的后继状态不考虑报文顺序号，AB协议系统如图5.1所示，其中C12是S到R的通道 ， C21是R到S的通道，协议状态由二维矩阵组成。初始状态有四个后继状 态：很显然，状态（2），（3）和（4）不是可达 状态(因为初始状态中A

7、B内部没有任何数据需 要传输，所以（2），（3），（4）状态是不 可能出现的，即不可达的)。那么怎样判定（1）是可达状态，而（2）， （3）和（4）不是可达状态呢？第五章 协议验证技术图5-1 AB协议系统第五章 协议验证技术为了解决这个问题，我们按下述格式定义交互事件：entity(state):actionpoint(state)?/!message 这里，entity(state)表示协议实体处于状态state中， action point(state)表示作用点处于状态state中，！表 示发送，？表示接收。作用点的状态定义为“0”或“1” 。发送（！）结束后，状态为“1”；接收（？）

8、结束 后，状态为“0”。AB协议系统有四个作用点，它们是 用户和S之间接口A，用户和R之间接口B，S和通道之 间接口a以及R和通道之间接口b。利用上述的事件表 达格式，图5.1的事件表述如下：第五章 协议验证技术(7)R(1):b(0)!ack (8) R(1):B(0)!m (9)C12(0):a(1)?m (10)C12(1):drop (11)C12(1):b(0)!m (12)C21(0):b(1)?ack (13)C21(1):a(0)!ack第五章 协议验证技术现在，我们就很容易判定初始状态下，事件（l ）可执行，而事件（5 ）、（9 ）和（12 ）不会执行 ，这是因为初始化后，作

9、用点状态分别是：A =l , b =0 , a =0 , b =0 利用作用点状态判定在协议状态q 之下，哪些事件会被执行，那么我们就可以找出q 的 所有后继状态 第五章 协议验证技术3 改进方法去掉内部作用状态，而根据通道状态来判定哪些事件会 被执行，将使算法变得简洁用这种方法时，外部作用点保 留，通道内的事件隐藏起来AB 协议系统的事件简化为： （1）S(0):A(1)?m (5) R(0):C12(1)?m （2） S(1):C12(0)!m (6) R(1):drop （3） S(2):timeout (7) R(1):C21(0)!ack （4） S(2):C21(1)?ack (8

10、) R(1):B(0)!m通道内的事件无需表示出来，通道C12 的drop 事件叠加 到事件（6 ）中第五章 协议验证技术如果通道为队列通道，它的状态定义就 会变得复杂，状态数也会激剧增加，事件的 表述方法也变得复杂。例如，对于边界为n 的队列通道，事件表述形式可能为： entity(state):channel(state（参见第三章3.2节）， 定义S*S为状态映射集合，例如，一个包括三个状 态S0、S1和S2的FSM，S*S包括九种映射：（S0 ，S0 ），（S1 ，S1），（S2 ，S2），（S0 ，S1）（ S2 ，S1）。下面研究一种特殊映射互拟关系。 如果两个状态pS，qS能够互

11、相模拟，那么（ p,q）为互拟关系（bisimulation relation）。互拟关 系分强互拟关系（strong bisimulation relation）和弱 互拟关系（weak bisimulation relation）4，13，它 们的定义如下： 1 强状态互拟关系：第五章 协议验证技术第五章 协议验证技术图 5.4 强互拟关系因为（2， 4）均为终止状态， （5， 5）、（3， 3）为相同状态aa第五章 协议验证技术第五章 协议验证技术图5.4和图5.5所示的例子中，我们可以得出这样 的一个结论，即强互拟关系和弱互拟关系的差别在 于后者忽略了内部事件。两个状态为强互拟关系就

12、一定为弱互拟关系，反之不然。一个FSM中所有强 状态互拟关系的集合为FSM的强互拟关系RS，RS是 S*S的一个子集。一个FSM中所有弱状态互拟关系的 集合为FSM的弱互拟关系RW，RW是S*S的一个子集 ，并且RW大于RS。图5.4所示的FSM的RW等于RS，图 5.5的RS=（1,1）,（2,2）,（3,3）,（4,4）,（5,5） ），而RW=RS+（2,3）。第五章 协议验证技术互拟关系（特别是弱互拟关系）有两种重要应用 ，一是FSM的简化，二是两个FSM的等价性比较（ 即等价性分析）。 1 FSM的简化如果（p,q）为的一对弱状态互拟关系， 那么p，q可合并成一个状态，FSM得到简化

13、。第3章 3.2.4节在讨论FSM的简化方法四（隐藏内部事件） 时，我们已经给出若干简化FSM的例子（图3.5、图 3.7）。第五章 协议验证技术2 FSM的等价比较我们真正感兴趣的是两个FSM是否等价，两个FSM 的等价分强互拟等价（strong bisimulation equivalence） 和弱互拟等价（weak bisimulation equivalence），它们分 别可借助于FSM的强互拟关系和弱互拟关系来定义。 强互拟等价：两个相同和为强互拟等价 的充分必要条件是： 第五章 协议验证技术上述定义（弱互拟等价为例）可解释为：为了证明两 个系统是否弱互拟等价，我们只要将两个系统

14、合起来 看作一个系统，找出复合系统的弱互拟关系Rw，并 且证明两个初始状态为弱状态互拟关系就可以了。条 件（2）有嵌套性，即如果(i1,i2)为弱状态互拟关系， 那么它们的后继状态一定是弱状态互拟关系（参见 FSM的弱状态互拟关系定义），同样，它们的后继状 态的后继状态一定是弱互拟关系因此两个系统的 所有状态一定是彼此为弱互拟关系。根据这个原理， 我们可以设计一个算法，建立一个自动证明系统去证 明两个FSM是否等价。第五章 协议验证技术在许多文献中，两个FSM的强（弱）互拟等价也称之 为强（弱）观察等价（strong/weak observation equivalence)。 图5.6的两个

15、FSM是弱观察等价的，它们的复合系统 的弱互拟关系Rw为： Rw (.,(),(0,(0,.),(0,(.,0),(00,(0,0),(1,(1,.),(1,(.,1),(11,( 1,1),(10,(1,0),(01,(0,1) 它们初始状态(.,(.,.)是弱状态互拟的，读者可验证各 对互拟状态是否成立，案例来自【20】。第五章 协议验证技术图5-6 FSM的弱观察等价第五章 协议验证技术5.4.2 基于CCS的观察等价性分析 上节定义的观察等价性可直接引入到CCS表达 式。两个系统的行为表达式B1和B2是强观察 等价的充分必要条件是它们对应的状态转换 系统是强观察等价的，同样，表达式B1和B2 是弱观察等价的充分必要条件是它们对应的 FSM是观察等价的。 怎样根据CCS表达式导出FSM呢？第五章 协议验证技术第五章 协议验证技术观察等价是CCS和LOTOS的理论基础，它 们所形成的代数变换规则有的基于强观察等价 性，有的基于弱观察等价行。CCS或LOTOS表 达式变换过程就是等价变换过程。第三章第5 节已给出了多个CCS表达式的实例，此处不再 重复。