5 协议验证技术.ppt

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

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

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

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

5、 q=last element from W; add q to A; find all successsors of q; if (q=error_state) report_error(); else for each successor state s of q if (s is not in A or W) add s to W; analyze(); delete q from W; ,集合W包含未被分析的协议状态，A包含已分析和正在分析中的协议状态, 算法执行之前，W包含initial state,A为空，算法执行完毕之后,W为空，A包含协议的所有可达状态。该算法简单明了，然而要将

6、它付诸实施时,我们还必须解决以下一些问题。,第五章 协议验证技术,1.状态表示方法 协议状态用状态矩阵表示为: 这里E1，E2，En，为n层协议的几个协议实体的局部状态，Cij为协议实体i到协议实体j的通道的状态。当所有通道可处理成空通道时，协议状态可用数组E1,E2,En表示（因为空通道只有一种状态）。,第五章 协议验证技术,2.怎样找到所有可达的后继状态 不考虑报文顺序号，AB协议系统如图5.1所示，其中是R到S的通道，协议状态由二维矩阵组成。初始状态有四个后继状态：,很显然，状态（2），（3）和（4）不是可达状态(因为初始状态中AB内部没有任何数据需要传输，所以（2），（3),(4)状态

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

8、口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 ）不会执行，这是因为初始化后，作用点状态分别是：A =l , B =0 , a =0 , b =0 利

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

10、 协议验证技术,如果通道为队列通道，它的状态定义就会变得复杂，状态数也会激剧增加，事件的表述方法也变得复杂。例如，对于边界为n 的队列通道，事件表述形式可能为： entity(state):channel(staten)!message. 就是说，当通道队列长度小于n 时，协议实体entity 才会执行报文发送事件。,第五章 协议验证技术,4 搜索方法 算法5 . 1 的搜索方法取决于W 队列性质如果W 为FIFO （先进先出）队列，搜索是按宽度优先（breadth first）进行的，如果W 为FILO （先进后出）队列，搜索是按深度优先（deapth first）进行的深度优先搜索方法占用

11、存贮空间小这是最大优点之一。假定每个状态有两个后继状态，算法执行m 步之后，对于深度优先搜索方法，W 的长度为m ，但对于宽度优先搜索，W 的长度为2m。,第五章 协议验证技术,5 ，状态爆炸和错误检测 第三章在讨论FSM 简化时提到了什么是状态爆炸问题随着协议机制复杂性的提高和队列通道边界值的增大，状态爆炸问题使穷尽可达性分析变得无法实行5.2.2讨论的非穷尽可达性分析技术力图解决这个问题 算法5.1 中的语句：if（q=error_state）report_error(),其内容非常丰富，实现比较困难。5 . 2 . 3 讨论各种协议错误的检侧方法。,第五章 协议验证技术,算法5 . 2

12、: start() W=initial state; A=; analyse(); analyse() If (W=empty) return; q =element from W; add q to A; find all successors of q; if (q = error_state) report_error(); else for some successor state s of q if (s is not in A or W) add s to W analyse(); Delete q from W ,5 . 2 . 2 非穷尽可达性分析 将算法5 . 1 的语句fo

13、r each successor state s of q 改为 for some successor state s of q, 其它语句不变，我们就得到非穷尽可达性分析算法,第五章 协议验证技术,现在问题是，怎样从q 的所有后继状态中选取某些（some）状态进行分析，当然，被选取的状态应该是最有价值的，最有分析意义的，能最大可能检测协议错误的状态 1 事件优先选择法 事件t1,t2tn使状态q 产生n 个后继状态（图5 . 2 ) ，如果给这些事件赋于一定优先级别数值，那么被选择的后继状态（一般只选择一个），应该是优先级别数高的事件产生的优先级别数值的赋值方法可以是： (1) 静态赋值 可

