【摘要】： 為了保證軟、硬件系統(tǒng)的可靠安全,包括圖靈獎得主A.PnDeli在內(nèi)的許多計(jì)算機(jī)科學(xué)家都認(rèn)為,采用形式化方法(Formal Methods)對系統(tǒng)進(jìn)行形式化驗(yàn)證和分析,是構(gòu)造可靠安全軟件的一個重要途徑。模型檢測(Model Checking)是形式驗(yàn)證方法中重要的一種。 形式化方法原則上就是采用數(shù)學(xué)與邏輯的方法描述和驗(yàn)證系統(tǒng)。其描述主要包括兩方面:一是系統(tǒng)行為的描述,也稱建模,通過構(gòu)造系統(tǒng)的模型來描述系統(tǒng)及其行為模式:二是系統(tǒng)性質(zhì)的描述,也稱規(guī)范或規(guī)約(Specification),即表示系統(tǒng)滿足的一些性質(zhì),如安全性、活性等。它們可以用一種或多種(規(guī)范)語言來描述。這些語言包括命題邏輯、一階邏輯、高階邏輯、時態(tài)邏輯、自動機(jī)、狀態(tài)機(jī)、代數(shù)、進(jìn)程代數(shù)、Pi演算、特殊的程序語言,以及程序語言的子集等。 行為時序邏輯TLA由Leslie Lamport提出,行為時序邏輯使得在一個程序中同時表達(dá)系統(tǒng)模型及系統(tǒng)屬性成為可能。它是時態(tài)邏輯的直接擴(kuò)展版本,它通過公式的形式表達(dá)系統(tǒng)模型與屬性。而基于TLA的描述語言TLA+是該邏輯的一種時序規(guī)約語言,它基于ZF集合理論、一階邏輯,適用于規(guī)約反應(yīng)式、并發(fā)式和分布式系統(tǒng)等等。TLC是對用TLA+描述的并發(fā)系統(tǒng)的模型檢測工具。有這樣一套完整的理論與檢測工具,我們就可以開展幾個方面的研究。 在研究中,我們從三個方向進(jìn)行,第一個方向是對行為時序邏輯TLA的理論進(jìn)行深入研究,力求能在理論上有所突破;第二個方向是對現(xiàn)實(shí)的系統(tǒng)進(jìn)行形式化描述與檢測;第三個方向是對協(xié)議進(jìn)行形式化描述與檢測,通過努力,在三個方向上都取得了一定的認(rèn)識,但還有許多研究工作需要繼續(xù)和加強(qiáng),從而能在基于TLA的形式化分析與檢測上取得成績。 在研究中,我們做了如下具體的工作: 1、在基于TLA的并發(fā)系統(tǒng)研究中,論文提出可控屬性的轉(zhuǎn)移系統(tǒng)。論文首先提出了狀態(tài)轉(zhuǎn)移條件Γ_c,這樣可以對行為A作出限定,然后提出可控行為A_(Γc),由狀態(tài)轉(zhuǎn)移條件和可控行為這兩個定義,進(jìn)而定義可控狀態(tài)、可控運(yùn)跡等等,最后提出了可控屬性的轉(zhuǎn)移系統(tǒng)的定義T_c=(Q,S_(cv),(?)_c,Λ_c,Γ_c),并提出和證明在一個可控屬性轉(zhuǎn)移系統(tǒng)T_c中,所有的狀態(tài)是可控狀態(tài)的。 對提出的定義和定理還需要實(shí)例來驗(yàn)證。我們從簡單的時鐘系統(tǒng)、電梯系統(tǒng)、交通系統(tǒng)到網(wǎng)絡(luò)協(xié)議進(jìn)行了形式化描述與檢測。對按可控轉(zhuǎn)移的Needham-Schroeder協(xié)議進(jìn)行形式化描述與檢測,結(jié)果證明提出的相關(guān)理論是合適的。 2、安全性是系統(tǒng)的重要屬性,在上面工作的基礎(chǔ)上,提出安全轉(zhuǎn)移系統(tǒng)。論文首先提出安全轉(zhuǎn)移條件Γ,安全性確認(rèn)T,然后提出安全行為A_(Γs),進(jìn)而定義安全狀態(tài)、安全運(yùn)跡等,由此定義安全轉(zhuǎn)移系統(tǒng)T_s=(Q,S_θ,(?)_s,Λ_s,Γ)。提出并證明安全運(yùn)跡的充分必要條件,及安全系統(tǒng)中的狀態(tài)是安全狀態(tài)的。 基于所提出的安全轉(zhuǎn)移系統(tǒng),對網(wǎng)絡(luò)銀行系統(tǒng)進(jìn)行形式化描述與檢測。在形式化過程中,發(fā)現(xiàn)銀行已經(jīng)采取種種防范措施使網(wǎng)絡(luò)銀行的安全性有了較好的保障,但在支付過程中,措施相對薄弱,于是提出面向支付的網(wǎng)鉻銀行安全轉(zhuǎn)移系統(tǒng)。對并發(fā)的面向支付的網(wǎng)上銀行安全轉(zhuǎn)移系統(tǒng)進(jìn)行基于TLA+的形式化描述。通過TLC檢測,表明基于安全轉(zhuǎn)移系統(tǒng)的網(wǎng)上銀行,滿足設(shè)定的多條安全性質(zhì),且在一定程度上增強(qiáng)了并發(fā)環(huán)境中網(wǎng)鉻銀行的安全性。 3、對系統(tǒng)進(jìn)行形式化與檢測,其主要目的是進(jìn)行活性(Liveness Porperty)的檢驗(yàn),Leslie Lamport提出了基于TLA的活性規(guī)則,論文對文獻(xiàn)中的一些相關(guān)規(guī)則加以詳細(xì)地證明,但發(fā)現(xiàn)這些規(guī)則還不夠用。如在對網(wǎng)絡(luò)協(xié)議、網(wǎng)絡(luò)銀行系統(tǒng)研究中,發(fā)現(xiàn)一個主體下可以設(shè)置多個子主體,如一個服務(wù)器可有多個客戶端,一個帳號下可設(shè)置多個子帳號。它們可以并發(fā)地執(zhí)行一行為。這樣的并發(fā)系統(tǒng)的多行為的活性規(guī)則是怎樣的呢? 通過研究,提出了在強(qiáng)、弱公平性下多行為的活性規(guī)則MWF1、MSF1、MSF2,這兒條規(guī)則對并發(fā)系統(tǒng)中多行為的活性進(jìn)行了歸納,對這兒條規(guī)則進(jìn)行了證明,并在形式化檢測中,以網(wǎng)絡(luò)銀行多用戶取款行為并發(fā)互斥系統(tǒng)為例,用TLA+進(jìn)行系統(tǒng)描述,并設(shè)計(jì)對這些規(guī)則的檢測,檢測的結(jié)果表明論文提出的強(qiáng)、弱公平性下多個行為者的活性規(guī)則是合適的。進(jìn)而歸納得到多行為者的安全行為在強(qiáng)、弱公平性下的性質(zhì)規(guī)則MWFS1、MSFS1、MSFS2,并加以證明與檢測。 4、基于TLA的檢測工具AVISPA是2003年元月歐共體支助的重大項(xiàng)目,檢測工具基于HLPSL語言進(jìn)行描述,主要用于網(wǎng)絡(luò)協(xié)議等的形式化與檢測,在初步的研究中,對Kerberros協(xié)議分四步模型與六步模型進(jìn)行形式化與檢測,通過檢測,說明在一定條件下協(xié)議是不安全的,并顯示出攻擊步驟。 另一個檢測工具TLC2.0是Compaq與Microsoft公司于2003年開發(fā)的,工具使用TLA+描述語言,通過對Neeham-Schroeder協(xié)議進(jìn)行形式化與檢測,發(fā)現(xiàn)Neeham-Schroeder協(xié)議在一定條件下可以被中間人攻破。 在形式化過程中,首先要對相關(guān)協(xié)議進(jìn)行準(zhǔn)確地描述與抽象,而后模型化。在對模型的描述中,要描述出通信雙方或多方的行為,信息通過設(shè)計(jì)的通道進(jìn)行通信,對侵入者的設(shè)計(jì),一般設(shè)定其可以接受任何信息,并可篡改任何信息。最后要設(shè)計(jì)檢測性質(zhì)。通過檢測發(fā)現(xiàn)問題或是相關(guān)性質(zhì)是否滿足。通過檢測,發(fā)現(xiàn)這兩個協(xié)議在一定條件下,是可以攻破的。 相比較而言,使用TLA+語言,要寫的基礎(chǔ)代碼要多些,更適合對系統(tǒng)的形式化與檢測,可做到“心中有數(shù)”;而使用HLPSL語言進(jìn)行協(xié)議描述,有許多現(xiàn)存的功能可用,對協(xié)議的檢測能力上表現(xiàn)得更強(qiáng)大。對檢測工具的對比研究,包含著名的檢測工具SPIN、SMV等等的對比研究,還需做大量的工作。
【學(xué)位授予單位】：貴州大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2009
【分類號】：TP302.2
【圖文】：

