基于行為時(shí)序邏輯TLA的系統(tǒng)、規(guī)則與協(xié)議檢測的研究.pdf

1、為了保證軟、硬件系統(tǒng)的可靠安全，包括圖靈獎(jiǎng)得主A.PnDeli在內(nèi)的許多計(jì)算機(jī)科學(xué)家都認(rèn)為，采用形式化方法(Formal Methods)對系統(tǒng)進(jìn)行形式化驗(yàn)證和分析，是構(gòu)造可靠安全軟件的一個(gè)重要途徑。模型檢測(Model Checking)是形式驗(yàn)證方法中重要的一種。
　　形式化方法原則上就是采用數(shù)學(xué)與邏輯的方法描述和驗(yàn)證系統(tǒng)。其描述主要包括兩方面：一是系統(tǒng)行為的描述，也稱建模，通過構(gòu)造系統(tǒng)的模型來描述系統(tǒng)及其行為模式；二是系統(tǒng)性

2、質(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ò)展版本，它通過公式

3、的形式表達(dá)系統(tǒng)模型與屬性。而基于TLA的描述語言TLA+是該邏輯的一種時(shí)序規(guī)約語言，它基于ZF集合理論、一階邏輯，適用于規(guī)約反應(yīng)式、并發(fā)式和分布式系統(tǒng)等等。TLC是對用TLA+描述的并發(fā)系統(tǒng)的模型檢測工具。有這樣一套完整的理論與檢測工具，我們就可以開展幾個(gè)方面的研究。
　　在研究中，我們從三個(gè)方向進(jìn)行，第一個(gè)方向是對行為時(shí)序邏輯TLA的理論進(jìn)行深入研究，力求能在理論上有所突破；第二個(gè)方向是對現(xiàn)實(shí)的系統(tǒng)進(jìn)行形式化描述與檢測；第三個(gè)方

4、向是對協(xié)議進(jìn)行形式化描述與檢測，通過努力，在三個(gè)方向上都取得了一定的認(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)移條件和可控行為這兩個(gè)定義，進(jìn)而定義可控狀態(tài)、可控運(yùn)跡等等，最后提出了可控

5、屬性的轉(zhuǎn)移系統(tǒng)的定義(Tc=Q,ScN,Lc,Λc,Γc)，并提出和證明在一個(gè)可控屬性轉(zhuǎn)移系統(tǒng)cT中，所有的狀態(tài)是可控狀態(tài)的。
　　對提出的定義和定理還需要實(shí)例來驗(yàn)證。我們從簡單的時(shí)鐘系統(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)。論文首先

6、提出安全轉(zhuǎn)移條件Γ，安全性確認(rèn)T，然后提出安全行為AΓs，進(jìn)而定義安全狀態(tài)、安全運(yùn)跡等，由此定義安全轉(zhuǎn)移系統(tǒng)Ts=(Q,Sθ,Ls,Λ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ā)的

7、面向支付的網(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)研究

8、中，發(fā)現(xiàn)一個(gè)主體下可以設(shè)置多個(gè)子主體，如一個(gè)服務(wù)器可有多個(gè)客戶端，一個(gè)帳號下可設(shè)置多個(gè)子帳號。它們可以并發(fā)地執(zhí)行一行為。這樣的并發(fā)系統(tǒng)的多行為的活性規(guī)則是怎樣的呢？
　　通過研究，提出了在強(qiáng)、弱公平性下多行為的活性規(guī)則MWF、1MSF、1MSF，這幾2條規(guī)則對并發(fā)系統(tǒng)中多行為的活性進(jìn)行了歸納，對這幾條規(guī)則進(jìn)行了證明，并在形式化檢測中，以網(wǎng)絡(luò)銀行多用戶取款行為并發(fā)互斥系統(tǒng)為例，用TLA+進(jìn)行系統(tǒng)描述，并設(shè)計(jì)對這些規(guī)則的檢測，檢測的結(jié)

9、果表明論文提出的強(qiáng)、弱公平性下多個(gè)行為者的活性規(guī)則是合適的。進(jìn)而歸納得到多行為者的安全行為在強(qiáng)、弱公平性下的性質(zhì)規(guī)則MWFS、1MSFS、1MSFS，2并加以證明與檢測。
　　4、基于TLA的檢測工具AVISPA是2003年元月歐共體支助的重大項(xiàng)目，檢測工具基于HLPSL語言進(jìn)行描述，主要用于網(wǎng)絡(luò)協(xié)議等的形式化與檢測，在初步的研究中，對Kerberros協(xié)議分四步模型與六步模型進(jìn)行形式化與檢測，通過檢測，說明在一定條件下協(xié)議是不安

10、全的，并顯示出攻擊步驟。
　　另一個(gè)檢測工具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)行通信，對侵入者的

11、設(shè)計(jì)，一般設(shè)定其可以接受任何信息，并可篡改任何信息。最后要設(shè)計(jì)檢測性質(zhì)。通過檢測發(fā)現(xiàn)問題或是相關(guān)性質(zhì)是否滿足。通過檢測，發(fā)現(xiàn)這兩個(gè)協(xié)議在一定條件下，是可以攻破的。
　　相比較而言，使用TLA+語言，要寫的基礎(chǔ)代碼要多些，更適合對系統(tǒng)的形式化與檢測，可做到“心中有數(shù)”；而使用HLPSL語言進(jìn)行協(xié)議描述，有許多現(xiàn)存的功能可用，對協(xié)議的檢測能力上表現(xiàn)得更強(qiáng)大。對檢測工具的對比研究，包含著名的檢測工具SPIN、SMV等等的對比研究，還需做