通信协议分析-5-协议验证技术

第五章

协议验证技术协议验证(protocolverification):对协议本身的逻辑正确性进行校验的过程。协议分析（protocolanalysis）协议综合（protocolsynthesis）通常所说的协议验证指的是协议分析。

协议综合将协议设计过程和协议验证过程融合在一起。它通过一组能确保所设计的协议是正确的规则，从一些基本协议模块（这些基本模块已证明是正确的）中产生所希望的目标协议。

协议分析的目的：对已设计的协议进行分析和校验（这些已设计的协议大都是采用非形式化设计方法产生的）。

主要内容5.1引言5.2基于CFSM的可达性分析

5.2.1CFSM 5.2.2穷尽可达性分析

5.2.3非穷尽可达性分析

5.2.4协议错误检测方法5.3不变性分析5.4基于FSM等价性分析5.1引言协议分析方法：可达性分析(reachabilityanalysis)

等价性分析(equivalenceanalysis)

不变性分析(invarianceanalysis)这些分析工作可以手工完成，但更重要的是确定算法之后，借助于分析工具在计算机中自动或半自动完成。5.1引言协议表达形式：

用自然语言描述的非形式化协议文本

用协议模型技术表达的协议模型

用形式描述语言描述的协议规范用程序设计语言描述的协议代码上述分析方法在这几种表达形式上都可进行（手工或软件工具）。然而，通常都在协议模型上进行协议分析（简单，容易形成确定算法）。5.2基于CFSM的可达性分析基于CFSM模型的可达性分析，产生和检查协议所有或部分可达状态。所谓可达状态指协议从初始状态开始经历有限次转换之后可达到的状态，所有可达状态构成可达图（reachabilitygraph）。可达性分析的最重要工作是产生和检查可达图，判定是否存在死锁、活锁等协议错误。5.2基于CFSM的可达性分析可达性分析涉及三个重要技术：怎样找出所有可达状态，构成可达图；怎样检测死锁、活锁等协议错误；怎样解决状态爆炸问题。5.2.1CFSMC1C2+ASender21-R+R-AReceiver21CFSM

CFSM(CommunicatingFiniteStateMachine)用状态、转移和通道表示此处sender拥有两个通道：C1和C2。类型均设为FIFO。

C1为输出通道。C2为输入通道。当满足输出转移条件，Sender通过C1将消息R发送给Receiver。当且仅当C2中存在消息A时，Sender启动接收转移过程。CFSM12CSFM的初始状态，每个CFSM只有一个初始状态CFSM的状态CFSM状态转移

-R发送R

+A接收A

