5 协议验证技术 (ok).ppt

第五章协议验证 分析 技术 5 1概述对协议本身的逻辑正确性进行校验的过程称之为协议验证 protocolverification 协议验证有两种途径 1 协议分析 protocolanalysis 2 协议综合 protocolsynthesis 通常所说的协议验证指的是前者 协议综合 将在第六章讨论 将协议设计过程和协议验证 分析 过程融合在一起 它通过一组能确保所设计的协议是正确的规则 从一些基本协议模块中 这些基本模块已证明是正确的 产生所希望的目标协议 协议分析的目的是 对已设计的协议进行分析和校验 这些已设计的协议大都是采用非形式化设计方法产生的 第五章协议验证技术 协议分析包括许多方法 例如 1 可达性分析 reachabilityanalysis 2 不变性分析 invarianceanalysis 3 等价性分析 equivalenceanalysis 4 符号执行 symbolexecution 模拟 simulation 等等 这些分析工作可以手动完成 协议有多种表达形式 这包括 用自然语言描述的非形式化协议文本 用形式描述语言 ESTELLE LOTOS SDL等 描述的协议规范 用协议模型技术 FSM Petrinet CCS等 表达的协议模型 以及用程序设计语言 C Pascal等 描述的协议代码 协议分析可在任何一种表达形式上进行 一般地说 上述所有方法都可在这几种表达形式上进行 手工或软件工具 然而 除符号执行之外 人们都在协议模型上进行协议分析 简单 容易形成确定算法 本章讨论三种分析方法 它们是可达性分析 不变性分析和等价分析 第五章协议验证技术 5 2可达性分析可达性分析 基于FSM模型技术 试图产生和检查协议所有或部分可达状态 所谓可达状态指协议从初始状态开始经历有限次转换之后可达到的状态 所有可达状态构成可达图 reachabilitygraph 可达性分析的最重要工作是产生和检查可达图 判定是否存在死锁 活锁等协议错误 可达性分析涉及三个重要技术 1 怎样找到所有可达状态 构成可达图 2 怎样检测死锁 活锁等协议错误 3 怎样解决状态爆炸问题 第五章协议验证技术 5 2 1穷尽可达性分析穷尽 exhaustive 可达性分析产生和检查所有协议状态 算法5 1描述了穷尽可达性分析的基本算法 该算法假定计算机的存储空间足够大 计算速度足够高 第五章协议验证技术 算法5 1 exhaustivereachabilityanalysisstart W initialstate 工作集 将被分析的状态A 被分析过的状态analyze 穷尽分析 analyze if W empty return q lastelementfromW 集合W包含未被分析的协议状态 A包含已分析和正在分析中的协议状态 算法执行之前 W包含initialstate A为空 算法执行完毕之后 W为空 A包含协议的所有可达状态 该算法简单明了 然而要将它付诸实施时 我们还必须解决以下一些问题 addqtoA findallsuccessorssofq if q error state report error else foreachsuccessorstatesofqif sisnotinAorW addstoW analyze deleteqfromW 第五章协议验证技术 1 状态表示方法协议状态用状态矩阵表示为 这里E1 E2 En 为n层协议的几个协议实体的局部状态 Cij为协议实体i到协议实体j的通道的状态 当所有通道可处理成空通道时 协议状态可用数组 E1 E2 En 表示 因为空通道只有一种状态 第五章协议验证技术 2 怎样找到所有可达的后继状态不考虑报文顺序号 AB协议系统如图5 1所示 其中C12是S到R的通道 C21是R到S的通道 协议状态由二维矩阵组成 初始状态有四个后继状态 很显然 状态 2 3 和 4 不是可达状态 因为初始状态中AB内部没有任何数据需要传输 所以 2 3 4 状态是不可能出现的 即不可达的 那么怎样判定 1 是可达状态 而 2 3 和 4 不是可达状态呢 第五章协议验证技术 图5 1AB协议系统 第五章协议验证技术 为了解决这个问题 我们按下述格式定义交互事件 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 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 利用作用点状态判定在协议状态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 R 1 B 0 m通道内的事件无需表示出来 通道C12的drop事件叠加到事件 6 中 第五章协议验证技术 如果通道为队列通道 它的状态定义就会变得复杂 状态数也会激剧增加 事件的表述方法也变得复杂 例如 对于边界为n的队列通道 事件表述形式可能为 entity state channel state n message 就是说 当通道队列长度小于n时 协议实体entity才会执行报文发送事件 第五章协议验证技术 4 搜索方法算法5 1的搜索方法取决于W队列性质 如果W为FIFO 先进先出 队列 搜索是按宽度优先 breadth first 进行的 如果W为FILO 先进后出 队列 搜索是按深度优先 depth first 进行的 深度优先搜索方法占用存贮空间小 这是最大优点之一 假定每个状态有两个后继状态 算法执行m步之后 对于深度优先搜索方法 W的长度为m 但对于宽度优先搜索 W的长度为2m 第五章协议验证技术 5状态爆炸和错误检测第三章在讨论FSM简化时提到了什么是状态爆炸问题 随着协议机制复杂性的提高和队列通道边界值的增大 状态爆炸问题使穷尽可达性分析变得无法实行 5 2 2讨论的非穷尽可达性分析技术力图解决这个问题 算法5 1中的语句 if q error state report error 其内容非常丰富 实现比较困难 5 2 3讨论各种协议错误的检侧方法 第五章协议验证技术 算法5 2 start W initialstate A analyze analyze If W empty return q elementfromW addqtoA 5 2 2非穷尽可达性分析将算法5 1的语句foreachsuccessorstatesofq改为forsomesuccessorstatesofq 其它语句不变 我们就得到非穷尽可达性分析算法 findallsuccessorssofq if q error state report error else forsomesuccessorstatesofqif sisnotinAorW addstoWanalyze DeleteqfromW 第五章协议验证技术 1 事件优先选择法事件t1 t2 tn使状态q产生n个后继状态 图5 2 如果给这些事件赋于一定优先级别数值 那么被选择的后继状态 一般只选择一个 应该是优先级别数高的事件产生的 优先级别数值的赋值方法可以是 现在问题是 怎样从q的所有后继状态中选取某些 some 状态进行分析 当然 被选取的状态应该是最有价值的 最有分析意义的 能最大可能检测协议错误的状态 1 静态赋值可达性分析进行之前 按照一定原则 发送事件优先于接收事件 协同事件高于内部事件等等 对所有事件赋于静态优先数值 可达性分析过程中 这些数值不改变 2 动态赋值可达性分析执行之前 所有事件赋于相同的优先数值 也可以不同 可达性分析过程中 事件每执行一次 其优先数减1 这种方法可均衡各个事件的执行次数 使本来很少有机会执行的事件能尽快的执行一次 第五章协议验证技术 第五章协议验证技术 2 协议实体优先选择法如果事件t1 t2 tn是由多个不同协议实体执行的 那么被选择的后继状态应该是优先级别高的协议实体所执行的事件产生的 协议实体的优先级别的赋值方法可以是 1 静态赋值按照一定原则 发方高于收方 响应方高于发起方 等等 赋给各个协议实体优先数值 可达性分析进行过程 数值不改变 2 动态赋值方法之一按照执行事件的多少或最后一次执行事件的时间动态改变协议实体的优先数值 例如 事件执行多的协议实体优先级别数降低 很长时间未执行任何事件的协议实体的优先级别数提高等等 动态赋值方法之二按照事件的相关特性动态调整协议实体的优先级别数值 例如当协议实体A执行完发送事件之后 那么执行该事件的协同事件的协议实体的优先数值就立即提高等等 第五章协议验证技术 3 纯粹随机选择法这是最简单而有效的选择方法 从q的n个后继状态中任取1个或几个进行分析 由于从q的n个后继状态中选择 最有分析价值 的状态是一个不可判定的问题 因此纯悴随机选择方法是一种简单适用的方法 非穷尽可达性分析往往要进行多次 每次的状态选择方法不同 才能得到较满意的结果 第五章协议验证技术 5 2 3协议错误的检测方法可达性分析可检侧死锁 活锁 无意义事件 非确定的输入事件等协议错误 1 如果q无任何后继状态 那么q就是死锁状态 2 在穷尽可达性分析中 如果一个事件未被执行一次 那么该事件可判定为无意义事件 3 对于非穷尽可达性分析 算法在执行一遍之后 如果某些事件未执行一次 那么在第二遍执行中应将这些事件的优先级别数值提高 只有当非穷尽可达性分析进行多次之后 才能判定那些事件为无意义事件 4 如果某个协议实体在执行输入事件之后所获取的报文不是它所期待的报文 那么这个事件为非确定输入事件 非确定输入事件反映协议的完备性不好 即协议没有考虑异常报文的接收处理问题 第五章协议验证技术 6 活锁 死循环 的检测是非常麻烦的事情 活锁的检测首先是循环的检测 在算法5 1和5 2中 如果q的后继状态已在W和A中存在时 那么循环可能存在 采用深度优先搜索方法时 循环容易检测 这是深度优先搜索的优点之二 如果q的后继状态s已在W中 那么s到q的状态序列 依次排列在W中 这是一个循环 作为一个案例分析 我们来检测图5 3的循环 图中状态编号表示深度优先搜索过程中算法所访问的状态的先后次序 状态 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中而是在A中 当算法执行到状态 10 时 10 的后继状态 6 也在A中 前者t4产生循环 后者t5不产生循环 这就说明 如果q的后继状态在A中 循环可能存在 第五章协议验证技术 当q的后继状态在A中时 判定它是否产生循环有两种方法 图5 3循环检测 第五章协议验证技术 1 断点法算法执行多遍 执行第n遍算法时 将前面 n 1 次算法已检测到的循环断开 以便检测新的循环 对于图5 3所示的系统 算法执行第一遍时 由t1 t2和t3产生的循环都能检测出来 执行第二遍算法的时断开 3 4 的转换 那么由t4产生的循环 1 2 8 9 4 5 就检测出来了 注意 第二次算法执行时 搜索顺序不同于第一次 执行第三次算法时再断开 8 9 那么由t6产生的循环 1 2 8 11 9 4 5 就检测出来了 图5 3循环检测 第五章协议验证技术 2 标记法算法执行过程中 每检测到一个循环就给处于循环之中的状态打上 标记 表明它已处于某个循环之中 如果q的某个后续状态不在W中而在A中 并且它已处于某个循环之中 那么是否真正产生了新的循环 还必须做进一步判定 判定规则是 如果q的后继状态s在A中 并且s已处于某个循环之中而且该循环序列的任何一个状态或几个仍然在W中 那么新的循环产生 图5 3中 当算法执行到状态 9 时 它的后继状态 4 在A中 并且已处于两个循环之中 这表明新的循环可能存在 由t3产生的循环的序列 3 4 5 中没有一个状态还处于W中 因此这个循环序列的所有状态不包括在新的循环之中 由t1产生的循环序列 1 2 3 4 5 中 1 和 2 仍然处于W中 因此新的循环序列存在 循环序列由 1 2 3 4 5 组成 当算法执行到状态 10 时 虽然它的后继状态 6 在A中 但由于 6 未处于任何其他循环之中 因此不存在新的循环 第五章协议验证技术 图5 3循环检测 第五章协议验证技术 当所有循环已经检测出来之后 我们就可以判定那些循环是死循环 死循环的判定是更为复杂的问题 一种方法是通过 进展状态 progressstate 的标记来确定一个循环是否为死循环 如果循环序列之内包含至少一个进展状态 那么它就不是死循环 进展状态的标记在可达性分析进行之前由手工进行 例如发送 超时 再发送构成一个循环 如果发送之前判定发送次数是否超过给定数值 超过给定值就转向错误处理 那么再发送状态就可以标记为进展状态 第五章协议验证技术 5 3不变性分析如果一个系统的某个性质能用一个确定的逻辑表达式描述 并且恒为真 不随系统的状态变化或执行序列而改变 那么这个性质称为系统的不变性质 简称系统不变性 协议的不变性分析包括二个工作 第一是完全正确地找出系统 协议 的不变性质 形成严格定义的不变性表达式 第二是以某种方式执行协议 验证不变性表达式是否恒为真 我们所说的不变性分析指的是第二项工作 第一项工作由手工进行 许多协议描述文本也包含了不变性表达式 不变性分析可采用两种途径 第一是不变性证明系统 往往采用归纳法 第二是不变性监测系统 下面分别介绍它们 第五章协议验证技术 5 3 1不变性证明系统用归纳法证明一个数学公式时 证明分两步进行 第一步证明x 0时公式是否成立 第二步 如果x n时公式成立 那么证明x n 1时公式是否成立 类似的 协议不变性证明也包括两步 首先 验证协议处于初始状态时不变性表达式是否成立 然后假设协议在某状态下不变性成立 验证协议从这个状态开始执行所有相关过程中不变性是否保持成立 我们以窗口流控制为例说明其证明过程 案例来自于文献资料 10 本文已作剪辑 第五章协议验证技术 滑动窗口流控制是点对点通讯协议 传输层 数据链路层 所广泛采用的一种流控制方法 发送端维持两个计数器LW和HW LW之值等于第一个未认可报文的顺序号 HW之值为下一次发送报文时能赋予的顺序号 HW和LW之间差为发送窗口 窗口宽度不应大于给定值 所有未认可报文放入ACKQUE队列中 如果收到一个认可报文 发送端将已认可的报文从ACKQUE队列中擦去 并修改LW之值 接收端维持一个计数器NS NS之值为下一个接受报文的顺序号 如果所接受的报文的顺序号不等于NS之值 丢弃该报文 假定报文顺序号为自然数并可以无限增大 那么对于这样一个窗口流控制 我们可形成3个不变性表达式 HW LW windowLW seq elementofACKQUE HWLW NS HW 第五章协议验证技术 这里 window为窗口宽度的最大值 函数seq 的返回值为报文的顺序号 表达式1规定未认可报文的个数必须小于或等于window 表达式2规定ACKQUE队列中的所有报文的顺序号应在窗口范围之内 表达式3规定接收端的NS总是在窗口之内 第五章协议验证技术 SM Sendamessage If HW LW window Seq message HW HW HW 1 sendthemessage putthemessagetoACKQUE RA Receiveanack if theackisOK and LW seq ack HW deleteallmessageinACKQUEwithseq message seq ack LW seq ack RS RE sendmessageaftertimeout SendallmessageinACKQUE RM Receiveamessage If themessageisOK and seq message NS deliverthemesssgetotheuser NS NS 1 SA Sendtheack sendtheackwithseq ack NS TM Transmitamessageoverthechannel themessagemaybelostordestroyed TA Transmitanackoverthechannel Theackmaybelostordestroyed 为了用归纳法证明上述窗口流控制的不变性 我们必须罗列出协议中的所有相关的原子操作 这些原子操作包括 第五章协议验证技术 原子操作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 并且i k j成立 验证发端协议实体发出一个新的报文之后 协议在执行所有相关原子操作之后 表达式3是否成立 SMSM发出顺序号为j的报文之后 HW j 1 LW NS HW 表达式3成立TMTM不改变HW LW和NS的值 第五章协议验证技术 RS如果超时事件产生 重发报文 RS不修改HW LW和NS RM由于SM执行之后HW j 1 当RM执行之后 虽然NS K 1 但表达式3仍然成立 如果所接收的报文顺序号有错 RM不修改NS 因此表达式3成立 SA不改变HW LW和NSTA不修改HW LW和NS TA发出的ACK报文的顺序号为k到j之间任意数值 即seq ck k j RA正确执行之后LW NS seq ck k j 而HW仍然为j 1 因此表达式3成立 如果RA丢弃ack报文 HW LW和NS不变 证毕 第五章协议验证技术 5 3 2不变性监测系统不变性监测系统借助监测软件和监测方法对模拟运行或符号执行中的协议进行不变性校验的过程称之为不变性监测 invariantmonitoring 这种方法要求在协议代码中插入断点 子程序的调用或返回可视为自然断点 每个断点处 监测系统取相关变量值 计算并校验不变性表达式是否成立 除此之外 监测程序还可以对程序断言 assert 进行校验 程序断言是嵌于协议代码指定地方的特殊语句 例如ASSERT state 1 协议代码运行到ASSERT语句时将指示监测程序对assert语句所申明的布尔表达式进行校验 不变性表达式不同于程序断言之处在于它无需插入协议代码之中 第五章协议验证技术 无论是不变性证明系统还是监测系统 我们都认为下述两个问题都是不可判定问题 不变性表达式已完整 准确 严密地表述了协议的所有行为和性质吗 用归纳法证明不变性时 引用的原子操作已覆盖了所有相关操作吗 在监测系统中 所设立的断点完备吗 在通过监测系统进行不变性分析时 我们还遇到一个麻烦问题 协议系统由多个协议实体组成 分布式 监测系统必须凌驾于它们之上 实现起来比较困难 由于上述这些问题和原因 不变性分析在协议验证中的应用受到很大限制 第五章协议验证技术 5 4等价性分析 等价 意味着某种程度上的 相同 和 无差别 如果两个协议模型或协议规范是等价的 那么它们可以互相替换 如果一个是正确的 那么另一个也是正确的 我们在第三章讨论FSM和CCS时已利用 等价 方法简化FSM图和CCS表达式 这实质上也是一种等价性分析方法 等价性分析的另一个途径是证明两个协议的FSM图或CCS表达式是等价的 典型的情况是证明协议规范和它的服务规范一致性 按等价的含义和等价的强弱 等价性分为 20 1观察等价 observationalequivalence 如果对两个协议进行状态到状态的互相模拟时所观察到的协议行为没有差别 这两个协议是观察等价的 本节重点讨论观察等价性 2测试等价 testequivalence 如果对两个协议施加相同的测试序列所观察到的协议行为没有差别 那么这两个协议是测试等价的 第五章协议验证技术 3跟踪等价 traceequivalence 如果两个协议执行的事件序列是相同的 那么它们是踪迹等价的 4实现等价 implementationequivalence 如果一个协议所做的每一件事情都能被第二个模仿 mimic 反之亦然 那么它们是实现等价的 这四种等价按强弱程度排列的话 顺序是 观察等价 测试等价 跟踪等价 实现等价 其中观察等价还分为强观察等价和弱观察等价 等价性的强弱反映两个协议对行为细节的相同程度 等价性越强 它们的行为细节的相同程度越高 第五章协议验证技术 5 4 1基于FSM的观察等价性分析对于状态转换系统 参见第三章3 2节 定义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 4 13 它们的定义如下 1强状态互拟关系 第五章协议验证技术 第五章协议验证技术 图5 4强互拟关系 因为 2 4 均为终止状态 5 5 3 3 为相同状态 a a 第五章协议验证技术 第五章协议验证技术 图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 5 而RW RS 2 3 第五章协议验证技术