基于行为时序逻辑TLA的系统、规则与协议检测的研究

发布时间：2020-06-22 00:59

【摘要】： 为了保证软、硬件系统的可靠安全,包括图灵奖得主A.PnDeli在内的许多计算机科学家都认为,采用形式化方法(Formal Methods)对系统进行形式化验证和分析,是构造可靠安全软件的一个重要途径。模型检测(Model Checking)是形式验证方法中重要的一种。形式化方法原则上就是采用数学与逻辑的方法描述和验证系统。其描述主要包括两方面:一是系统行为的描述,也称建模,通过构造系统的模型来描述系统及其行为模式:二是系统性质的描述,也称规范或规约(Specification),即表示系统满足的一些性质,如安全性、活性等。它们可以用一种或多种(规范)语言来描述。这些语言包括命题逻辑、一阶逻辑、高阶逻辑、时态逻辑、自动机、状态机、代数、进程代数、Pi演算、特殊的程序语言,以及程序语言的子集等。行为时序逻辑TLA由Leslie Lamport提出,行为时序逻辑使得在一个程序中同时表达系统模型及系统属性成为可能。它是时态逻辑的直接扩展版本,它通过公式的形式表达系统模型与属性。而基于TLA的描述语言TLA+是该逻辑的一种时序规约语言,它基于ZF集合理论、一阶逻辑,适用于规约反应式、并发式和分布式系统等等。TLC是对用TLA+描述的并发系统的模型检测工具。有这样一套完整的理论与检测工具,我们就可以开展几个方面的研究。在研究中,我们从三个方向进行,第一个方向是对行为时序逻辑TLA的理论进行深入研究,力求能在理论上有所突破;第二个方向是对现实的系统进行形式化描述与检测;第三个方向是对协议进行形式化描述与检测,通过努力,在三个方向上都取得了一定的认识,但还有许多研究工作需要继续和加强,从而能在基于TLA的形式化分析与检测上取得成绩。在研究中,我们做了如下具体的工作: 1、在基于TLA的并发系统研究中,论文提出可控属性的转移系统。论文首先提出了状态转移条件Γ_c,这样可以对行为A作出限定,然后提出可控行为A_(Γc),由状态转移条件和可控行为这两个定义,进而定义可控状态、可控运迹等等,最后提出了可控属性的转移系统的定义T_c=(Q,S_(cv),(?)_c,Λ_c,Γ_c),并提出和证明在一个可控属性转移系统T_c中,所有的状态是可控状态的。对提出的定义和定理还需要实例来验证。我们从简单的时钟系统、电梯系统、交通系统到网络协议进行了形式化描述与检测。对按可控转移的Needham-Schroeder协议进行形式化描述与检测,结果证明提出的相关理论是合适的。 2、安全性是系统的重要属性,在上面工作的基础上,提出安全转移系统。论文首先提出安全转移条件Γ,安全性确认T,然后提出安全行为A_(Γs),进而定义安全状态、安全运迹等,由此定义安全转移系统T_s=(Q,S_θ,(?)_s,Λ_s,Γ)。提出并证明安全运迹的充分必要条件,及安全系统中的状态是安全状态的。基于所提出的安全转移系统,对网络银行系统进行形式化描述与检测。在形式化过程中,发现银行已经采取种种防范措施使网络银行的安全性有了较好的保障,但在支付过程中,措施相对薄弱,于是提出面向支付的网铬银行安全转移系统。对并发的面向支付的网上银行安全转移系统进行基于TLA+的形式化描述。通过TLC检测,表明基于安全转移系统的网上银行,满足设定的多条安全性质,且在一定程度上增强了并发环境中网铬银行的安全性。 3、对系统进行形式化与检测,其主要目的是进行活性(Liveness Porperty)的检验,Leslie Lamport提出了基于TLA的活性规则,论文对文献中的一些相关规则加以详细地证明,但发现这些规则还不够用。如在对网络协议、网络银行系统研究中,发现一个主体下可以设置多个子主体,如一个服务器可有多个客户端,一个帐号下可设置多个子帐号。它们可以并发地执行一行为。这样的并发系统的多行为的活性规则是怎样的呢? 通过研究,提出了在强、弱公平性下多行为的活性规则MWF1、MSF1、MSF2,这儿条规则对并发系统中多行为的活性进行了归纳,对这儿条规则进行了证明,并在形式化检测中,以网络银行多用户取款行为并发互斥系统为例,用TLA+进行系统描述,并设计对这些规则的检测,检测的结果表明论文提出的强、弱公平性下多个行为者的活性规则是合适的。进而归纳得到多行为者的安全行为在强、弱公平性下的性质规则MWFS1、MSFS1、MSFS2,并加以证明与检测。 4、基于TLA的检测工具AVISPA是2003年元月欧共体支助的重大项目,检测工具基于HLPSL语言进行描述,主要用于网络协议等的形式化与检测,在初步的研究中,对Kerberros协议分四步模型与六步模型进行形式化与检测,通过检测,说明在一定条件下协议是不安全的,并显示出攻击步骤。另一个检测工具TLC2.0是Compaq与Microsoft公司于2003年开发的,工具使用TLA+描述语言,通过对Neeham-Schroeder协议进行形式化与检测,发现Neeham-Schroeder协议在一定条件下可以被中间人攻破。在形式化过程中,首先要对相关协议进行准确地描述与抽象,而后模型化。在对模型的描述中,要描述出通信双方或多方的行为,信息通过设计的通道进行通信,对侵入者的设计,一般设定其可以接受任何信息,并可篡改任何信息。最后要设计检测性质。通过检测发现问题或是相关性质是否满足。通过检测,发现这两个协议在一定条件下,是可以攻破的。相比较而言,使用TLA+语言,要写的基础代码要多些,更适合对系统的形式化与检测,可做到“心中有数”;而使用HLPSL语言进行协议描述,有许多现存的功能可用,对协议的检测能力上表现得更强大。对检测工具的对比研究,包含著名的检测工具SPIN、SMV等等的对比研究,还需做大量的工作。
【学位授予单位】：贵州大学
【学位级别】：博士
【学位授予年份】：2009
【分类号】：TP302.2
【图文】：

运行结果,时钟系统

将上面不同的情况和活性条件加入到一起形成一个完整的电子时钟系统。可以加入性质进行检测，如 :PROPERTIESExistTimesHMSever由于提示占用太多内存而不能检测。如图2.4所示。图2.4运行结果一

运行结果,检测工具

图2.5运行结果二2.8TLC检测工具检测工具TLCZ.o是由ComPaq与Microsoft公司于2003共同研发的基于TLA的检测工具，通过TLc检测工具，可以实现对系统的基于TLA模型化的检测，从而来判断最初的设想并可对系统进行深一步地认识。2.8.1TLC检测形式使用TLC的检测形式如下:P，二g尸口”2_nameoptionssPe‘~万l。其中，Pl卿二，n_nam。尚avatlatk.TLC中检测程序的名字;oPlio邢是检测参数;sPecjle是要检测的文件名。2.9本章小结LeslieLamPortl’一，】提出的行为时序逻辑TLA，具有用一个程序同时表达系统模型与系统性质的特点。本章对行为时序逻辑TLA语法和语义、线性时态逻辑‘公平性、活性、逻辑

【引证文献】