此外还可以表示为：(1,2,-R)和(2,1,+A)-R2+A1C1C2+ASender21-R+R-AReceiver21当前状态当协议启动时，Sender和Receiver各处于各自的初始状态。处于状态1的Receiver不能启动输出转移(1,2,+R)，处于状态1的Sender可以启动输出转移(1,2,-R)，使Sender的当前状态转移到2，消息R被放入通道C1。C1C2+ASender21-R+R-AReceiver21R5.2.1CFSM此时Sender处于状态2，可执行的转移为(2,1,+A)，但C2中无消息A，因此Sender等待。处于状态2的Receiver检测到C1中存在消息R，满足转移(1,2,+R)激活条件，Receiver接收R(从C1中将R取走)，当前状态变为2。C1C2+ASender21-R+R-AReceiver21RC1C2+ASender21-R+R-AReceiver215.2.1CFSM此时Sender处于状态2，可执行的转移为(2,1,+A)，但C2中无消息A，因此Sender等待。处于状态2的Receiver执行输出转移(1,2,-A)，将A放入通道C2，当前状态回到1。C1C2+ASender21-R+R-AReceiver21C1C2+ASender21-R+R-AReceiver21A5.2.1CFSM此时Receiver处于状态1，可执行的转移为(1,2,+R)，但C1中无消息R，因此Receiver等待。处于状态2的Sender检测到C2中存在消息A，满足转移(2,1,+A)激活条件，Sender接收A(从C2中将A取走)，当前状态变为1。C1C2+ASender21-R+R-AReceiver21AC1C2+ASender21-R+R-AReceiver215.2.1CFSM若输入通道为空，接收状态无法执行接收转移。当Sender和Receiver均处于接收状态，并且通道为空，则协议无法继续运行，该状态称为死锁，如上图所示。C1C2+ASender21-R+R-AReceiver215.2.1CFSM若通道C2中存在消息B，而Sender无法执行接收转移(2,1,+B)。则协议无法继续运行，该状态称为意外输入，如上图所示。C1C2+ASender21-R+R-AReceiver21B5.2.1CFSMReceiver的状态3永远无法成为当前状态，该状态称为不可执行状态。转移(2,3,+B)和(3,1,-C)永远不会被执行，这种转移被称为不可执行转移。C1C2+ASender21-R+R-AReceiver21B3-C+B5.2.1CFSM5.2.1CFSM协议状态用状态矩阵表示为：这里，E1,E2,…,En为几个协议实体的局部状态，Cij为协议实体i到协议实体j的通道的状态。当所有通道可处理成空通道时，协议状态可用数组[E1,E2,…,En]表示。…………………穷尽(exhausive)可达性分析产生和检查所有协议状态。以下算法描述穷尽可达性分析的基本思路：

start(){W={initialstate};A={};analyze();}analyze(){if(W==empty)return;q=elementfromW;addqtoA;findallsuccessorsofq;if(q==error_state)report_error();else{foreachsuccessorstatesofqif(sisnotinAorW){addstoW;analyze();}deleteqfromW;}}5.2.2穷尽可达性分析集合W包含未被分析的协议状态，A包含已分析和正在分析中的协议状态。算法执行之前，W包含initialstate，A为空，算法执行完毕之后，W为空，A包含协议的所有可达状态。该算法假定计算机的存贮空间足够大，计算速度足够高。5.2.2穷尽可达性分析5.2.2穷尽可达性分析5.2.2穷尽可达性分析不考虑报文顺序号，AB协议系统如图所示，其中C12是S到R的通道，C21是R到S的通道，协议状态由二维矩阵组成。初始状态有四个后继状态：

……状态（1）

……状态（2）

……状态（3）

……状态（4）5.2.2穷尽可达性分析显然，状态(2)，(3)和(4)不是可达状态。如何判定(1)是可达状态，而(2)，(3)和(4)不是可达状态。按下述格式定义交互事件：

entity(state):action-point(state)?/!message

entity(state)表示协议实体处于状态state中，action-point(state)表示作用点处于状态state中，!表示发送，?表示接收。作用点的状态定义为“0”或“1”，发送(!)结束后，状态为“1”，接收(?)结束后，状态为“0”。AB协议系统有四个作用点，它们是用户和S之间接口A，用户和R之间接口B，S和通道之间接口a和R和通道之间接口b。利用上述的事件表达格式，上页图对应的事件表述如下：5.2.2穷尽可达性分析事件(1)S(0):A(1)?m事件(8)R(1):B(0)!m事件(2)S(1):a(0)!m事件(9)C12(0):a(1)?m事件(3)S(2):timeout事件10)C12(1):drop事件(4)S(2):a(1)?ack事件(11)C12(1):b(0)!m事件(5)R(0):b(1)?m事件(12)C21(0):b(1)?ack事件(6)R(1):drop事件(13)C21(1):a(0)!ack事件(7)R(1):b(0)!ack5.2.2穷尽可达性分析则状态(1)，(2)，(3)和(4)分别对应事件(1)，(9)，(5)和(12)。初始状态时：

