《第4讲_协议验证技术》由会员分享，可在线阅读，更多相关《第4讲_协议验证技术（69页珍藏版）》请在金锄头文库上搜索。
1、 网网 络络 协协 议议 工工 程程 第第 4讲：协议验证技术讲：协议验证技术9/17/20241协议验证技术第第 4 讲：协议验证技术讲：协议验证技术4.1 概述概述4.2 协议性质协议性质4.3 可达性分析可达性分析4.4 不变性分析不变性分析4.5 逻辑证明逻辑证明4.6 其它验证方法其它验证方法9/17/20242协议验证技术协议验证协议验证v每一个新设计的协议在被完全证明没有错误之每一个新设计的协议在被完全证明没有错误之前，都应认为不是完全正确的。前，都应认为不是完全正确的。v协议验证技术和形式描述技术是同步发展的，协议验证技术和形式描述技术是同步发展的，它也是协议工程技术中研究最早
2、、最深入的课它也是协议工程技术中研究最早、最深入的课题，使用的技术方法多种多样。题，使用的技术方法多种多样。 9/17/20243协议验证技术验证的含义验证的含义v“验证验证”的含义：的含义： 验证协议的设计。验证协议的设计。通过分析每一层的所有协议实体间的所有可能的交通过分析每一层的所有协议实体间的所有可能的交互、协议的抽象规范中所确定的功能以及通过低层互、协议的抽象规范中所确定的功能以及通过低层提供的服务所实现的对等层间的通信来确定上述操提供的服务所实现的对等层间的通信来确定上述操作是否满足协议的服务规范。作是否满足协议的服务规范。在设计阶段进行验证，可以及早发现协议错误，大在设计阶段进行
3、验证，可以及早发现协议错误，大大降低协议开发成本。大降低协议开发成本。 验证协议的实现。验证协议的实现。检查每一个协议实体的实现是否满足它的抽象协议检查每一个协议实体的实现是否满足它的抽象协议规范。大多数情况下，协议实现的验证是通过不同规范。大多数情况下，协议实现的验证是通过不同的测试工具来实现的。的测试工具来实现的。有时也将其称为协议实现评估或协议的一致性测试有时也将其称为协议实现评估或协议的一致性测试 一般情况下，协议验证指的是第一般情况下，协议验证指的是第(1)类验类验证，这也是本课程的观点。具体来说，协证，这也是本课程的观点。具体来说，协议验证是指根据协议规范来检查协议实体议验证是指根
4、据协议规范来检查协议实体间的交互是否满足一定特性间的交互是否满足一定特性(properties)或条件或条件(conditions)的过程，例如，检查的过程，例如，检查是否有死锁存在。通过协议验证，可以获是否有死锁存在。通过协议验证，可以获知协议设计是否满足正确性、完整性和一知协议设计是否满足正确性、完整性和一致性等要求。致性等要求。 9/17/20244协议验证技术Verification and Validationv在英文文献中，在英文文献中，“验证验证”一词有两种不同的表示：一词有两种不同的表示：validation和和verification。它们的含义也比较混乱。它们的含义也比较混
5、乱。 v文献文献Rud98认为认为:validation主要是指检查协议逻辑上的一致性，以查实协议设主要是指检查协议逻辑上的一致性，以查实协议设计中是否存在某些错误，这些错误是所有协议中都可能存在计中是否存在某些错误，这些错误是所有协议中都可能存在的共性错误，与具体的协议功能无关，例如，验证有无死锁。的共性错误，与具体的协议功能无关，例如，验证有无死锁。而而verification则是指检查协议是否能成功地提供指定的协议功则是指检查协议是否能成功地提供指定的协议功能能。 v文献文献Lai98认为认为:verification主要是指检查一个系统是否满足它的规格说明，主要是指检查一个系统是否满足
6、它的规格说明，而而validation的含义则不仅包括的含义则不仅包括verification，还可能包括对最还可能包括对最终的系统实现进行测试，系统模拟，性能分析预测等。终的系统实现进行测试，系统模拟，性能分析预测等。 9/17/20245协议验证技术Verification and ValidationvBohem：Verification: to establish the truth of correspondence between a software product and its specification (“truth”) or are we building the pr
7、oduct right?Validation: to establish the fitness or worth of a software product for its operational mission (“to be worth”) or are we building the right product?v谢书中介绍：谢书中介绍：Verification: 在功能方面进行验证在功能方面进行验证Validation: 在语法方面进行证实在语法方面进行证实v在实践当中，在实践当中，validation和和verification所采用的技术并没有所采用的技术并没有明显的界限。也正因
8、为如此，很多文献并没有严格区分明显的界限。也正因为如此，很多文献并没有严格区分validation和和verification，而是混用这两个单词。而是混用这两个单词。9/17/20246协议验证技术Verification and Validation9/17/20247协议验证技术形式化验证形式化验证v非形式化验证则主要通过传统的遍历非形式化验证则主要通过传统的遍历(walkthrough)和代码检查和代码检查(inspection)来实来实现。现。v协议验证通常与形式描述技术有关。形式化验协议验证通常与形式描述技术有关。形式化验证主要将形式描述技术和推理技术相结合，是证主要将形式描述技术
9、和推理技术相结合，是形式化描述技术的一个重要方面，其优点是：形式化描述技术的一个重要方面，其优点是：一方面可以获得无二义性的协议规范，一方面可以获得无二义性的协议规范，另一方面可以通过计算机辅助工具来帮助实施自动另一方面可以通过计算机辅助工具来帮助实施自动或半自动验证。或半自动验证。 v协议设计者必须在早期的协议设计阶段采用一协议设计者必须在早期的协议设计阶段采用一些技术或工具来发现设计中存在的错误，这也些技术或工具来发现设计中存在的错误，这也是协议验证的最重要的目的。是协议验证的最重要的目的。 9/17/20248协议验证技术第第 4 讲：协议验证技术讲：协议验证技术4.1 概述概述4.2
10、协议性质协议性质4.3 可达性分析可达性分析4.4 不变性分析不变性分析4.5 逻辑证明逻辑证明4.6 其它验证方法其它验证方法9/17/20249协议验证技术协议性质协议性质v 协议验证的最主要内容是检查协议是否满足规协议验证的最主要内容是检查协议是否满足规定的定的协议性质协议性质。一般情况下，将协议性质分为。一般情况下，将协议性质分为两类：两类：一般性质一般性质(general properties)。指所有协议所具有指所有协议所具有的一些公共特性。不同文献对这类性质的个数和描的一些公共特性。不同文献对这类性质的个数和描述也不尽相同。述也不尽相同。特殊性质特殊性质(specific pro
11、perties)。是指与具体协议内是指与具体协议内容有关的性质。对这些性质的定义构成了服务规范容有关的性质。对这些性质的定义构成了服务规范的主体内容。的主体内容。 v也有文献将协议性质分为安全性也有文献将协议性质分为安全性(safety)和活和活跃性跃性(liveness)。9/17/202410协议验证技术一般性质一般性质v可达性可达性(Reachability)。验证协议的各种可能状态之间的可验证协议的各种可能状态之间的可达关系。如果协议的某个状态从初态不可达，则表明协议有达关系。如果协议的某个状态从初态不可达，则表明协议有错误。如果从状态错误。如果从状态A到状态到状态B的变迁不可能发生的
12、变迁不可能发生(直接或间接直接或间接)，则从状态，则从状态A到状态到状态B是不可达的。是不可达的。 v没有死锁没有死锁(Deadlock freeness)。最典型的死锁是协议中各实最典型的死锁是协议中各实体都处于这样的一种等待状态，即只有在体都处于这样的一种等待状态，即只有在“某一事件某一事件”发生发生后才能做进一步的动作，但在该状态下，这个后才能做进一步的动作，但在该状态下，这个“某一事件某一事件”却不可能发生。死锁发生时，协议所处的状态称为死锁状态。却不可能发生。死锁发生时，协议所处的状态称为死锁状态。 v 没有活锁没有活锁(Livelock freeness) 。活锁是指协议处于无限的
13、死活锁是指协议处于无限的死循环中，而没有别的事件可使协议从这一循环中解脱出来。循环中，而没有别的事件可使协议从这一循环中解脱出来。例如，协议无限制地执行超时重发操作，但总是收不到对方例如，协议无限制地执行超时重发操作，但总是收不到对方的确认信息。状态还是在变化的，不过不能脱离这种死循环的确认信息。状态还是在变化的，不过不能脱离这种死循环状态而已。状态而已。 9/17/202411协议验证技术一般性质（一般性质（Cont.）v弱活锁弱活锁(Weak livelock)。是指协议处于死循环中，只有当协是指协议处于死循环中，只有当协议交换命令的相对速度达到某一状态时，协议才退出死循议交换命令的相对速
14、度达到某一状态时，协议才退出死循环。环。v时间相关的活锁时间相关的活锁(Time-dependent livelock)。也称为也称为临时阻临时阻塞塞(Tempo-blocking)。它是指协议处于死循环中，但是当通它是指协议处于死循环中，但是当通信双方交换报文的相对速度到达某一状态时，协议可以从信双方交换报文的相对速度到达某一状态时，协议可以从死循环中出来。死循环中出来。v有界性有界性(Boundedness)。检验协议的某些成分或参数的容量检验协议的某些成分或参数的容量(例如：通道容量、窗口大小例如：通道容量、窗口大小)是否有界。有界性是针对协是否有界。有界性是针对协议元素性质和通道性质而
15、言。议元素性质和通道性质而言。v可恢复性或自同步性可恢复性或自同步性（Recovery from failures）。）。这是当这是当出现差错后，协议能否在有限的步骤内返回到正常状态出现差错后，协议能否在有限的步骤内返回到正常状态( (包包括初始态括初始态) )执行。执行。 9/17/202412协议验证技术一般性质（一般性质（Cont.）v无状态二义性无状态二义性(State ambiguities freeness)。一个进程在某一个进程在某一时刻只允许具有一个稳定状态。所谓稳定状态是指当通一时刻只允许具有一个稳定状态。所谓稳定状态是指当通信双方的通道为空时的进程状态。若在某一时刻进程可以
16、信双方的通道为空时的进程状态。若在某一时刻进程可以有多个稳定状态，则称该进程的状态为二义状态。有多个稳定状态，则称该进程的状态为二义状态。v互斥性互斥性(Mutual exclusion)(Mutual exclusion)。互斥性是指有些协议动作不互斥性是指有些协议动作不能同时被多个用户执行。例如，多个用户不能同时请求同能同时被多个用户执行。例如，多个用户不能同时请求同一资源。一资源。 v终止或进展终止或进展(Termination or Progress)。是指协议提供的是指协议提供的服务必须在有限时间内完成。服务必须在有限时间内完成。终止是针对终止协议终止是针对终止协议(terminat
17、ing protocols)而言，意思是指协议而言，意思是指协议总是能到达期望的结束状态。总是能到达期望的结束状态。而进展则是针对循环协议而进展则是针对循环协议(cyclic protocols)而言，意思是指协议而言，意思是指协议总是能到达它的初始状态。总是能到达它的初始状态。 9/17/202413协议验证技术一般性质（一般性质（Cont.）v无冗余描述无冗余描述(Absence of Overspecification)。协协议规范中没有无用的、冗余描述，例如，没有议规范中没有无用的、冗余描述，例如，没有未经实践的报文接收未经实践的报文接收(absence of unexercised
18、message receptions)。 v公平性公平性(Fairness)。是指每一个协议实体均应是指每一个协议实体均应平等地得到运行的机会，无论其它的协议实体平等地得到运行的机会，无论其它的协议实体想做什么。想做什么。 9/17/202414协议验证技术特殊性质特殊性质v完整性完整性(Completeness)。是指协议设计考虑了是指协议设计考虑了所有可能发生的事件、选项以及服务。检验协所有可能发生的事件、选项以及服务。检验协议是否能处理所有可能的输入，即是否缺少应议是否能处理所有可能的输入，即是否缺少应用的处理，或有无非期待的接收或输入用的处理，或有无非期待的接收或输入(即错即错收收)。
19、也有的文献将完整性称为。也有的文献将完整性称为完全正确性完全正确性(complete correctness)。v一致性一致性(consistency)。是指协议服务行为是指协议服务行为(或或性质性质)和协议行为和协议行为(或性质或性质)一致，即协议应该一致，即协议应该提供用户要求的服务，而无需提供用户没有要提供用户要求的服务，而无需提供用户没有要求的服务。也有文献将一致性称为求的服务。也有文献将一致性称为部分正确性部分正确性(partial correctness)、等价性等价性(equivelence)等等。 9/17/202415协议验证技术一般性质一般性质 vs. 特殊性质特殊性质v协
20、议验证着重在于一般性质，而协议测试则着协议验证着重在于一般性质，而协议测试则着重于特殊性质。重于特殊性质。 9/17/202416协议验证技术安全性安全性(safety) vs. 活动性活动性(liveness)v安全性安全性是指协议的所有动作均需与它的服务规范保持一致，即没有是指协议的所有动作均需与它的服务规范保持一致，即没有不期望的情况出现。不期望的情况出现。不期望的情况包括：不可接收的事件、不可进一步向前的状不期望的情况包括：不可接收的事件、不可进一步向前的状态、错误的动作、错误的条件、变量值越界等。态、错误的动作、错误的条件、变量值越界等。例如，如果传输协议传送报文，则它必须将这些报文
21、传送到例如，如果传输协议传送报文，则它必须将这些报文传送到正确的目的地，按正确的顺序，并且无差错地交给目的主机。正确的目的地，按正确的顺序，并且无差错地交给目的主机。安全性保证协议不出现错误。安全性保证协议不出现错误。v活动性活动性是指在有穷时间内，完成规范所规定的动作是指在有穷时间内，完成规范所规定的动作(或所有的服务必或所有的服务必须在有限时间内完成须在有限时间内完成)。在进行逻辑验证时，确保一个有限的时延就足够了。但是，在进行逻辑验证时，确保一个有限的时延就足够了。但是，在验证协议的效率和响应能力时，则必须定量地确定期望的在验证协议的效率和响应能力时，则必须定量地确定期望的时延、吞吐率以
22、及其它的一些指标。时延、吞吐率以及其它的一些指标。 9/17/202417协议验证技术安全性安全性(safety) vs. 活动性活动性(liveness)v活动性活动性(Cont.)协议的活动性体现在协议的活动性体现在终止性终止性(termination)和和进展性进展性(progress)两个方面。两个方面。 终止性终止性是指协议从任何一个状态开始运行，经过有限时间总是指协议从任何一个状态开始运行，经过有限时间总能正确地达到终止状态；能正确地达到终止状态；进展性进展性是指协议从初始状态运行，经过有限时间总能到达指是指协议从初始状态运行，经过有限时间总能到达指定状态。定状态。 在某些情况下，
23、终止状态和初始状态是同一的。这样，协议在某些情况下，终止状态和初始状态是同一的。这样，协议从初始状态出发总能正确地回到初始状态，并可反复运行。从初始状态出发总能正确地回到初始状态，并可反复运行。 9/17/202418协议验证技术第第 4 讲：协议验证技术讲：协议验证技术4.1 概述概述4.2 协议性质协议性质4.3 可达性分析可达性分析4.4 不变性分析不变性分析4.5 逻辑证明逻辑证明4.6 其它验证方法其它验证方法9/17/202419协议验证技术协议验证方法协议验证方法v验证方法主要有两类：验证方法主要有两类：模型检查模型检查(Model Checking)(Model Checkin
24、g)。最常见方法：最常见方法：可达性分析可达性分析(RA: Reachability analysis) ，它包括状它包括状态穷举，状态随机枚举，状态概率枚举等方法态穷举，状态随机枚举，状态概率枚举等方法 不变性分析不变性分析(invariance analysis)等价性分析等价性分析(equivalence analysis)重要问题：状态空间爆炸重要问题：状态空间爆炸 证明证明( (Proving) )试图用推理演算方法严密地证明协议的各种性质试图用推理演算方法严密地证明协议的各种性质v其他方法：其他方法：模拟模拟（Simulation）通过一些模拟试验来测试协议的各种性质通过一些模拟试
25、验来测试协议的各种性质9/17/202420协议验证技术可达性可达性分析分析一、概一、概 述述9/17/202421协议验证技术可达性可达性分析分析v可达性分析是最常用的协议验证方法。它试图产可达性分析是最常用的协议验证方法。它试图产生和检查协议所有或部分可达状态。生和检查协议所有或部分可达状态。“可达状态可达状态”是指协议从初始状态开始经历是指协议从初始状态开始经历有限次转有限次转换之后可达到的状态。换之后可达到的状态。所有可达状态构成可达图所有可达状态构成可达图( (RG: Reachability Graph)。9/17/202422协议验证技术可达性可达性分析（分析（Cont.）v可达
26、性分析的原理是可达性分析的原理是: :采用穷举法检查同一层内两个或多个协议实体间所有采用穷举法检查同一层内两个或多个协议实体间所有可能的交互所产生的状态。可能的交互所产生的状态。将协作的协议实体的状态以及连接这些协议实体的低将协作的协议实体的状态以及连接这些协议实体的低层称为系统的层称为系统的全局状态全局状态或或混合状态混合状态(composite or global state)。从一个给定的初始状态开始，所有可能的变迁从一个给定的初始状态开始，所有可能的变迁(用户命用户命令、超时、报文到达等令、超时、报文到达等)产生许多新的全局状态。产生许多新的全局状态。对每一个新产生的状态重复执行上述过
27、程直到没有新对每一个新产生的状态重复执行上述过程直到没有新的状态产生的状态产生(某些变迁将导致系统返回到已产生的状态某些变迁将导致系统返回到已产生的状态)。 对于一个给定的初始状态和一组关于低层协议的假定对于一个给定的初始状态和一组关于低层协议的假定(提供的服务的类型提供的服务的类型)，这种分析能够确定协议可能产，这种分析能够确定协议可能产生的所有结果。生的所有结果。 9/17/202423协议验证技术可达性可达性分析（续）分析（续）v可达性分析最适合于用状态变迁模型描述的协议模型。可达性分析最适合于用状态变迁模型描述的协议模型。对于状态变迁模型的全局状态空间的产生也比较容易自动化，目前对于状
28、态变迁模型的全局状态空间的产生也比较容易自动化，目前已有很多作此用途的工具。已有很多作此用途的工具。v对于程序语言描述的协议模型也可以使用可达性分析方法。对于程序语言描述的协议模型也可以使用可达性分析方法。具体做法是：在程序中设置许多断点具体做法是：在程序中设置许多断点(break points)，这些断点有效这些断点有效地定义了系统的控制状态。地定义了系统的控制状态。v可达性分析方法特别适用于验证上一节提到的协议的一般性可达性分析方法特别适用于验证上一节提到的协议的一般性质质，因为这些性质是可达图结构的一种直接结果。，因为这些性质是可达图结构的一种直接结果。没有出口的全局状态要么是死锁，要么
29、是期望的结束状态。没有出口的全局状态要么是死锁，要么是期望的结束状态。同样，收到一个没有定义如何处理的报文或超过了传输媒体的带宽同样，收到一个没有定义如何处理的报文或超过了传输媒体的带宽等情况很容易被发现。等情况很容易被发现。 9/17/202424协议验证技术可达性可达性分析（分析（Cont.）v可达性分析涉及三个重要技术：可达性分析涉及三个重要技术： 怎样找出所有可达状态，构成可达图。怎样找出所有可达状态，构成可达图。 怎样检测死锁、活锁等协议错误。怎样检测死锁、活锁等协议错误。 怎样解决状态空间爆炸问题。怎样解决状态空间爆炸问题。 9/17/202425协议验证技术可达性可达性分析分析二
30、、可达性分析算法二、可达性分析算法9/17/202426协议验证技术可达性可达性分析算法分析算法v文献文献Holz93给出了三个主要的可达性分析算法：给出了三个主要的可达性分析算法：穷尽性可达性分析算法穷尽性可达性分析算法(exhaustive or full search)(exhaustive or full search)，受控部分搜索算法受控部分搜索算法(controlled partial search)(controlled partial search)，随机模拟算法随机模拟算法(random simulation)(random simulation)。 9/17/202427
31、协议验证技术算法一：算法一：穷尽性可达性分析算法穷尽性可达性分析算法 start() W = 初始状态初始状态; /* 工作集：分析的状态工作集：分析的状态 */ A = ; /* 已分析过的状态已分析过的状态 */ analyze(); analyze() /* 全局搜索全局搜索 */ if (W为空为空) return; q = 取自取自W的元素；的元素； 将将q加入到加入到A中中 if (q是错误状态是错误状态) report_error(); /* 报告错误报告错误 */ else for (q的每一个后继状态的每一个后继状态s) if (s不在不在A或或W中中) 把把s加入到加入到W
32、中；中；analyze(); 从从W中删除中删除q； 工作集工作集W控制系统状态空间树的搜索控制系统状态空间树的搜索顺序。如果工作集顺序。如果工作集W中的状态以先进中的状态以先进先出（先出（FIFO）的顺序取出，那么算的顺序取出，那么算法执行的是状态空间树的先广搜索法执行的是状态空间树的先广搜索（breadth-first）；）；如果以先进后出如果以先进后出（FILO）的顺序取出，则是状态空的顺序取出，则是状态空间树的先深搜索间树的先深搜索(deapth-first)。先深先深搜索方法占用存贮空间小，这是其最搜索方法占用存贮空间小，这是其最大优点之一。大优点之一。 假定每个状态有两个后假定每个
33、状态有两个后继状态，算法执行继状态，算法执行m步步之后，对于先深搜索方之后，对于先深搜索方法，法，W的长度为的长度为m，而而对于先广搜索方法，对于先广搜索方法，W的长度为的长度为2m。 9/17/202428协议验证技术算法一：算法一：穷尽性可达性分析算法穷尽性可达性分析算法 start() W = 初始状态初始状态; /* 工作集：分析的状态工作集：分析的状态 */ A = ; /* 已分析过的状态已分析过的状态 */ analyze(); analyze() /* 全局搜索全局搜索 */ if (W为空为空) return; q = 取自取自W的元素；的元素； 将将q加入到加入到A中中 i
34、f (q是错误状态是错误状态) report_error(); /* 报告错误报告错误 */ else for (q的每一个后继状态的每一个后继状态s) if (s不在不在A或或W中中) 把把s加入到加入到W中；中；analyze(); 从从W中删除中删除q； 9/17/202429协议验证技术算法一：算法一：穷尽性可达性分析算法穷尽性可达性分析算法v上述算法假定用来进行验证的计算机的存贮空间上述算法假定用来进行验证的计算机的存贮空间足够大，且计算速率足够高。这往往是不现实的。足够大，且计算速率足够高。这往往是不现实的。v因此，大多数情况下，只有将协议验证模型化简因此，大多数情况下，只有将协议
35、验证模型化简到给定机器能够分析的程度时基于这种算法的验到给定机器能够分析的程度时基于这种算法的验证才可行。证才可行。一般采用结构化或分层的方法来降低模型的复杂性。一般采用结构化或分层的方法来降低模型的复杂性。但在某些情况下，由于被分析的问题的固有复杂性，只但在某些情况下，由于被分析的问题的固有复杂性，只能将模型化简到一定程度，因为如果再进一步化简则可能将模型化简到一定程度，因为如果再进一步化简则可能丢失其基本的、重要的性质。能丢失其基本的、重要的性质。由此产生了另外一种搜索算法，即受控部分搜索算法。由此产生了另外一种搜索算法，即受控部分搜索算法。 9/17/202430协议验证技术算法二：算法
36、二：受控部分搜索算法受控部分搜索算法/* start()与算法与算法5.1中的相同中的相同 */analyze() /* 部分搜索部分搜索 */ if (W为空为空) return; q = 取自取自W的元素；的元素； 将将q加入到加入到A中中 if (q是错误状态是错误状态) report_error(); /* 报告错误报告错误 */ else for (q的某些后继状态的某些后继状态s) if (s不在不在A或或W中中) 把把s加入到加入到W中；中；analyze(); 从从W中删除中删除q； 选择状态的规则有很多，例如，选择状态的规则有很多，例如，限制深度法限制深度法(Depth-bo
37、unds)，散散开搜索开搜索(Scatter Search)，定向定向搜索法搜索法(Guided Search)，概率法概率法(Probabilistic Search)，启发启发式式Yu91，随机选择法随机选择法(Random Selections)West87，状态矢量状态矢量法法Holz91等等 算法不考虑检查协议所有可算法不考虑检查协议所有可能的状态，而是预先确定满能的状态，而是预先确定满足某些要求足某些要求(如，死锁如，死锁)的潜的潜在的全局状态，然后检查这在的全局状态，然后检查这些状态是否可达。些状态是否可达。 9/17/202431协议验证技术算法二：算法二：受控部分搜索算法受控
38、部分搜索算法v限制深度法限制深度法。原理是限制被分析的执行序列的长度，从而只需分析协议行为的原理是限制被分析的执行序列的长度，从而只需分析协议行为的一个子集。实质上，限制了完全搜索算法中的工作集一个子集。实质上，限制了完全搜索算法中的工作集W的大小。的大小。限制深度法是一种相当标准和简单的部分搜索技术。限制深度法是一种相当标准和简单的部分搜索技术。 v散开搜索法散开搜索法。原理是尽可能选择有可能导致死锁的执行序列来进行检查，从而原理是尽可能选择有可能导致死锁的执行序列来进行检查，从而增加尽快发现错误的概率。例如，死锁的一个前提条件是没有待增加尽快发现错误的概率。例如，死锁的一个前提条件是没有待
39、处理的报文处理的报文(通道为空通道为空)，因此，这种算法更可能去检查报文接收，因此，这种算法更可能去检查报文接收操作而不是发送操作。操作而不是发送操作。 v定向搜索法定向搜索法。在定向搜索法中，为每一个后继状态计算它的代价函数值在定向搜索法中，为每一个后继状态计算它的代价函数值(cost function)。然后，根据这个计算结果作为是否执行它的依据。代然后，根据这个计算结果作为是否执行它的依据。代价函数在搜索过程中可以动态地改变。价函数在搜索过程中可以动态地改变。如果代价函数是固定的，则相当于散开搜索法。如果代价函数是固定的，则相当于散开搜索法。目前，被证明有用的代价函数或定向表达式还不多见
40、。目前，被证明有用的代价函数或定向表达式还不多见。 9/17/202432协议验证技术算法二：算法二：受控部分搜索算法受控部分搜索算法v概率搜索法概率搜索法。在这种方法中，根据状态出现的概率的递减顺序来选择后继状态。在这种方法中，根据状态出现的概率的递减顺序来选择后继状态。将系统中的所有变迁都标上标签，最简单地处理就是打上将系统中的所有变迁都标上标签，最简单地处理就是打上“高高”或或“低低”标签，分别表示出现概率的高低。然后，根据标签来选标签，分别表示出现概率的高低。然后，根据标签来选择要检查的状态。择要检查的状态。 v随机选择法随机选择法。前几种方法总是试图预测在何处最容易发现协议错误，这种
41、预测前几种方法总是试图预测在何处最容易发现协议错误，这种预测是有很大风险的。是有很大风险的。因为根据因为根据MurphyMurphy定律的推论，错误最可能隐藏在设计者或验证者定律的推论，错误最可能隐藏在设计者或验证者认为不像有错误的地方认为不像有错误的地方Holz93Holz93。随机选择法不关心在哪些状态最可能发现错误，而是随机地选择随机选择法不关心在哪些状态最可能发现错误，而是随机地选择后继状态。后继状态。它不仅是一种最容易实现的技术，也是一种最有可能产生高质量它不仅是一种最容易实现的技术，也是一种最有可能产生高质量的搜索的方法。的搜索的方法。 9/17/202433协议验证技术算法二：算
42、法二：受控部分搜索算法受控部分搜索算法v一般来说，受控部分搜索算法较全局搜索方法有一般来说，受控部分搜索算法较全局搜索方法有效和可行。但是，这种方法不能保证协议无错。效和可行。但是，这种方法不能保证协议无错。通常需要执行多次才能得到比较可信的结果。通常需要执行多次才能得到比较可信的结果。 9/17/202434协议验证技术算法三：算法三：随机模拟算法随机模拟算法v前面介绍的受控部分搜索算法部分地解决了穷尽性可达性前面介绍的受控部分搜索算法部分地解决了穷尽性可达性分析算法的状态爆炸问题，因而得到了广泛的应用。分析算法的状态爆炸问题，因而得到了广泛的应用。 v但是，在有些情况下，这种受控部分搜索算
43、法也会变得不但是，在有些情况下，这种受控部分搜索算法也会变得不可行。例如，如果想直接将一个协议验证算法应用到一个可行。例如，如果想直接将一个协议验证算法应用到一个高度详细的、正在一台机器上运行的、经编译过的代码上高度详细的、正在一台机器上运行的、经编译过的代码上时，即使是使用受控部分搜索算法也需要大量的内存来保时，即使是使用受控部分搜索算法也需要大量的内存来保存搜索的状态。存搜索的状态。 v在这种情况下，惟一可行的方法是从搜索算法中去掉状态在这种情况下，惟一可行的方法是从搜索算法中去掉状态集集A和和W，而用而用随机模拟随机模拟(random simulation)或或随机遍历随机遍历(rand
44、om walk)的方法搜索协议的状态空间。的方法搜索协议的状态空间。 9/17/202435协议验证技术算法三：算法三：随机模拟算法随机模拟算法analyze() /* 随机模拟随机模拟 */ q = 初始状态初始状态; while (1) if (q = 错误状态错误状态) report_error(); q = 初始状态初始状态; else q = q的一个后继状态；的一个后继状态；9/17/202436协议验证技术三种三种算法的比较算法的比较v穷尽性可达性分析算法的优点在于可以证明协议中没有错误，穷尽性可达性分析算法的优点在于可以证明协议中没有错误，但问题在于其应用范围有限。但问题在于其
45、应用范围有限。最主要原因是该算法能分析的最大状态数目依赖于协议、描述方法最主要原因是该算法能分析的最大状态数目依赖于协议、描述方法和可用的计算资源。特别是当系统状态的数目非常大时会发生状态和可用的计算资源。特别是当系统状态的数目非常大时会发生状态空间爆炸。空间爆炸。一般来说，根据协议状态空间大小和可用的内存空间，这种算法的一般来说，根据协议状态空间大小和可用的内存空间，这种算法的覆盖率并不一定能达到覆盖率并不一定能达到100%。如果状态空间大小为。如果状态空间大小为R，执行搜索时执行搜索时内存中能够存储的最大状态数为内存中能够存储的最大状态数为A，那么只有当那么只有当R小于等于小于等于A时覆盖
46、时覆盖率和搜索质量才能达到率和搜索质量才能达到100%。 当当R大于等于大于等于A时，全搜索策略将变成部分搜索，且不能保证检查协时，全搜索策略将变成部分搜索，且不能保证检查协议中最重要的部分，覆盖率减小到议中最重要的部分，覆盖率减小到A/R，而搜索质量变得更差。而搜索质量变得更差。因此，对于复杂的协议，穷尽性可达性分析的效果只能算作是一种因此，对于复杂的协议，穷尽性可达性分析的效果只能算作是一种低质量的部分搜索。低质量的部分搜索。 9/17/202437协议验证技术三种三种算法的比较算法的比较 (Cont.)v受控部分搜索算法的目的是证明错误的存在，而不是证明受控部分搜索算法的目的是证明错误的
47、存在，而不是证明没有错误。没有错误。v与穷尽性可达性分析相比，这种算法可以有效地解决状态与穷尽性可达性分析相比，这种算法可以有效地解决状态空间爆炸问题，同时利用有限的资源来验证协议的最重要空间爆炸问题，同时利用有限的资源来验证协议的最重要的部分，从而最大限度地发现错误。的部分，从而最大限度地发现错误。v其缺点是必须能够预先判断出协议中的错误的大概位置，其缺点是必须能够预先判断出协议中的错误的大概位置，然而这很难预先做到。因为，多个进程间的关系非常复杂，然而这很难预先做到。因为，多个进程间的关系非常复杂，不能仅仅根据其表面的关系来判断。不能仅仅根据其表面的关系来判断。v另外，虽然这些方法能够减小
48、状态空间的大小，但它们都另外，虽然这些方法能够减小状态空间的大小，但它们都没有提供任何工具，将状态空间的大小与可用内存相匹配。没有提供任何工具，将状态空间的大小与可用内存相匹配。v使用这些方法时，有效搜索的部分状态空间的大小是协议使用这些方法时，有效搜索的部分状态空间的大小是协议相关的，只能通过实验确定，要想找到一种最优的方法，相关的，只能通过实验确定，要想找到一种最优的方法，必须按照不同的选择策略进行多次验证。必须按照不同的选择策略进行多次验证。 9/17/202438协议验证技术三种算法的比较三种算法的比较 (Cont.)v随机模拟算法与协议系统的大小和复杂性无关，即使随机模拟算法与协议系
49、统的大小和复杂性无关，即使是无限大小的系统，也可以应用。因此，对于复杂的是无限大小的系统，也可以应用。因此，对于复杂的验证问题，这种算法也许是唯一可用的方法。验证问题，这种算法也许是唯一可用的方法。v但这种方法也有些问题，例如，但这种方法也有些问题，例如，它没有明确的终止，无法判断是否已经访问过系统的所有可它没有明确的终止，无法判断是否已经访问过系统的所有可达状态；达状态；由于没有算法的终止，也就无法判断是否已经发现了系统的由于没有算法的终止，也就无法判断是否已经发现了系统的所有错误所有错误v因此只能发现协议中的错误，而不能证明协议中没有因此只能发现协议中的错误，而不能证明协议中没有错误。错误
50、。 9/17/202439协议验证技术可达性可达性分析分析三、基于可达性分析的三、基于可达性分析的协议错误的检测方法协议错误的检测方法 9/17/202440协议验证技术协议错误的检测协议错误的检测v死锁。死锁。如如果果一一个个状状态态无无任任何何后后继继状状态态，那那么么该该状状态态就就是是死死锁锁状态。状态。v无意义事件。无意义事件。在在穷穷尽尽可可达达性性分分析析中中，如如果果一一个个事事件件未未被被执执行行一一次次，那么该事件可判定为无意义事件。那么该事件可判定为无意义事件。对对于于非非穷穷尽尽可可达达性性分分析析，算算法法在在执执行行一一遍遍之之后后，如如果果某某些些事事件件未未执执
51、行行一一次次，那那么么在在第第二二遍遍执执行行中中应应将将这这些些事事件件的的优优先先级级别别数数值值提提高高。只只有有当当非非穷穷尽尽可可达达性性分分析析进行多次之后，才能判定哪那些事件为无意义事件。进行多次之后，才能判定哪那些事件为无意义事件。 9/17/202441协议验证技术协议错误的检测（协议错误的检测（Cont.）v非确定的输入事件。非确定的输入事件。 如果某个协议实体在执行输入事件之后所获取的报文不是它所期如果某个协议实体在执行输入事件之后所获取的报文不是它所期待的报文，那么这个事件为非确定输入事件。非确定输入事件反待的报文，那么这个事件为非确定输入事件。非确定输入事件反映协议的
52、完整性不好，即协议没有考虑异常报文的接收处理问题。映协议的完整性不好，即协议没有考虑异常报文的接收处理问题。 v活锁。活锁。 活锁的检测首先是循环的检测。当所有循环都已检测出来之后，活锁的检测首先是循环的检测。当所有循环都已检测出来之后，我们就可以判定那些循环是死循环。我们就可以判定那些循环是死循环。 死循环的判定是较为复杂的问题。一种方法是通过死循环的判定是较为复杂的问题。一种方法是通过“进展状态进展状态(progress state)”的标记来确定一个循环是否为死循环。如果循环的标记来确定一个循环是否为死循环。如果循环序列之内包含致少一个进展状态，那么它就不是死循环。进展状序列之内包含致少
53、一个进展状态，那么它就不是死循环。进展状态的标记在可达性分析进行之前由手工进行。态的标记在可达性分析进行之前由手工进行。 例如：例如：发送发送-超时超时-再发送再发送 构成一个循环，如果发送之前判定发构成一个循环，如果发送之前判定发送次数是否超过给定数值送次数是否超过给定数值(超过就转向错误处理超过就转向错误处理)，那么再发送状，那么再发送状态就可以标记为进展状态。态就可以标记为进展状态。 9/17/202442协议验证技术可达性可达性分析分析四、状态空间爆炸问题四、状态空间爆炸问题 9/17/202443协议验证技术状态空间爆炸问题状态空间爆炸问题v随着协议复杂性的提高和队列通道边界值的增随
54、着协议复杂性的提高和队列通道边界值的增大，状态爆炸问题使穷尽可达性分析无法进行。大，状态爆炸问题使穷尽可达性分析无法进行。v除了前面介绍的部分搜索算法，还可以采用下除了前面介绍的部分搜索算法，还可以采用下列方法来减小状态空间使之处于一个可控制的列方法来减小状态空间使之处于一个可控制的范围之内。范围之内。 部分规格说明和验证部分规格说明和验证(Partial Specification and Verification) 选择大的动作单元选择大的动作单元(Choosing Large Units of Actions) 分解或划分分解或划分(Decomposition or Partitioni
55、ng) 按断言来分类状态按断言来分类状态(Classifying States by Assertions) 9/17/202444协议验证技术部分规格说明和验证部分规格说明和验证v根据具体描述方法的特点，只选取协议的某些根据具体描述方法的特点，只选取协议的某些方面进行描述。例如，在用状态变迁图来描述方面进行描述。例如，在用状态变迁图来描述协议时，常常只描述主要状态间的状态变迁规协议时，常常只描述主要状态间的状态变迁规则，而忽略参数值和其它的状态变量等细节。则，而忽略参数值和其它的状态变量等细节。 9/17/202445协议验证技术选择大的动作单元选择大的动作单元 v状态空间爆炸是因为不同实体
56、执行的动作相互交状态空间爆炸是因为不同实体执行的动作相互交织所造成的。织所造成的。我们可以通过合并一些状态或动作来减少状态及变迁我们可以通过合并一些状态或动作来减少状态及变迁数。例如，可以将协议数据的准备和发送看作是一个数。例如，可以将协议数据的准备和发送看作是一个不可分割的动作，从准备到发送不需同其它实体交互。不可分割的动作，从准备到发送不需同其它实体交互。从而可以将这样一个动作看作是一次从而可以将这样一个动作看作是一次“状态变迁状态变迁”。 v这种方法的一个特殊应用例子是：这种方法的一个特殊应用例子是：仅仅考虑传输通道为空时的状态，即发送方发送的报仅仅考虑传输通道为空时的状态，即发送方发送
57、的报文立即能够到达接收方。文立即能够到达接收方。当要传输的报文的数量比较小或不考虑传输时延时，当要传输的报文的数量比较小或不考虑传输时延时，这种这种“空通道抽象空通道抽象”是合理的。在这种情况下，可以是合理的。在这种情况下，可以将不同实体的发送和接收变迁合并到一个涉及到两个将不同实体的发送和接收变迁合并到一个涉及到两个实体的联合状态变迁中。实体的联合状态变迁中。 9/17/202446协议验证技术分解或划分分解或划分 v这种方法前提条件是可以将协议分解或划分成这种方法前提条件是可以将协议分解或划分成多个可控制的阶段、子层或模块。然后，对每多个可控制的阶段、子层或模块。然后，对每一个子层、阶段或
58、模块进行独立地描述和验证。一个子层、阶段或模块进行独立地描述和验证。v由于分解后的协议组件或阶段的状态及状态变由于分解后的协议组件或阶段的状态及状态变迁数要远小于原始协议，所以这种方法大大降迁数要远小于原始协议，所以这种方法大大降低了对原始协议验证的复杂性。低了对原始协议验证的复杂性。 v例如，将例如，将HDLCHDLC分解成以下几个子层：比特填充、分解成以下几个子层：比特填充、校验和过程元素。后者又可以细分为几个组件。校验和过程元素。后者又可以细分为几个组件。v需要注意的是，证明了每一个组件或阶段的正需要注意的是，证明了每一个组件或阶段的正确性，并不一定能安全保证原始协议的正确性。确性，并不
59、一定能安全保证原始协议的正确性。 9/17/202447协议验证技术按断言来分类状态按断言来分类状态 v在可达性分析中，考虑状态类而不是单个状态。在可达性分析中，考虑状态类而不是单个状态。通过选择合适的谓词，可以大大减少状态数目。通过选择合适的谓词，可以大大减少状态数目。v例如，考虑一个协议实体接收编号的信息帧。不例如，考虑一个协议实体接收编号的信息帧。不考虑将序列号变量的各种可能的值看作是不同的考虑将序列号变量的各种可能的值看作是不同的状态，取而代之仅仅考虑三种状态：变量状态，取而代之仅仅考虑三种状态：变量“小于小于”，“等于等于”，“大于大于”收到的信息帧的编号。收到的信息帧的编号。 9/
60、17/202448协议验证技术第第 4 讲：协议验证技术讲：协议验证技术4.1 概述概述4.2 协议性质协议性质4.3 可达性分析可达性分析4.4 不变性分析不变性分析4.5 逻辑证明逻辑证明4.6 其它验证方法其它验证方法9/17/202449协议验证技术不变性分析不变性分析v如果一个系统的某个性质能用一个确定的如果一个系统的某个性质能用一个确定的逻辑表逻辑表达式达式描述，并且描述，并且恒为真恒为真(不随系统的状态变化或不随系统的状态变化或执行序列而改变执行序列而改变)，那么这个性质称为系统的不，那么这个性质称为系统的不变性质，简称为变性质，简称为系统不变性系统不变性(system inva
61、riance)。v协议不变性分析包括二个工作：协议不变性分析包括二个工作：第一是第一是完全正确地找出系统完全正确地找出系统( (协议协议) )的不变性质的不变性质，形成，形成严格定义的不变性逻辑表达式。这项工作由手工进行，严格定义的不变性逻辑表达式。这项工作由手工进行，许多协议描述文本也包含了不变性表达式。许多协议描述文本也包含了不变性表达式。 第二是以某种方式执行协议，验证不变性表达式是否第二是以某种方式执行协议，验证不变性表达式是否恒为真。我们所说的不变性分析指的是第二项工作。恒为真。我们所说的不变性分析指的是第二项工作。 9/17/202450协议验证技术不变性分析不变性分析v不变性分析
62、可采用两种途径：不变性分析可采用两种途径： 不变性证明系统不变性证明系统(通常采用归纳法通常采用归纳法)； 不变性监测系统。不变性监测系统。 9/17/202451协议验证技术不变性证明系统不变性证明系统v采用归纳法时，协议不变性证明包括两步：采用归纳法时，协议不变性证明包括两步： 验证协议处于初始状态时不变性表达式是否成立；验证协议处于初始状态时不变性表达式是否成立； 然后，假定协议在某状态下不变性成立，验证协议然后，假定协议在某状态下不变性成立，验证协议从这个状态开始执行所有相关事件过程中不变性是从这个状态开始执行所有相关事件过程中不变性是否保持成立。否保持成立。 9/17/202452协
63、议验证技术不变性监测系统不变性监测系统v不变性监测系统借助监测软件和监测方法对模拟运行或不变性监测系统借助监测软件和监测方法对模拟运行或符号执行中的协议进行不变性校验的过程称之为符号执行中的协议进行不变性校验的过程称之为不变性不变性监测监测(invariant monitoring)。这种方法要求在协议代码中插入这种方法要求在协议代码中插入断点断点(子程序的调用或返回可视子程序的调用或返回可视为自然断点为自然断点)，每个断点处，监测系统取相关变量值，计算并校验不变性表达每个断点处，监测系统取相关变量值，计算并校验不变性表达式是否成立。式是否成立。v通过监测系统进行不变性分析时，还会遇到一个麻烦
64、问通过监测系统进行不变性分析时，还会遇到一个麻烦问题：题：协议系统由多个协议实体组成协议系统由多个协议实体组成(分布性分布性)，监测系统必须凌驾于，监测系统必须凌驾于它们之上，实现起来比较困难。它们之上，实现起来比较困难。v由于上述这些问题和原因，不变性分析在协议验证中的由于上述这些问题和原因，不变性分析在协议验证中的应用受到很大限制。应用受到很大限制。 9/17/202453协议验证技术系统不变式系统不变式 vs. 断言断言v不变性监测程序还可对程序断言不变性监测程序还可对程序断言(assert)进行进行校验，程序断言是嵌于协议代码指定地方的特校验，程序断言是嵌于协议代码指定地方的特殊语句，
65、例如殊语句，例如ASSERT(state = =1)。协议代码协议代码运行到运行到ASSERT语句时将指示监测程序对语句时将指示监测程序对ASSERT语句所申明的布尔表达式进行校验。语句所申明的布尔表达式进行校验。v不变性表达式则要求无论系统不变性表达式则要求无论系统( (协议协议) )处于何种处于何种状态，不变性表达式都必须成立。状态，不变性表达式都必须成立。v此外，不变性表达式不同于程序断言之处还在此外，不变性表达式不同于程序断言之处还在于它于它无需插入协议代码中无需插入协议代码中。 9/17/202454协议验证技术不变性分析：问题不变性分析：问题v无论是不变性证明系统还是监测系统，下述
66、两个无论是不变性证明系统还是监测系统，下述两个问题都是不可判定问题：问题都是不可判定问题：不变性表达式已完整、准确、严密地表述了协议的所不变性表达式已完整、准确、严密地表述了协议的所有行为和性质吗？有行为和性质吗？ 用归纳法证明不变性时，引用的原子操作已覆盖所有用归纳法证明不变性时，引用的原子操作已覆盖所有相关操作吗？在监测系统中，所设立的断点完备吗？相关操作吗？在监测系统中，所设立的断点完备吗？ 9/17/202455协议验证技术不变性分析：参考文献不变性分析：参考文献vButler Lampson Butler Lampson 在在MITMIT的讲稿的讲稿: : “Principles o
67、f Computer Systems” “Principles of Computer Systems” 9/17/202456协议验证技术第第 4 讲：协议验证技术讲：协议验证技术4.1 概述概述4.2 协议性质协议性质4.3 可达性分析可达性分析4.4 不变性分析不变性分析4.5 逻辑证明逻辑证明4.6 其它验证方法其它验证方法9/17/202457协议验证技术逻辑证明逻辑证明v逻辑证明用逻辑证明用“推理演算技术推理演算技术”严密地证明协议的各种性质，严密地证明协议的各种性质，也称为也称为程序证明程序证明。推理演算技术主要包括：。推理演算技术主要包括：时态逻辑、时态逻辑、谓词逻辑、谓词逻辑
68、、代数演算等。代数演算等。 v逻辑证明方法将协议的正确性要求格式化成断言逻辑证明方法将协议的正确性要求格式化成断言(assertions)，这些断言由变量和过程组成。这些断言由变量和过程组成。理想情况下，这些格式化的正确性要求应该由服务规范提供。理想情况下，这些格式化的正确性要求应该由服务规范提供。但是，在大多数情况下，服务还没有被很好地定义，所以验证者必但是，在大多数情况下，服务还没有被很好地定义，所以验证者必须自己来格式化这些正确性要求。须自己来格式化这些正确性要求。在得到协议的格式化断言后，就可以证明每一个协议实体满足这些在得到协议的格式化断言后，就可以证明每一个协议实体满足这些高级断言
69、高级断言(这些断言通常涉及到两个实体这些断言通常涉及到两个实体)。要做到这一点，通常要求在协议程序中合适的地方插入一些附加的要做到这一点，通常要求在协议程序中合适的地方插入一些附加的断言。断言。 9/17/202458协议验证技术逻辑证明（续）逻辑证明（续）v优点：优点：有坚实的数学基础有坚实的数学基础能够验证协议的所有性质，而不仅仅是一般性质能够验证协议的所有性质，而不仅仅是一般性质不需处理状态空间爆炸问题不需处理状态空间爆炸问题 v问题：问题：理想情况下，所有正确性要求均可被格式化成合适的理想情况下，所有正确性要求均可被格式化成合适的断言，但是这断言，但是这需要很强的创新能力需要很强的创新
70、能力。另外，采用这类技术的验证过程很难自动化，因为它另外，采用这类技术的验证过程很难自动化，因为它们需要程序证明方面的专门知识。们需要程序证明方面的专门知识。当系统具有无限状态时，证明并不总是可行。此时，当系统具有无限状态时，证明并不总是可行。此时，要么中途停止证明过程，要么还需补充有关证明技术要么中途停止证明过程，要么还需补充有关证明技术和被验证的设计等方面的复杂的知识。和被验证的设计等方面的复杂的知识。 9/17/202459协议验证技术断言证明断言证明(AP: Assertion Proving) v断言证明在系统所有可能的状态集合上使用谓词。断言证明在系统所有可能的状态集合上使用谓词。
71、每一个谓词定义一个状态集合，集合中的状态使每一个谓词定义一个状态集合，集合中的状态使得该谓词为真。得该谓词为真。v在可达性分析时，可将基于某一谓词的状态集看在可达性分析时，可将基于某一谓词的状态集看成是一个状态。这样，谓词的选择对减少系统状成是一个状态。这样，谓词的选择对减少系统状态数是至关重要的。态数是至关重要的。v断言证明可以验证协议的某些属性，例如利用不断言证明可以验证协议的某些属性，例如利用不变式断言可以验证协议的安全性和活跃性。变式断言可以验证协议的安全性和活跃性。v断言证明首先需要定义能反映协议各种正确性特断言证明首先需要定义能反映协议各种正确性特性的断言，并将它形式化。然后，证明
72、每一个协性的断言，并将它形式化。然后，证明每一个协议实体满足所定义的断言。议实体满足所定义的断言。 9/17/202460协议验证技术代数验证代数验证(AV: Algebraic verification) v代数验证是一种基于用进程代数描述的协议文代数验证是一种基于用进程代数描述的协议文本上的验证方法。本上的验证方法。v这种方法的一般过程为：这种方法的一般过程为：首先用表达式或文法首先用表达式或文法(grammars)描述协议组件；描述协议组件；然后，将组件描述集成起来，并简化集成后的协议然后，将组件描述集成起来，并简化集成后的协议描述；描述；最后，通过手工或自动分析来验证协议的正确性。最后
73、，通过手工或自动分析来验证协议的正确性。 9/17/202461协议验证技术时态逻辑时态逻辑(TL: Temporal Logic) v时态逻辑是对谓词逻辑的扩展，在谓词逻辑的时态逻辑是对谓词逻辑的扩展，在谓词逻辑的基础上增加了一些与时序有关的操作符基础上增加了一些与时序有关的操作符(模态模态算子算子)。v利用这些扩展的时序操作符可以实现以时间为利用这些扩展的时序操作符可以实现以时间为序的事件序列的推理。序的事件序列的推理。v在时态逻辑中，通过不变式或时态断言可以描在时态逻辑中，通过不变式或时态断言可以描述协议的安全性和活跃性。述协议的安全性和活跃性。v验证以系统断言证明为基础，利用已被验证的
74、验证以系统断言证明为基础，利用已被验证的低级断言和时态逻辑为实施。低级断言和时态逻辑为实施。 9/17/202462协议验证技术结构化归纳结构化归纳(SI: Structural Induction) v当验证拥有大量交互实体的协议当验证拥有大量交互实体的协议(如，路由协议如，路由协议)时，结构化归纳是一种很有用的方法。时，结构化归纳是一种很有用的方法。v对于期望的验证要求，可以先在实体的子集上进对于期望的验证要求，可以先在实体的子集上进行验证。行验证。v然后用归纳法证明如果对于然后用归纳法证明如果对于N个实体指定的条件个实体指定的条件(要求要求)成立，则对于成立，则对于N+1个实体时条件也成
75、立。个实体时条件也成立。v这种方法也称为这种方法也称为“拓朴归纳拓朴归纳(induction on topology)”。 9/17/202463协议验证技术符号执行符号执行(SX: Symbolic Execution) v符号执行创建一棵证明树，树上每一个结点代表符号执行创建一棵证明树，树上每一个结点代表一类全局状态。树根表示证明开始时的初始状态，一类全局状态。树根表示证明开始时的初始状态，而树叶则表示所有可能的结束状态。而树叶则表示所有可能的结束状态。v每一个结点都有一个谓词表每一个结点都有一个谓词表(predicate list)与之与之相连，谓词表描述了与该结点相关联的一类结点。相连
76、，谓词表描述了与该结点相关联的一类结点。v如果想证明一个协议具有某种属性，则必须证明如果想证明一个协议具有某种属性，则必须证明所有的结束状态都具有该属性。所有的结束状态都具有该属性。v符号执行也可以看作是一种可达性分析方法。符号执行也可以看作是一种可达性分析方法。 9/17/202464协议验证技术第第 4 讲：协议验证技术讲：协议验证技术4.1 概述概述4.2 协议性质协议性质4.3 可达性分析可达性分析4.4 不变性分析不变性分析4.5 逻辑证明逻辑证明4.6 其它验证方法其它验证方法9/17/202465协议验证技术其他验证方法其他验证方法v协议综合协议综合(SYNT: Synthesi
77、s) 协议综合通过构造设计规则来自动产生正确的协议。协议综合协议综合通过构造设计规则来自动产生正确的协议。协议综合将协议设计和协议验证紧密结合起来将协议设计和协议验证紧密结合起来。它力图使用一组能够确。它力图使用一组能够确保所产生的协议是正确的规则，由保所产生的协议是正确的规则，由“协议零部件协议零部件”装配出一个装配出一个符合要求的目标协议，或由协议的需求描述生成一个目标协议。符合要求的目标协议，或由协议的需求描述生成一个目标协议。这种方法常常采用交互式的规范和验证系统来保证所产生的规这种方法常常采用交互式的规范和验证系统来保证所产生的规范的正确性。范的正确性。v模拟模拟(SIM: Simu
78、lation) 模拟通过协议规范的执行来获得协议行为的描述。这种方法一模拟通过协议规范的执行来获得协议行为的描述。这种方法一般用于复杂协议的验证。这些复杂协议的状态空间巨大，以致般用于复杂协议的验证。这些复杂协议的状态空间巨大，以致于很难用可达性分析来实施验证。一般的模拟只涉及到协议状于很难用可达性分析来实施验证。一般的模拟只涉及到协议状态空间中的部分状态。如果模拟涉及到所有的状态，则相当于态空间中的部分状态。如果模拟涉及到所有的状态，则相当于可达性分析，这种模拟称为穷尽性模拟可达性分析，这种模拟称为穷尽性模拟(Exhaustive simulation)。 9/17/202466协议验证技术
79、其他验证方法（其他验证方法（Cont.）v规范执行规范执行(SPE: Specification Execution) 如果协议规范是用可执行的规范描述语言写的，则如果协议规范是用可执行的规范描述语言写的，则可以通过执行协议规范来验证协议的性质。当然，可以通过执行协议规范来验证协议的性质。当然，规范执行需要一个语言解释器。在软件工程中，这规范执行需要一个语言解释器。在软件工程中，这种方法也称为快速原型种方法也称为快速原型(rapid prototyping)。 v混合方法混合方法(HT: Hybrid Technique) 就协议规范而言，可达性分析和程序证明两种方法就协议规范而言，可达性分析
80、和程序证明两种方法的混合方法能够充分利用这两种技术的优点。用状的混合方法能够充分利用这两种技术的优点。用状态模型来描述协议的主要状态，从而使状态空间保态模型来描述协议的主要状态，从而使状态空间保持在比较小的水平，因而可以用一些自动分析方法持在比较小的水平，因而可以用一些自动分析方法来分析协议的一般性质。对于特殊性质，可以利用来分析协议的一般性质。对于特殊性质，可以利用由变量和过程组成的断言的证明来处理。由变量和过程组成的断言的证明来处理。 9/17/202467协议验证技术验证技术功能比较验证技术功能比较 9/17/202468协议验证技术协议验证：思考题协议验证：思考题v试试分析滑动窗口协议，找出一到二个滑动窗口分析滑动窗口协议，找出一到二个滑动窗口协议的不变式来。协议的不变式来。v撰写一篇关于状态空间爆炸问题的综述文章。撰写一篇关于状态空间爆炸问题的综述文章。（参考文献（参考文献98-4(StateSpaceExplosion).ps）9/17/202469协议验证技术
