协议工程中的协议验证技术

协议工程中的协议验证技术

随着计算机通信和网络技术的发展，网络技术的复杂性与日俱增，主要体现在网络技术的开发难度大、周期长、存在许多潜在错误。在协议开发过程中，任何错误和错误都会给系统的稳定、可靠性、强度、安全性、容错性和不同系统之间的沟通带来重大影响。因此，就合同工程的实施过程，合同工程的正式方法进行了描述。然而，与传统软件安全方法相比，合同设计方法是相对应的。整个协议开发过程是一体化的、系统化的和形式的。协议工程包括形式化描述、协议验证、协议综合、协议实现、协议一致性测试等多方面的理论和技术.在这些形式化技术中,形式化描述与验证技术是整个协议设计与实现的基础,对协议实现的正确性、完整性和复杂度有至关重要的影响.对协议本身的逻辑正确性进行校验的过程称之为验证.协议验证有两种途径:协议分析和协议综合,通常所说的协议验证指的是前者.协议分析的目的是:对已设计的协议进行分析和校验(这些已设计的协议大都是采用非形式化设计方法产生的).协议的正确性验证试图在协议开发的前期最大限度地检测和纠正协议错误和缺陷,包括死锁、活锁、不可执行的行动、协议外部性能不符合服务要求等.协议验证技术多种多样但可以分为三类:可达性分析是最常用的技术,它包括状态穷举、状态随机枚举、状态概率枚举等方法;逻辑证明试图用推理演算方法严密地证明协议的各种性质,采用的推理演算技术主要来自于时序逻辑、谓词逻辑、代数演算等数学领域;第三类验证技术是模拟.协议综合将协议设计和协议验证紧密结合起来,也可以认为是一类验证技术.关于协议的形式化方法,目前已研究开发出多种形式模型,概括起来主要有以下几种:有限状态机FSM(FiniteStateMachine)、Petri网PN(PetriNet)、时序逻辑TL(TemporalLogic)、通讯系统演算CCS(CalculasofCommunicationSystem)、形式文法FG(FormalGrammar)、过程语言PL(ProceduralLanguage)等数学模型和逻辑模型.本文主要研究基于前三种模型的通信协议验证技术.1限次转换之后达到的状态有限状态机FSM是最为重要的一种形式描述技术,是很多形式化方法的基础.它直观性强,可实现与其它形式方法的组合和转换,且易于自动实现,因而在FDT中占有重要的地位.有限状态机最常用的技术是可达性分析技术.可达性分析技术试图产生和检查协议所有或部分可达状态.所谓可达性状态指协议从状态开始经历有限次转换之后达到的状态,所有可达性状态构成可达图.可达性分析最重要的工作是产生和检查可达图,判断是否存在死锁、活锁等协议错误,它涉及三个重要技术:(1)怎样找出所有可达图,构成可达图;(2)怎样检测死锁、活锁等协议错误;(3)怎样解决状态爆炸问题.一般来说,对于每次发生的转变,可通过使用系统全局状态来决定特性,像是否表示一个死锁状态,所有实体是否在当前状态能接收发给它的所有报文等.基于FSM描述的协议验证可通过构造可达树来实现.可达树的根为系统的初始状态.从初始状态出发,列举出全部可能的转移,每一个转移将产生一个新的状态空间,即形成可达树的一个叶节点,产生一个叶节点的过程叫一次扰动过程.在此叶结点的基础上,不断生长新的叶节点,直到没有新的叶节点为止.可达树上各节点分别表示某一给定时刻的全局状态矩阵(GMS),它动态地反映了两个或多个协议实体或进程的交互活动.FSM由于简单、直观而得到广泛应用,但不利于协议验证的实现,不易于描述复杂的系统.2petri网的可达性分析一组通信实体可以描述为单一的或成组的相互通信的Petri网模型,网间通信由直接耦合或者由库所和变迁表示的通道实现.网络的动态特性如控制和数据流由发生规则和标记分布描述.为适应不同规范集验证的需求,从基本Petri网模型衍化出许多扩展模型系统,如谓词/动作Petri网、时间Petri网(TPN)、带时态逻辑的Petri网、有色Petri网(XCPN)、面向对象Petri网(NPN)等.Petri网还没有国际标准,但已得到广泛应用.对于单个特定协议的验证可能涉及专门的技术,而可达性分析和不变量分析是验证大多数协议的基本途径,Petri网模型的许多性质都可以由它们推导出来,这为映射相应协议的性质提供了可能.而Petri网自身具备的可运行性方便了系统形式化描述级模拟.(1)可达性分析是指生成Petri网的全部可达状态,以检查是否符合协议所要求出现的状态以及期望的行为特征,通常包括死锁、意外接受/发送、变迁活性以及库所标记数的有界性等.可达性分析从初始全局标识开始,根据每一个点活变迁或并发变迁集(同时具备点火条件的变迁的集合)生成分支结点,总体上形成可达图.(2)不变量分析研究的是Petri网在特定执行模式下不变量的特性.研究最广泛且理论上最完备的两种不变量是T-不变量和P-不变量.P-不变量对应于Petri网中标记总数保持不变的库所子集,它反映协议的守衡性,如Stop-Wait协议中的发送方、信道和接收方的缓冲器中的报文总数恒为1.T-不变量是指保持网标识不变的变迁序列,它反映协议运作的循环或重复特性.(3)状态爆炸问题.由于状态空间随着模型增长,人们一直试图压缩RG或Petri网的规范.目前主要有保持特性变换和构造/分解理论这两种途径.前者的具体方法是,在保持有界性、活性等Petri网模型特性的前提下,增加生成可达图时的限制条件或在可达性分析之前间接地改变网模型,如用单个库所或变迁代替一个特定子网,建立层次化的可达图或网模型以及基于等价关系削减结点数等.后者的关键问题是如何确定构造和分解Petri网的规则,手段仍然是划分子网,分析网元素的相关性以及建立层次模型等.(4)其他分析功能.由于Petri网具备严格的矩阵运算理论支持,它还能推导出许多系统行为特征,如等价关系、进程等;而Petri网与其他几种形式化描述工具的内在联系使得它能起到模型间的桥梁作用,已经出现许多自动正向/反向翻译Petri网与Estelle或Lotos等语言工具.这里要特别提到的是,因为数学基础是随机过程(排队论),所以,SPN能够用于协议的性能评价,定量地求解系统的主要性能指标,如报文队列长度(库所标记数)、吞吐量和丢包率等.3基于序列逻辑的协议验证和分析3.1电子商务协议的类ban逻辑与模型这种逻辑包含各种关于对分布式系统中消息的知识和信任,或从某些知识得到其他知识和信任的推导规则.最有影响的逻辑系统则属BurrowsM,AbadiM和NeedhamR于1989年提出的BAN逻辑.BAN逻辑形式化定义协议的目标,并且还确定了协议初始时刻各参与者的知识和信任,通过协议里消息的发送和接收步骤产生新知识,运用推导规则来得到目标信任和知识.如果得到最终的关于知识和信任的语句集里不包含所要得到的信任和知识语句时,就表明协议存在安全缺陷.BAN逻辑包含5个推导规则,基本上能表达信任的建立和传递过程,它的定义和规则集合的简洁清晰性与其他相比非常突出.基于逻辑本身的发展规律,这个领域的研究总是围绕逻辑体制的诞生、应用、找缺陷和改进这样一个不断发展和完善的过程.因此,人们在使用BAN时发现其存在这样和那样的缺陷.此后出现了五六种基于BAN逻辑的改进逻辑,一般称之为“类BAN逻辑”,这在IEEE软件工程杂志和IEEE计算机安全工作组会议上有很多研究成果.其中GNY90和AT91逻辑比较受人注意.GNY90拓展了BAN的范围,详细定义了如消息可认证相关的规则,与BAN相比更为全面而细致.但它的规则膨胀到50个,这阻碍了它的应用推广.AT91则以它良好的计算模型和形式语言而受到好评.利用AT91框架,1996年推出了一种用于统一这些类BAN的逻辑被称为SVO逻辑.MB93逻辑则因提出格式化改写协议方法及引入集合概念而独具特色.但BAN类逻辑不适用于分析电子商务协议,原因在于信念逻辑是要证明某个主体相信某一个公式,而可追究性的目的在于某个主体要想第三方证明另一方对某个公式负有责任.为此Kailar提出了新的用于分析电子商务中可追究性的形式化分析方法,简称Kailar逻辑,它是目前电子商务协议中主要的形式化分析工具.但它具有不能分析协议的公平性、对协议语句的解释及初始化假设是非形式化的、无法处理密文等局限性.其他模态逻辑还有CKT5和KPL以及其它几种逻辑.其中CKT5逻辑曾被用于分析NeedhamSchroeder依赖实现的缺陷.另外,对基于时序逻辑的加密协议也有研究.3.2ws自身的发展另一种分析验证协议的方法是利用数学代数理论,使用代数表示协议参与者和敌对方的知识具有前两种方法的优点:自动机模型的精致和模态逻辑对知识发展的推理能力.Meadows在1990年曾尝试使用代数分析描述知识的能力来拓展NRL分析器的推理模型,其应用效果并不理想.近两年来,在这一领域的研究却比较活跃,该方法最早的实现是FDR模型检测器.之后有BrunoDutertre的PVS验证系统.FDR和PVS系统现在应用比较广泛,对协议工程化设计有帮助.另外,在利用数学手段分析认证协议的方法中,还有用Spi演算描述和验证密码学安全协议.不过,这种方法是采用有名字的通道控制域来实现的,不是真正意义上的利用加密技术实现的保密,它的实现代价很高.3.3规制证明方法这是一个新的研究热点,同证明程序的正确性一样,将协议的证明规约到证明一些循环不变式.这方面开始于Kemmerer的InaJo和ITP的研究,这个领域里值得一提的有Paulson的Isabelle证明系统、Bolignana的Coq证明系统、Dutertre和Schneider的PVS证明系统以及Snekkenes的公理证明器HOT.规约证明方法既可手动进行,也可自动证明;自动证明比较复杂,是目前一个发展方向.关于协议验证的研究也是基于规约证明的,其自动化证明需进一步完善.3.4议验证ps上述各种形式的分析协议技术既有各自的应用领域,又有各自的缺陷与不足.主要表现在:(1)基于模型的协议验证具有假定算法强大、攻击者可获得任意信息、安全的不可判定性等特点.(2)基于模态逻辑的分析需要理想化协议,不需秘密确定,既可手动进行,也可自动支持.(3)状态搜索法通常采用模型检测器来查找攻击途径,这种方法有效,但限于有限状态.(4)归纳证明可以手动进行,但工作量大,最好用验证工具.4复杂协议的原因协议验证研究仍在发展中,通常真实的协议难于分析,原因有以下几点:(1)协议描述不精确;