A=1,B=0,a=0,b=0因此事件(5)，(9)和(12)均不可执行。可见利用作用点标识，可以很容易判断协议处于状态q时，那些事件可以被执行，因而可以找到相应的后续状态。5.2.2穷尽可达性分析事件(1)S(0):A(1)?m事件(8)R(1):B(0)!m事件(2)S(1):a(0)!m事件(9)C12(0):a(1)?m事件(3)S(2):timeout事件10)C12(1):drop事件(4)S(2):a(1)?ack事件(11)C12(1):b(0)!m事件(5)R(0):b(1)?m事件(12)C21(0):b(1)?ack事件(6)R(1):drop事件(13)C21(1):a(0)!ack事件(7)R(1):b(0)!ack5.2.2穷尽可达性分析去掉内部作用状态，而根据通道状态来判定那些事件会被执行，将使算法变得简洁。用这种方法时，外部作用点保留，通道内的事件隐藏起来。AB协议系统的事件简化为：通道内的事件无需表示出来，通道C12的drop事件迭加到事件（6）中。

事件(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)R(1):B(0)!m5.2.2穷尽可达性分析如果通道为队列通道，它的状态定义就会变得复杂，状态数也会急剧增加，事件的表达方法也变得复杂。例如，对于边界为n的队列通道，事件表达形式可能为：

entity(state):channel(state<n)!message就是说，当通道队列长度小于n时，协议实体entity才会执行报文发送事件。C1C2-R+ASender21+R-AReceiver21CFSMCFSM-Bgsn：全局状态标识11EE21RE-R21BEgs0gs2-B意外输入，接收者无法确定如何处理消息B。E:通道空22EE+R21EA-A+Ags1gs3gs4可达图例：根据初始状态获得所有可能的状态。5.2.2穷尽可达性分析从全局初始态(所有通道为空，各实体均处于其初始态)开始，尝试执行所有可能的转移，遍历所有可达的状态。将死锁和意外输入的状况用独立的全局状态标识，仔细验证导致死锁和意外输入的原因，如果是协议本身的错误，则修改协议；如果是协议实现的疏忽，则指定相应的补救措施。通过检测通道中的消息数量，设计协议所需的缓冲区空间。通过标注可达的状态和已执行的转移，发现不可达状态和不可执行转移。5.2.2穷尽可达性分析对(M,N)构成的CFSM模型实施可达性分析。如果通道为FIFO类型，则验证需要多大的缓冲区空间？检验是否存在不可达状态和不可执行的转移？5.2.2穷尽可达性分析随着协议机制复杂性的提高和队列通道边界值的增大，状态爆炸问题使穷尽可达性分析变得无法实行。

非穷尽可达性分析技术为解决这个问题提供可行的办法。将穷尽可达性搜索算法的语句foreachsuccessorstatesofq改为forsomesuccessorstatesofq,其它语句不变，就得到非穷尽可达性分析算法。

5.2.3非穷尽可达性分析非穷尽可达性分析的关键问题是，怎样从q的所有后继状态中选取某些状态进行分析。

被选取的状态应该最有价值，最有分析意义，能最大可能检测协议错误的状态。5.2.3非穷尽可达性分析事件优先选择法协议实体优先选择法纯粹随机选择法5.2.3非穷尽可达性分析事件优先选择法5.2.3非穷尽可达性分析

