《协议验证技术》PPT课件.ppt

第5章协议验证技术 2 内容提要 概述 1 协议性质 2 可达性分析 3 不变性分析 4 3 协议验证 Holzman 每一个新设计的协议在被完全证明没有错误之前 都应认为不是完全正确的 协议验证技术和形式描述技术是同步发展的 它也是协议工程技术中研究最早 最深入的课题 使用的技术方法多种多样 4 验证的含义 验证 的含义 验证协议的设计 通过分析每一层的所有协议实体间的所有可能的交互 协议的抽象规范中所确定的功能以及通过低层提供的服务所实现的对等层间的通信来确定上述操作是否满足协议的服务规范 在设计阶段进行验证 可以及早发现协议错误 大大降低协议开发成本 验证协议的实现 检查每一个协议实体的实现是否满足它的抽象协议规范 大多数情况下 协议实现的验证是通过不同的测试工具来实现的 有时也将其称为协议实现评估或协议的一致性测试 一般情况下 协议验证指的是第 1 类验证 这也是本课程的观点 具体来说 协议验证是指根据协议规范来检查协议实体间的交互是否满足一定特性 properties 或条件 conditions 的过程 例如 检查是否有死锁存在 通过协议验证 可以获知协议设计是否满足正确性 完整性和一致性等要求 5 VerificationandValidation 在英文文献中 验证 一词有两种不同的表示 validation和verification 它们的含义也比较混乱 文献 Rud98 认为 validation主要是指检查协议逻辑上的一致性 以查实协议设计中是否存在某些错误 这些错误是所有协议中都可能存在的共性错误 与具体的协议功能无关 例如 验证有无死锁 而verification则是指检查协议是否能成功地提供指定的协议功能 文献 Lai98 认为 verification主要是指检查一个系统是否满足它的规格说明 而validation的含义则不仅包括verification 还可能包括对最终的系统实现进行测试 系统模拟 性能分析预测等 6 VerificationandValidation Bohem Verification toestablishthetruthofcorrespondencebetweenasoftwareproductanditsspecification truth orarewebuildingtheproductright Validation toestablishthefitnessorworthofasoftwareproductforitsoperationalmission tobeworth orarewebuildingtherightproduct 谢94版网络书中介绍 Verification 在功能方面进行验证Validation 在语法方面进行证实在实践当中 validation和verification所采用的技术并没有明显的界限 也正因为如此 很多文献并没有严格区分validation和verification 而是混用这两个单词 7 VerificationandValidation 8 形式化验证 非形式化验证则主要通过传统的遍历 walkthrough 和代码检查 inspection 来实现 协议验证通常与形式描述技术有关 形式化验证主要将形式描述技术和推理技术相结合 是形式化描述技术的一个重要方面 其优点是 一方面可以获得无二义性的协议规范 另一方面可以通过计算机辅助工具来帮助实施自动或半自动验证 协议设计者必须在早期的协议设计阶段采用一些技术或工具来发现设计中存在的错误 这也是协议验证的最重要的目的 9 形式化协议验证 主要两类方法 模型检测 ModelChecking 基于状态搜索 StateExploration 演绎验证 DeductiveVerification 基于定理证明 TheoremProving 10 模型检测方法 步骤 建模 Modeling 描述 Specification 验证 Verification 问题 状态空间爆炸协议运行的无穷状态空间的不可搜索性协议运行过程中的无穷消息空间的不可搜索性 11 定理证明方法 步骤 将实现方案和功能描述都转换为一种形式逻辑 如命题逻辑 一阶逻辑 FirstOrderLogic FOL 高阶逻辑 HigherOrderLogic HOL 等建立公理系统 作为验证的依据 并将协议性质构造成一组代定数定理根据公理系统 使用定理证明器 通过逻辑推理 逻辑规约等手段 构造证明过程 证明实现方案和功能描述等价问题 入门难 前两步难 12 内容提要 概述 1 协议性质 2 可达性分析 3 不变性分析 4 13 协议性质 协议验证的最主要内容是检查协议是否满足规定的协议性质 一般情况下 将协议性质分为两类 一般性质 generalproperties 指所有协议所具有的一些公共特性 不同文献对这类性质的个数和描述也不尽相同 特殊性质 specificproperties 是指与具体协议内容有关的性质 对这些性质的定义构成了服务规范的主体内容 也有文献将协议性质分为安全性 safety 和活跃性 liveness 14 一般性质 可达性 Reachability 验证协议的各种可能状态之间的可达关系 如果协议的某个状态从初态不可达 则表明协议有错误 如果从状态A到状态B的变迁不可能发生 直接或间接 则从状态A到状态B是不可达的 没有死锁 Deadlockfreeness 最典型的死锁是协议中各实体都处于这样的一种等待状态 即只有在 某一事件 发生后才能做进一步的动作 但在该状态下 这个 某一事件 却不可能发生 死锁发生时 协议所处的状态称为死锁状态 没有活锁 Livelockfreeness 活锁是指协议处于无限的死循环中 而没有别的事件可使协议从这一循环中解脱出来 例如 协议无限制地执行超时重发操作 但总是收不到对方的确认信息 状态还是在变化的 不过不能脱离这种死循环状态而已 15 一般性质 Cont 弱活锁 Weaklivelock 是指协议处于死循环中 只有当协议交换命令的相对速度达到某一状态时 协议才退出死循环 时间相关的活锁 Time dependentlivelock 也称为临时阻塞 Tempo blocking 它是指协议处于死循环中 但是当通信双方交换报文的相对速度到达某一状态时 协议可以从死循环中出来 有界性 Boundedness 检验协议的某些成分或参数的容量 例如 通道容量 窗口大小 是否有界 有界性是针对协议元素性质和通道性质而言 可恢复性或自同步性 Recoveryfromfailures 这是当出现差错后 协议能否在有限的步骤内返回到正常状态 包括初始态 执行 16 一般性质 Cont 无状态二义性 Stateambiguitiesfreeness 一个进程在某一时刻只允许具有一个稳定状态 所谓稳定状态是指当通信双方的通道为空时的进程状态 若在某一时刻进程可以有多个稳定状态 则称该进程的状态为二义状态 互斥性 Mutualexclusion 互斥性是指有些协议动作不能同时被多个用户执行 例如 多个用户不能同时请求同一资源 终止或进展 TerminationorProgress 是指协议提供的服务必须在有限时间内完成 终止是针对终止协议 terminatingprotocols 而言 意思是指协议总是能到达期望的结束状态 而进展则是针对循环协议 cyclicprotocols 而言 意思是指协议总是能到达它的初始状态 17 一般性质 Cont 无冗余描述 AbsenceofOverspecification 协议规范中没有无用的 冗余描述 例如 没有未经实践的报文接收 absenceofunexercisedmessagereceptions 公平性 Fairness 是指每一个协议实体均应平等地得到运行的机会 无论其它的协议实体想做什么 18 特殊性质 完整性 Completeness 是指协议设计考虑了所有可能发生的事件 选项以及服务 检验协议是否能处理所有可能的输入 即是否缺少应用的处理 或有无非期待的接收或输入 即错收 也有的文献将完整性称为完全正确性 completecorrectness 一致性 consistency 是指协议服务行为 或性质 和协议行为 或性质 一致 即协议应该提供用户要求的服务 而无需提供用户没有要求的服务 也有文献将一致性称为部分正确性 partialcorrectness 等价性 equivelence 等 19 一般性质vs 特殊性质 协议验证着重在于一般性质 而协议测试则着重于特殊性质 20 安全性 safety vs 活动性 liveness 安全性是指协议的所有动作均需与它的服务规范保持一致 即没有不期望的情况出现 不期望的情况包括 不可接收的事件 不可进一步向前的状态 错误的动作 错误的条件 变量值越界等 例如 如果传输协议传送报文 则它必须将这些报文传送到正确的目的地 按正确的顺序 并且无差错地交给目的主机 安全性保证协议不出现错误 活动性是指在有穷时间内 完成规范所规定的动作 或所有的服务必须在有限时间内完成 在进行逻辑验证时 确保一个有限的时延就足够了 但是 在验证协议的效率和响应能力时 则必须定量地确定期望的时延 吞吐率以及其它的一些指标 21 安全性 safety vs 活动性 liveness 活动性 Cont 协议的活动性体现在终止性 termination 和进展性 progress 两个方面 终止性是指协议从任何一个状态开始运行 经过有限时间总能正确地达到终止状态 进展性是指协议从初始状态运行 经过有限时间总能到达指定状态 在某些情况下 终止状态和初始状态是同一的 这样 协议从初始状态出发总能正确地回到初始状态 并可反复运行 22 内容提要 概述 1 协议性质 2 可达性分析 3 不变性分析 4 23 协议验证方法 验证方法主要有两类 模型检查 ModelChecking 最常见方法 可达性分析 RA Reachabilityanalysis 它包括状态穷举 状态随机枚举 状态概率枚举等方法不变性分析 invarianceanalysis 等价性分析 equivalenceanalysis 重要问题 状态空间爆炸证明 Proving 试图用推理演算方法严密地证明协议的各种性质其他方法 模拟 Simulation 通过一些模拟试验来测试协议的各种性质 24 可达性分析 一 概述 25 可达性分析 可达性分析是最常用的协议验证方法 它试图产生和检查协议所有或部分可达状态 可达状态 是指协议从初始状态开始经历有限次转换之后可达到的状态 所有可达状态构成可达图 RG ReachabilityGraph 26 可达性分析 Cont 可达性分析的原理是 采用穷举法检查同一层内两个或多个协议实体间所有可能的交互所产生的状态 将协作的协议实体的状态以及连接这些协议实体的低层称为系统的全局状态或混合状态 compositeorglobalstate 从一个给定的初始状态开始 所有可能的变迁 用户命令 超时 报文到达等 产生许多新的全局状态 对每一个新产生的状态重复执行上述过程直到没有新的状态产生 某些变迁将导致系统返回到已产生的状态 对于一个给定的初始状态和一组关于低层协议的假定 提供的服务的类型 这种分析能够确定协议可能产生的所有结果 27 可达性分析 续 可达性分析最适合于用状态变迁模型描述的协议模型 对于状态变迁模型的全局状态空间的产生也比较容易自动化 目前已有很多作此用途的工具 对于程序语言描述的协议模型也可以使用可达性分析方法 具体做法是 在程序中设置许多断点 breakpoints 这些断点有效地定义了系统的控制状态 可达性分析方法特别适用于验证上一节提到的协议的一般性质 因为这些性质是可达图结构的一种直接结果 没有出口的全局状态要么是死锁 要么是期望的结束状态 同样 收到一个没有定义如何处理的报文或超过了传输媒体的带宽等情况很容易被发现 28 可达性分析 Cont 可达性分析涉及三个重要技术 怎样找出所有可达状态 构成可达图 怎样检测死锁 活锁等协议错误 怎样解决状态空间爆炸问题 29 可达性分析 二 可达性分析算法 30 可达性分析算法 文献 Holz93 给出了三个主要的可达性分析算法 穷尽性可达性分析算法 exhaustiveorfullsearch 受控部分搜索算法 controlledpartialsearch 随机模拟算法 randomsimulation 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中 analyze 从W中删除q 工作集W控制系统状态空间树的搜索顺序 如果工作集W中的状态以先进先出 FIFO 的顺序取出 那么算法执行的是状态空间树的先广搜索 breadth first 如果以先进后出 FILO 的顺序取出 则是状态空间树的先深搜索 deapth first 先深搜索方法占用存贮空间小 这是其最大优点之一 假定每个状态有两个后继状态 算法执行m步之后 对于先深搜索方法 W的长度为m 而对于先广搜索方法 W的长度为2m 32 算法一 穷尽性可达性分析算法 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中 analyze 从W中删除q 33 算法一 穷尽性可达性分析算法 上述算法假定用来进行验证的计算机的存贮空间足够大 且计算速率足够高 这往往是不现实的 因此 大多数情况下 只有将协议验证模型化简到给定机器能够分析的程度时基于这种算法的验证才可行 一般采用结构化或分层的方法来降低模型的复杂性 但在某些情况下 由于被分析的问题的固有复杂性 只能将模型化简到一定程度 因为如果再进一步化简则可能丢失其基本的 重要的性质 由此产生了另外一种搜索算法 即受控部分搜索算法 34 算法二 受控部分搜索算法 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 bounds 散开搜索 ScatterSearch 定向搜索法 GuidedSearch 概率法 ProbabilisticSearch 启发式 Yu91 随机选择法 RandomSelections West87 状态矢量法 Holz91 等 算法不考虑检查协议所有可能的状态 而是预先确定满足某些要求 如 死锁 的潜在的全局状态 然后检查这些状态是否可达 35 算法二 受控部分搜索算法 限制深度法 原理是限制被分析的执行序列的长度 从而只需分析协议行为的一个子集 实质上 限制了完全搜索算法中的工作集W的大小 限制深度法是一种相当标准和简单的部分搜索技术 散开搜索法 原理是尽可能选择有可能导致死锁的执行序列来进行检查 从而增加尽快发现错误的概率 例如 死锁的一个前提条件是没有待处理的报文 通道为空 因此 这种算法更可能去检查报文接收操作而不是发送操作 定向搜索法 在定向搜索法中 为每一个后继状态计算它的代价函数值 costfunction 然后 根据这个计算结果作为是否执行它的依据 代价函数在搜索过程中可以动态地改变 如果代价函数是固定的 则相当于散开搜索法 目前 被证明有用的代价函数或定向表达式还不多见 36 算法二 受控部分搜索算法 概率搜索法 在这种方法中 根据状态出现的概率的递减顺序来选择后继状态 将系统中的所有变迁都标上标签 最简单地处理就是打上 高 或 低 标签 分别表示出现概率的高低 然后 根据标签来选择要检查的状态 随机选择法 前几种方法总是试图预测在何处最容易发现协议错误 这种预测是有很大风险的 因为根据Murphy定律的推论 错误最可能隐藏在设计者或验证者认为不像有错误的地方 Holz93 随机选择法不关心在哪些状态最可能发现错误 而是随机地选择后继状态 它不仅是一种最容易实现的技术 也是一种最有可能产生高质量的搜索的方法 37 算法二 受控部分搜索算法 一般来说 受控部分搜索算法较全局搜索方法有效和可行 但是 这种方法不能保证协议无错 通常需要执行多次才能得到比较可信的结果 38 算法三 随机模拟算法 前面介绍的受控部分搜索算法部分地解决了穷尽性可达性分析算法的状态爆炸问题 因而得到了广泛的应用 但是 在有些情况下 这种受控部分搜索算法也会变得不可行 例如 如果想直接将一个协议验证算法应用到一个高度详细的 正在一台机器上运行的 经编译过的代码上时 即使是使用受控部分搜索算法也需要大量的内存来保存搜索的状态 在这种情况下 惟一可行的方法是从搜索算法中去掉状态集A和W 而用随机模拟 randomsimulation 或随机遍历 randomwalk 的方法搜索协议的状态空间 39 算法三 随机模拟算法 analyze 随机模拟 q 初始状态 while 1 if q 错误状态 report error q 初始状态 elseq q的一个后继状态 40 三种算法的比较 穷尽性可达性分析算法的优点在于可以证明协议中没有错误 但问题在于其应用范围有限 最主要原因是该算法能分析的最大状态数目依赖于协议 描述方法和可用的计算资源 特别是当系统状态的数目非常大时会发生状态空间爆炸 一般来说 根据协议状态空间大小和可用的内存空间 这种算法的覆盖率并不一定能达到100 如果状态空间大小为R 执行搜索时内存中能够存储的最大状态数为A 那么只有当R小于等于A时覆盖率和搜索质量才能达到100 当R大于等于A时 全搜索策略将变成部分搜索 且不能保证检查协议中最重要的部分 覆盖率减小到A R 而搜索质量变得更差 因此 对于复杂的协议 穷尽性可达性分析的效果只能算作是一种低质量的部分搜索 41 三种算法的比较 Cont 受控部分搜索算法的目的是证明错误的存在 而不是证明没有错误 与穷尽性可达性分析相比 这种算法可以有效地解决状态空间爆炸问题 同时利用有限的资源来验证协议的最重要的部分 从而最大限度地发现错误 其缺点是必须能够预先判断出协议中的错误的大概位置 然而这很难预先做到 因为 多个进程间的关系非常复杂 不能仅仅根据其表面的关系来判断 另外 虽然这些方法能够减小状态空间的大小 但它们都没有提供任何工具 将状态空间的大小与可用内存相匹配 使用这些方法时 有效搜索的部分状态空间的大小是协议相关的 只能通过实验确定 要想找到一种最优的方法 必须按照不同的选择策略进行多次验证 42 三种算法的比较 Cont 随机模拟算法与协议系统的大小和复杂性无关 即使是无限大小的系统 也可以应用 因此 对于复杂的验证问题 这种算法也许是唯一可用的方法 但这种方法也有些问题 例如 它没有明确的终止 无法判断是否已经访问过系统的所有可达状态 由于没有算法的终止 也就无法判断是否已经发现了系统的所有错误因此只能发现协议中的错误 而不能证明协议中没有错误 43 可达性分析 三 基于可达性分析的协议错误的检测方法 44 协议错误的检测 死锁 如果一个状态无任何后继状态 那么该状态就是死锁状态 无意义事件 在穷尽可达性分析中 如果一个事件未被执行一次 那么该事件可判定为无意义事件 对于非穷尽可达性分析 算法在执行一遍之后 如果某些事件未执行一次 那么在第二遍执行中应将这些事件的优先级别数值提高 只有当非穷尽可达性分析进行多次之后 才能判定哪那些事件为无意义事件 45 协议错误的检测 Cont 非确定的输入事件 如果某个协议实体在执行输入事件之后所获取的报文不是它所期待的报文 那么这个事件为非确定输入事件 非确定输入事件反映协议的完整性不好 即协议没有考虑异常报文的接收处理问题 活锁 活锁的检测首先是循环的检测 当所有循环都已检测出来之后 我们就可以判定那些循环是死循环 死循环的判定是较为复杂的问题 一种方法是通过 进展状态 progressstate 的标记来确定一个循环是否为死循环 如果循环序列之内包含致少一个进展状态 那么它就不是死循环 进展状态的标记在可达性分析进行之前由手工进行 例如 发送 超时 再发送构成一个循环 如果发送之前判定发送次数是否超过给定数值 超过就转向错误处理 那么再发送状态就可以标记为进展状态 46 可达性分析 四 状态空间爆炸问题 47 状态空间爆炸问题 随着协议复杂性的提高和队列通道边界值的增大 状态爆炸问题使穷尽可达性分析无法进行 除了前面介绍的部分搜索算法 还可以采用下列方法来减小状态空间使之处于一个可控制的范围之内 部分规格说明和验证 PartialSpecificationandVerification 选择大的动作单元 ChoosingLargeUnitsofActions 分解或划分 DecompositionorPartitioning 按断言来分类状态 ClassifyingStatesbyAssertions 48 部分规格说明和验证 根据具体描述方法的特点 只选取协议的某些方面进行描述 例如 在用状态变迁图来描述协议时 常常只描述主要状态间的状态变迁规则 而忽略参数值和其它的状态变量等细节 49 选择大的动作单元 状态空间爆炸是因为不同实体执行的动作相互交织所造成的 我们可以通过合并一些状态或动作来减少状态及变迁数 例如 可以将协议数据的准备和发送看作是一个不可分割的动作 从准备到发送不需同其它实体交互 从而可以将这样一个动作看作是一次 状态变迁 这种方法的一个特殊应用例子是 仅仅考虑传输通道为空时的状态 即发送方发送的报文立即能够到达接收方 当要传输的报文的数量比较小或不考虑传输时延时 这种 空通道抽象 是合理的 在这种情况下 可以将不同实体的发送和接收变迁合并到一个涉及到两个实体的联合状态变迁中 50 分解或划分 这种方法前提条件是可以将协议分解或划分成多个可控制的阶段 子层或模块 然后 对每一个子层 阶段或模块进行独立地描述和验证 由于分解后的协议组件或阶段的状态及状态变迁数要远小于原始协议 所以这种方法大大降低了对原始协议验证的复杂性 例如 将HDLC分解成以下几个子层 比特填充 校验和过程元素 后者又可以细分为几个组件 需要注意的是 证明了每一个组件或阶段的正确性 并不一定能安全保证原始协议的正确性 51 按断言来分类状态 在可达性分析中 考虑状态类而不是单个状态 通过选择合适的谓词 可以大大减少状态数目 例如 考虑一个协议实体接收编号的信息帧 不考虑将序列号变量的各种可能的值看作是不同的状态 取而代之仅仅考虑三种状态 变量 小于 等于 大于 收到的信息帧的编号 52 内容提要 概述 1 协议性质 2 可达性分析 3 不变性分析 4 53 不变性分析 如果一个系统的某个性质能用一个确定的逻辑表达式描述 并且恒为真 不随系统的状态变化或执行序列而改变 那么这个性质称为系统的不变性质 简称为系统不变性 systeminvariance 协议不变性分析包括二个工作 第一是完全正确地找出系统 协议 的不变性质 形成严格定义的不变性逻辑表达式 这项工作由手工进行 许多协议描述文本也包含了不变性表达式 第二是以某种方式执行协议 验证不变性表达式是否恒为真 我们所说的不变性分析指的是第二项工作 54 不变性分析 不变性分析可采用两种途径 不变性证明系统 通常采用归纳法 不变性监测系统 55 不变性证明系统 采用归纳法时 协议不变性证明包括两步 验证协议处于初始状态时不变性表达式是否成立 然后 假定协议在某状态下不变性成立 验证协议从这个状态开始执行所有相关事件过程中不变性是否保持成立 56 不变性监测系统 不变性监测系统借助监测软件和监测方法对模拟运行或符号执行中的协议进行不变性校验的过程称之为不变性监测 invariantmonitoring 这种方法要求在协议代码中插入断点 子程序的调用或返回可视为自然断点 每个断点处 监测系统取相关变量值 计算并校验不变性表达式是否成立 通过监测系统进行不变性分析时 还会遇到一个麻烦问题 协议系统由多个协议实体组成 分布性 监测系统必须凌驾于它们之上 实现起来比较困难 由于上述这些问题和原因 不变性分析在协议验证中的应用受到很大限制 57 系统不变式vs 断言 不变性监测程序还可对程序断言 assert 进行校验 程序断言是嵌于协议代码指定