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

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

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

【引證文獻(xiàn)】

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

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

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

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

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

本文編號(hào)：2724930