事件t1,t2,……,tn使状态q产生n个后继状态，如果给这些事件赋于一定优先级，那么被选择的后继状态（一般只选择一个），应该是优先级别数高的事件产生的。优先级别数值的赋值方法：事件优先选择法5.2.3非穷尽可达性分析静态赋值。可达性分析进行之前，按照一定原则（发送事件优先于接收事件，协同事件高于内部事件，等等）对所有事件赋于静态优先数值，分析过程中，这些数值不改变。动态赋值。可达性分析执行之前，所有事件赋于相同的优先数值（也可以不同），可达性分析过程中，事件每执行一次，其优先数减1。这种方法可均衡各个事件的执行次数，使本来很少有机会执行的事件能尽快的执行一次。协议实体优先选择法5.2.3非穷尽可达性分析如果事件t1,t2,……,tn是由多个不同协议实体执行的，那么被选择的后继状态应该是优先级别高的协议实体所执行的事件产生的。协议实体的优先级别的赋值方法：协议实体优先选择法5.2.3非穷尽可达性分析静态赋值。按照一定原则（发方高于收方，响应方高于发起方，等等）赋给各个协议实体优先级别，可达性分析进行过程，数值不改变。协议实体优先选择法5.2.3非穷尽可达性分析动态赋值方法之一。按照执行事件的多少或最后一次执行事件的时间动态改变优先数值。例如，事件执行多的协议实体优先级别数降低，很长时间未执行任何事件的协议实体的优先级别数提高，等等。动态赋值方法之二。按照事件的相关特性动态调整优先级别。例如当协议实体A执行完发送事件之后，那么执行该事件的协同事件的协议实体的优先数值就立即提高，等等。纯粹随机选择法5.2.3非穷尽可达性分析从q的n个后继状态中任取一个进行分析。由于从q的n个后继状态中选择“最有分析价格”的状态是一个不可判定的问题，因此纯粹随机选择方法是一种简单实用的方法。非穷尽可达性分析往往要进行多次（每次的状态选择方法不同）才能得到较满意的结果。

5.2.4协议错误检测方法可达性分析可检测死锁、活锁、不可达状态、不可执行事件和意外输入等协议错误。如果q无任何后继状态，那么q就是死锁状态。5.2.4协议错误检测方法可达性分析可检测死锁、活锁、不可达状态、不可执行事件和意外输入等协议错误。在穷尽可达性分析中，如果一个事件未被执行一次，那么该事件可判定为不可执行事件。对于非穷尽可达性分析，算法在执行一遍之后，如果某些事件未执行一次，那么在第二遍执行中应将这些事件的优先级别数值提高，只有当非穷尽可达性分析进行多次之后，才能判定那些事件为不可执行事件。5.2.4协议错误检测方法可达性分析可检测死锁、活锁、不可达状态、不可执行事件和意外输入等协议错误。如果某个协议实体在执行输入事件之后所获取的报文不是它所期待的报文，那么这个事件为意外输入事件。意外输入反映协议的完备性不好，即协议没有考虑异常报文的接收处理等问题。5.2.4协议错误检测方法活锁的检测较为复杂，首先要检测循环，常用方法：1)断点法算法执行多遍，执行第n遍算法时，将前面(n-1)次算法检测到的循环断开，以便检测新的循环。对于下页图所示的系统，算法执行第一遍时，由t1,t2和t3产生的循环都能检测出来。执行第二遍算法时断开(3)－(4)的转换，那么由t4产生的循环(1)(2)(8)(9)(4)(5)就检测出来了（注意：第二次执行算法时，搜索顺序不同于第一次）。执行第三次算法时再断开(8)－(9)，那么由t6产生的循环(1)(2)(8)(11)(9)(4)(5)就检测出来了。

5.2.4协议错误检测方法2)标记法算法执行时，每检测到一个循环就给处于循环之中的状态打上“标记”。如果q的某个后继状态不在W中而在A中，并且它已打上标记，还须作进一步判定是否真正产生了新的循环。判定规则：如果q的后继状态s在A中，并且s已打上标记，且该循环序列的任何一个状态或几个仍然在W中，那么新的循环产生。5.2.4协议错误检测方法2)标记法上页图中，当算法执行到状态(9)时，它的后继状态(4)在A中，并且已处于两个循环之中，这表明新的循环可能存在。由t3产生的循环的序列(3)(4)(5)中没有一个状态还处于W中，因此这个循环序列的所有状态不包括在新的循环之中。由t1产生的循环的序列(1)(2)(3)(4)(5)中，(1)和(2)仍然处于W中，因此新的循环序列存在，循环序列由(1)(2)(8)(9)(4)(5)组成。当算法执行到状态(10)时，虽然它的后继状态(6)在A中，但由于(6)未处于任何其它循环之中，因此不存在新的循环。