14、达性分析进行之前，按照一定原则（发送事件优先于接收事件，协同事件高于内部事件等等）对所有事件赋于静态优先数值，可达性分析过程中，这些数值不改变 (2) 动态赋值 可达性分析执行之前，所有事件赋于相同的优先数值（也可以不同），可达性分析过程中，事件每执行一次，其优先数减1 。这种方法可均衡各个事件的执行次数，使本来很少有机会执行的事件能尽快的执行一次。,第五章 协议验证技术,2 协议实体优先选择法 如果事件t1,t2tn是由多个不同协议实体执行的，那么被选择的后继状态应该是优先级别高的协议实体所执行的事件产生的协议实体的优先级别的赋值方法可以是： (1) 静态赋值 按照一定原则（发方高于收方，响

15、应方高于发起方， ，等等）赋给各个 协议实体优先数值，可达性分析进行过程，数值不改变 (2) 动态赋值 方法之一 按照执行事件的多少或最后一次执行事件的时间动态改变协议实体的优先数值例如事件执行多的协议实体优先级别数降低，很长时间未执行任何事件的协议实体的优先级别数提高等等 动态斌值方法之二 按照事件的相关特性动态调整协议实体的优先级别数值例如当协议实体A 执行完发送事件之后，那么执行该事件的协同事件的协议实体的优先数值就立即提高等等,第五章 协议验证技术,3 纯粹随机选择法 这是最简单而有效的选择方法：从q的n 个后继状态中任取1个或几个进行分析由于从q 的n 个后继状态中选择“最有分析价值

16、”的状态是一个不可判定的问题，因此纯悴随机选择方法是一种简单适用的方法。 非穷尽可达性分析往往要进行多次（每次的状态选择方法不同）才能得到较满意的结果,第五章 协议验证技术,5 .2.3 协议错误的检测方法 可达性分析可检侧死锁、活锁、无意义事件、非确定的输入事件等协议错误 （1）如果q 无任何后继状态，那么q 就是死锁状态 （2） 在穷尽可达性分析中，如果一个事件未被执行一次，那么该事件可判定为无意义事件 （3）对于非穷尽可达性分析，算法在执行一遍之后，如果某些事件未执行一次那么在第二遍执行中应将这些事件的优先级别数值提高。只有当非穷尽可达性分析进行多次之后，才能判定那些事件为无意义事件 （

17、4） 如果某个协议实体在执行输入事件之后所获取的报文不是它所期待的报文，那么这个事件为非确定输入事件非确定输入事件反映协议的完备性不好，即协议没有考虑异常报文的接收处理问题。,第五章 协议验证技术,（6）活锁（死循环）的检测是非常麻烦的事情 活锁的检测首先是循环的检测在算法5 . 1 和5 . 2 中，如果q 的后继状态已在W 和A 中存在时，那么循环可能存在采用深度优先搜索方法时，循环容易检测（这是深度优先搜索的优点之二）：如果q 的后继状态s 已在W 中，那么s 到q 的状态序列（依次排列在W 中）这是一个循环作为一个案例分析我们来检测图5 . 3 的循环，图中状态编号表示深度优先搜索过程