將上面不同的情況和活性條件加入到一起形成一個完整的電子時鐘系統(tǒng)�？梢约尤胄再|(zhì)進(jìn)行檢測，如 :PROPERTIESExistTimesHMSever由于提示占用太多內(nèi)存而不能檢測。如圖2.4所示。圖2.4運(yùn)行結(jié)果一

圖2.5運(yùn)行結(jié)果二2.8TLC檢測工具檢測工具TLCZ.o是由ComPaq與Microsoft公司于2003共同研發(fā)的基于TLA的檢測工具，通過TLc檢測工具，可以實(shí)現(xiàn)對系統(tǒng)的基于TLA模型化的檢測，從而來判斷最初的設(shè)想并可對系統(tǒng)進(jìn)行深一步地認(rèn)識。2.8.1TLC檢測形式使用TLC的檢測形式如下:P，二g尸口”2_nameoptionssPe‘~萬l。其中，Pl卿二，n_nam。尚avatlatk.TLC中檢測程序的名字;oPlio邢是檢測參數(shù);sPecjle是要檢測的文件名。2.9本章小結(jié)LeslieLamPortl’一，】提出的行為時序邏輯TLA，具有用一個程序同時表達(dá)系統(tǒng)模型與系統(tǒng)性質(zhì)的特點(diǎn)。本章對行為時序邏輯TLA語法和語義、線性時態(tài)邏輯‘公平性、活性、邏輯

【引證文獻(xiàn)】

相關(guān)期刊論文 前2條

1 吳勇;李祥;;基于TLA的ARQ協(xié)議描述與驗(yàn)證[J];計(jì)算機(jī)安全;2012年08期

2 夏薇;姚益平;慕曉冬;;面向事件圖和事件時態(tài)邏輯的模型檢驗(yàn)方法[J];軟件學(xué)報(bào);2013年03期

相關(guān)碩士學(xué)位論文 前1條

1 李翠翠;基于SPIN模型檢測的電子商務(wù)協(xié)議分析與驗(yàn)證[D];華東理工大學(xué);2012年

本文編號：2724930