5.2.4协议错误检测方法当所有循环都已检测出来之后，就可以判定那些循环是死循环。死循环的判定是一件更为复杂的问题。通常通过“进展状态”(progressstate)的标记来确定一个循环是否为死循环。如果循环序列之内包含至少一个进展状态，那么它就不是死循环。进展状态的标记在可达性分析进行之前手工完成。例如发送→超时→再发送构成一个循环，如果再发送之前判定发送次数是否超过给定数值（超过给定值就转向错误处理），那么再发送状态就可以标记为进展状态。5.3不变性分析如果一个系统的某个性质能用一个确定的逻辑表达式描述，并且恒为真（不随系统的状态变化或执行序列而改变），那么这个性质称为系统的不变性质，简称系统不变性。协议不变性分析包括：第一是找出系统（协议）的不变性质，形成严格定义的不变性表达式；第二是以某种方式执行协议，验证不变性表达式是否恒为真。我们所说的不变性分析指的是第二项工作。不变性分析可采用两种途径：第一是不变性证明系统（往往采用归纳法），第二是不变性监测系统。我们介绍第一种方法。5.3不变性分析用归纳法证明一个数学公式时，证明分三步进行：第一步证明x=0时公式是否成立；第二步，假设x=n时公式成立；第三步，证明x=n＋1时公式是否成立。类似的，协议不变性证明也包括三步。首先，验证协议处于初始状态时不变性表达式是否成立；然后，假定协议在某状态下不变性成立；最后，验证协议从这个状态开始执行所有相关事件过程中不变性是否保持成立。5.3不变性分析以窗口流控制为例说明其证明过程。/teaching/rn/animations/gbn_sr/5.3不变性分析以窗口流控制为例说明其证明过程。滑动窗口流控制是点对点通讯协议（传输层，数据链路层）所广泛采用的一种流控制方法。

发送端维护两个计数器LW和HWLW：第一个已发送未认可报文的顺序号HW：下一次发送报文时能赋于的顺序号HW–LW<=window所有未认可报文放入ACKQUE队列中

如果收到一个认可报文,发送端将已认可的报文从ACKQUE队列中擦出，改变LW。5.3不变性分析以窗口流控制为例说明其证明过程。接收端维护一个计数器NS，NS

=下一个准备接收报文的顺序号。

如果所接收的报文的顺序号不等于NS之值，丢弃该报文。

假定报文顺序号为自然数并可无限增大。

对于这样一个窗口流控制，可得出3个不变性表达式：5.3不变性分析

HW–LW≤window （1）

LW≤seq(elementofACKQUE)≤HW （2）

LW≤NS≤HW （3）其中：window为窗口宽度的最大值函数seq()的返回值为报文的顺序号式(1)规定未认可报文的个数必须小于或等于window式(2)规定ACKQUE队列中的所有报文的顺序号应在窗口范围之内式(3)规定接收端的NS总是在窗口之内5.3不变性分析协议中相关的原子操作包括：SM:(Sendamessage)If(HW–LW<window){seq(msg)=HW;HW=HW+1;sendthemsg;putthemsgtoACKQUE; }RA:(Receiveanack)If((theackisOK)and(LW<=seq(ack)<=HW)){deleteallmsgsinACKQUEwithseq(msg)<seq(ack);LW=seq(ack);}RS:(Re-sendmessagesaftertimeout)sendallmessagesinACKQUE;5.3不变性分析协议中相关的原子操作包括：RM:(Receiveamessage)