18、中算法所访问的状态的先后次序状态（5 ）有三个后继状态（1 ）、（3 ) 和（6 ) . ( 6 ）不在W 中，它不构成循环后继状态（3 ）在W 中，事件t3产生循环，循环序列为（3 ) ( 4 ) ( 5 ) 后继状态（1 ）在w 中，t1产生循环，循环序列为（I ) ( 2 ) ( 3 ) ( 4 ) ( 5 ) 深度优先搜索方法不但容易检测循环，而且很容易得出循环序列,第五章 协议验证技术,现在的问题是，上述方法能检测出所有循环吗？答案是否定的，例如，图5 . 3中t4，t5 ，t6和t7，产生的循环就检测不出来当算法执行到状态（9 ）时，( 9 ）的后继状态之一（4 ）已不在W 中而是

19、在A 中当算法执行到状态（10 ）时，( 10 ）的后继状态（6 ）也在A 中前者t4产生循环，后者t5不产生循环，这就说明，如果q 的后继状态在A 中，循环可能存在。,第五章 协议验证技术,当q的后继状态在A中时，判定它是否产生循环有两种方法。,第五章 协议验证技术,断点法 算法执行多遍，执行第n遍算法时，将前面（n-1）次算法已检测到的循环断开，以便检测新的循环。对于图5.3所示的系统，算法执行第一遍时，由t1，t2和t3产生的循环都能检测出来。执行第二遍算法的时断开（3）（4）的转换，那么由t4产生的循环（1）（2）（8）（9）（4）（5）就检测出来了（注意：第二次算法执行时，搜索顺序不

20、同于第一次）。执行第三次算法时再断开（8）（9），那么由t6产生的循环（1）（2）（8）（11）（9）（4）（5）就检测出来了。,第五章 协议验证技术,标记法 算法执行过程中，每检测到一个循环就给处于循环之中的状态打上“标记”，表明它已处于某个循环之中。如果q的某个后续状态不在W中而在A中，并且它已处于某个循环之中，那么是否真正产生了新的循环，还必须做进一步判定。判定规则是：如果q的后继状态s在A中，并且s已处于某个循环之中而且该循环序列的任何一个状态或几个仍然在W中，那么新的循环产生。图5.3中，当算法执行但状态（9）时，它的后继状态（4）在A中，并且已处于两个循环之中，这表明新的循环可能存

21、在。由t3产生的循环的序列（3）（4）（5）中没有一个状态还处于W中，因此这个循环序列的所有状态不包括在新的循环之中。由t1产生的循环序列（1）（2）（3）（4）（5）中，（1）和（2）仍然处于W中，因此系ind循环序列存在，循环序列由（1）（2）（3）（4）（5）组成。当算法执行到状态（10）时，虽然它的后继状态（6）在A中，但由于（6）未处于任何其他循环之中，因此不存在新的循环。,第五章 协议验证技术,当所有循环已经检测出来之后，我们就可以判定那么循环是死循环。死循环的判定是更为复杂的问题。一种方法是通过“进展状态（progress state）”的标记来确定一个循环是否为死循环。如果循环

22、序列之内包含至少一个进展状态，那么它就不是死循环。进展状态的标记在可达性分析进行之前由手工进行。例如发送超时再发送构成一个循环，如果发送之前判定发送次数是否超过给定数值（超过给定值就转向错误处理），那么再发送状态就可以标记为进展状态。,第五章 协议验证技术,5.3 不变性分析 如果一个系统的某个性质能用一个确定的逻辑表达式描述，并且恒为真（不随系统的状态变化或执行序列而改变），那么这个性质称为系统的不变性质，简称系统不变性。协议的不变性分析包括二个工作：第一是完全正确的找出系统（协议）的不变性质。形成严格定义的不变性表达式；第二是以某种方式执行协议，验证不变性表达式是否恒为真。我们所说的不变性

23、分析指的是第二项工作。第一项工作由手工进行，许多协议描述文本也包含了不变性表达式。 不变性分析可采用两种途径：第一是不变性证明系统（往往采用归纳法），第二是不变性监测系统。下面分别介绍它们。,第五章 协议验证技术,5.3.1 不变性证明系统 用归纳法证明一个数学公式时，证明分两步进行：第一步证明x=0时公式是否成立；第二步，如果x=n时公式成立，那么证明x=n+1时公式是否成立。类似的，协议不变性证明也包括两步。首先，验证协议处于初始状态时不变性表达式是否成立，然后假设协议在某状态下不变性成立，验证协议从这个状态开始执行所有相关过程中不变性是否保持成立。 我们以窗口流控制为例说明其证明过程，案

24、例来自于文献资料【10】，本文已作剪辑。,第五章 协议验证技术,滑动窗口流控制是点对点通讯协议（传输层，数据链路层）所广泛采用的一种流控制方法。发送端维持两个计数器LW和HW，LW之值等于第一个未认可报文的顺序号，HW之值为下一次发送报文时能赋予的顺序号，HW和LW之间差为发送窗口，窗口宽度不应大于给定值。所有为认可报文放入ACKQUE队列中，如果收到一个认可报文，发送端将已认可的报文从ACKQUE队列中擦去，并修改LW之值。接收端维持一个计数器NS，NS之值为下一个接受报文的顺序号。如果所接受的报文的顺序号不等于NS之值，丢弃该报文。假定报文顺序号为自然数并可以无限增大，那么对于这样一个窗口

25、流控制，我们可形成3个不变性表达式： HW LW window LW seq(element of ACKQUE) HW LW NS HW,第五章 协议验证技术,这里，window为窗口宽度的最大值，函数seq()的返回值为报文的顺序号。表达式1规定为认可报文的个数必须小于或等于window，表达式2规定ACKQUE队列中的所有报文的顺序号应在窗口范围之内，表达式3规定接收端的NS总是在窗口之内。,第五章 协议验证技术,为了用归纳法证明上述窗口流控制的不变性，我们必须罗列出协议中的所有相关的原子操作。这些原子操作包括： SM:(Send a message) If( HW LW window)

26、 Seq(message) = HW; HW = HW+1; send the message; put the message to ACKQUE; RA:(Receive an ack) if ( the ack is OK) and (LW = seq(ack) =HW) delete all message in ACKQUE with seq(message) seq(ack); LW = seq(ack); RS:(RE send message after timeout) Send all message in ACKQUE; RM:(Receive a message) If

27、 (the message is OK) and (seq(message) =NS) deliver the messsge to the user; NS = NS + 1; SA:(Send the ack) send the ack with seq(ack) = NS; TM:(Transmit a message over the channel) the message may be lost or destroyed; TA:(Transmit an ack over the channel) The ack may be lost or destroyed;,第五章 协议验证

28、技术,原子操作SM，RA和RS由发端协议实体执行，RM和SA由收端协议实体执行，TM和TA由通道执行。不变性1和2的证明比较简单，因为只涉及发端协议实体所执行的原子操作。下面用归纳法证明不变性3。 证明： 第一步初始化后，HW = 0,LW = 0, NS = 0 因此LW=NS=HW,表达式3成立。 第二步假定协议在执行到某个状态时HW=j，LW=i，NS=k，并且ikj成立。验证发端协议实体发出一个新的报文之后，协议在执行所有相关原子操作之后，表达式3是否成立。 SM SM发出顺序号为j的报文之后，HW= j+1，LWNSHW,表达式3成立 TM TM不改变HW，LW和NS的值；,第五章

29、协议验证技术,RS 如果超时事件产生，重发报文，RS不修改HW,LW和NS； RM 由于SM执行之后HW=j+1，当RM执行之后，虽然NS=K+1，但表达式3仍然成立。如果所接收的报文顺序号有错，RM不修改NS，因此表达式3成立； SA 不改变 HW,LW和NS TA 不修改HW,LW和NS,TA发出的ACK报文的顺序号为k到j之间任意数值，即seq(ck)=kj； RA 正确执行之后LW=NS=seq(ck)=kj,而HW仍然为j+1，因此表达式3成立。如果RA丢弃ack报文，HW,LW和NS不变。 证毕。,第五章 协议验证技术,5.3.2 不变性监测系统 不变性监测系统借助监测软件和监测方

30、法对模拟运行或符号执行中的协议进行不变性校验的过程称之为不变性监测（invariant monitoring）。这种方法要求在协议代码中插入断点（子程序的调用或返回可视为自然断点），每个断点处，监测系统取相关变量值，计算并校验不变性表达式是否成立。除此之外，监测程序还可以对程序断言（assert）进行校验，程序断言是嵌于协议代码指定地方的特殊语句，例如ASSERT(state= =1)。协议代码运行到ASSERT语句时将指示监测程序对assert语句所申明的布尔表达式进行校验。不变性表达式不同于程序断言之处在于它无需插入协议代码之中。,第五章 协议验证技术,无论是不变性证明系统还是监测系统，我

31、们都认为下述两个问题都是不可判定问题。 不变性表达式已完整、准确、严密地表述了协议的所有行为和性质吗？ 用归纳法证明不变性时，引用的原子操作已覆盖了所有相关操作吗？在监测系统中，所设立的断点完备吗？ 在通过监测系统进行不变性分析时，我们还遇到一个麻烦问题。协议系统由多个协议实体组成（分布式），监测系统必须凌驾于它们之上，实现起来比较困难。由于上述这些问题和愿因，不变性分析在协议验证中的应用受到很大限制。,第五章 协议验证技术,5.4 等价性分析 “等价”意味着某种程度上的“相同”和“无差别”。如果两个协议模型或协议规范是等价的，那么它们可以互相替换，如果一个是正确的，那么另一个也是正确的。我们

32、在第三章讨论FSM和CCS时已利用“等价”方法简化FSM图和CCS表达式，这实质上也是一种等价性分析方法。等价性分析的另一个途径是证明两个协议的FSM图或CCS表达式是等价的，典型的情况是证明协议规范和它的服务规范一致性。 按等价的含义和等价的强弱，等价性分为【20】： 1 观察等价（observational equivalence） 如果对两个协议进行状态到状态的互相模拟时所观察到的协议行为没有差别，这两个协议是观察等价的。本节重点讨论观察等价性。 2 测试等价（test equivalence） 如果对两个协议施加相同的测试序列所观察到的协议行为没有差别，那么这两个协议是测试等价的。,第

33、五章 协议验证技术,3 跟踪等价（trace equivalence） 如果两个协议执行的事件序列是相同的，那么它们是踪迹等价的。 4 实现等价（implementation equivalence） 如果一个协议所做的每一件事情都能被第二个模仿（mimic），反之亦然，那么它们是实现等价的。 这四种等价按强弱程度排列的话，顺序是：观察等价、测试等价、跟踪等价、实现等价，其中观察等价还分为强观察等价和弱观察等价。等价性的强弱反映两个协议对行为细节的相同程度，等价性越强，它们的行为细节的相同程度越高。,第五章 协议验证技术,5.4.1 基于FSM的观察等价性分析 对于状态转换系统（参见第三章3.

34、2节），定义S*S为状态映射集合，例如，一个包括三个状态S0、S1和S2的FSM，S*S包括九种映射：（S0 ，S0），（S1 ，S1），（S2 ，S2），（S0 ，S1）（S2 ，S1）。下面研究一种特殊映射互拟关系。 如果两个状态pS，qS能够互相模拟，那么（p,q）为互拟关系（bisimulation relation）。互拟关系分强互拟关系（strong bisimulation relation）和弱互拟关系（weak bisimulation relation）4，13，它们的定义如下： 1 强状态互拟关系： 状态转换系统的两个状态pS，qS为强互拟关系的充分必要条件是，对所有eE

35、：,第五章 协议验证技术, 如果存在一个pS，p pT，那么就一定存在一个qS，qqT，并且（p,q）为强互拟关系； 如果存在一个qS，q qT，那么就一定存在一个pS，p pT，并且（p,q）为强互拟关系； 2 弱状态互拟关系： 状态转换系统的两个状态pS，qS为弱互拟关系的充分必要条件是，对所有eE，e不为I（内部事件）； 如果存在一个pS，p pT，那么就一定存在一个qS，q qT，并且（p,q）为弱互拟关系； 如果存在一个qS，q qT，那么就一定存在一个pS，p pT，并且（p,q）为弱互拟关系；,第五章 协议验证技术,第五章 协议验证技术,第五章 协议验证技术,图5.4和图5.5所示的例子中，我们可以得出这样的一个结论，即强互拟关系和弱互拟关系的差别在于后者忽略了内部事件。两个状态为强互拟关系就一定为弱互拟关系，反之不然。一个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,