If((themsgisOK)and(seq(msg)==NS)){deliverthemsgtotheuser;

SA;NS=NS+1;}SA:(Sendtheack)sendtheackwithseq(ack)=NS;TM:(Transmitamessageoverthechannel)themsgmaybelostordestroyed;TA:(Transmitanackoverthechannel)theackmaybelostordestroyed;5.3不变性分析不变性表达式（3）的证明如下：第一步：初始化后，HW＝0，LW＝0，NS＝0因此LW＝NS＝HW。第二步：假定协议在执行到某个状态时，HW＝j，LW=i,NS=k，并且i≤k≤j成立。验证发端协议实体发出一个新的报文之后，协议在执行所有相关原子操作之后，式（３）是否成立。5.3不变性分析第三步：SM发出顺序号为j的报文之后，HW=j+1,LW≤NS＜HW，式（３）成立；TM不改变HW、LW和NS之值；如果超时事件产生，重发报文，RS不修改HW、LW和NS；由于SM执行之后HW=j+1，当RM执行之后，NS＝k+1，式（３）仍然成立。如果所接收的报文顺序号有错，RM不修改NS，因此式（３）成立：SA不改变HW、LW和NS；TA不修改HW、LW和NS，TA发出的ACK报文的顺序号为k到j之间任意数值，即seq(ack)=k…j；RA正确执行之后LW＝NS＝seq(ack)=k…j，而HW仍然为j+1，因此式（３）成立。如果RA丢弃ack报文，HW、LW和NS不变。5.4基于FSM等价性分析“等价”意味着某种程序上的“相同”和“无差别”。如果两个协议模型或协议规范是等价的，那么它们可以互相替换，如果一个是正确的，那么另一个也是正确的。等价性分析的目的是证明两个协议的FSM图是等价的，典型的情况是证明协议规范和它的服务规范一致性。5.4基于FSM等价性分析按等价的含义和等价的强弱，等价性分为：1、观察等价（observationalequivalence）如果对两个协议进行状态到状态的互相模拟时所观察到的协议行为没有差别，这两个协议是观察等价的。2、测试等价（testequivalence）如果对两个协议施加相同的测试序列所观察到的协议行为没有差别，那么这两个协议是测试等价的。3、踪迹等价（traceequivalence）如果两个协议执行的事件序列是相同的，那么它们是踪迹等价的。4、实现等价（implementationequivalence）如果一个协议所做的每一件事情都能被第二个模仿（mimic），反之亦然，那么它们是实现等价的。5.4基于FSM等价性分析生活中有哪些等价关系？5.4基于FSM等价性分析基于FSM的观察等价性分析

对于状态转换系统（S,i,E,T），定义S*S为状态映射集合。例如，一个包括三个状态S0，S1和S2的FSM，S*S包括九种映射：（S0，S0），（S1，S1），（S2，S2），（S0，S1），…（S2，S1）。

互拟关系：如果两个状态p∈S，q∈S能互相模拟，那么（p,q）为互拟关系（bisimulationrelation）。互拟关系分强互拟关系（strongbisimulationrelation）和弱互拟关系（weakbisimulationrelation）。5.4基于FSM等价性分析强状态互拟关系：状态转换系统（S,i,E,T）的两个状态p∈S，q∈S为强互拟关系的充分必要条件是：对所有e∈E，如果存在一个p'∈S,p→e→p'∈T，那么就一定存在一个q'∈S,q→e→q'∈T，并且(p',q')为强互拟关系；如果存在一个q'∈S,q→e→q'∈T，那么就一定存在一个p'∈S,p→e→p'∈T，并且(p',q')为强互拟关系。5.4基于FSM等价性分析弱状态互拟关系：状态转换系统（S,i,E,T）的两个状态p∈S，q∈S为弱互拟关系的充分必要条件是：对所有e∈E，e≠I

如果存在一个p'∈S,p→e→p'∈T，那么就一定存在一个q'∈S,q→e→q'∈T，并且(p',q')为弱互拟关系；如果存在一个q'∈S,q→e→q'∈T，那么就一定存在一个p'∈S,p→e→p'∈T，并且(p',q')为弱互拟关系。5