基于Petri網(wǎng)的安全策略分析與驗(yàn)證方法研究.pdf

1、伴隨著科學(xué)技術(shù)的飛速發(fā)展，信息已成為推動(dòng)社會(huì)前進(jìn)的巨大動(dòng)力。利用計(jì)算機(jī)和網(wǎng)絡(luò)對(duì)信息進(jìn)行收集、加工、存儲(chǔ)以及交換等，越來越成為各行各業(yè)必不可少的手段，計(jì)算機(jī)已經(jīng)滲透到了社會(huì)生活的各個(gè)方面，各種信息系統(tǒng)的建立和使用造成我們對(duì)計(jì)算機(jī)系統(tǒng)事實(shí)上的依賴。但是，由于各系統(tǒng)中存儲(chǔ)的數(shù)據(jù)、網(wǎng)絡(luò)上傳輸和交換的數(shù)據(jù)都是具有一定價(jià)值的信息，對(duì)這些信息的非法訪問、竊取、篡改等行為必然導(dǎo)致計(jì)算機(jī)安全問題的出現(xiàn)。
　　 當(dāng)前，系統(tǒng)的龐大和復(fù)雜化使得系統(tǒng)安全

2、性能分析與驗(yàn)證問題變得越來越復(fù)雜并越來越引起人們的重視。提供有效的數(shù)學(xué)理論工具、直觀的模型描述方法和有效的模型分析方法以及實(shí)用的輔助分析軟件，是系統(tǒng)安全性能分析與驗(yàn)證所面臨的迫切需要解決的問題，這也正是基于Petri 網(wǎng)的安全策略分析與驗(yàn)證技術(shù)的核心。
　　 從計(jì)算機(jī)系統(tǒng)、Web 服務(wù)以及安全協(xié)議的安全需求和現(xiàn)實(shí)基礎(chǔ)出發(fā)，對(duì)相關(guān)理論、協(xié)議、關(guān)鍵技術(shù)以及具體實(shí)現(xiàn)進(jìn)行了廣泛深入的研究。主要研究工作包括以下幾個(gè)方面：
　　 保

3、密性策略和完整性策略是重要的安全策略，在許多軍用和商用系統(tǒng)中得到廣泛的應(yīng)用。其代表模型分別是Bell-LaPadula 模型和Biba 模型，這兩個(gè)模型是數(shù)學(xué)上的對(duì)偶。保密性策略用于防止信息的非授權(quán)泄漏，而完整性策略則是防止信息被非授權(quán)更改。對(duì)采用了特定安全模型的具體實(shí)用系統(tǒng)需要一個(gè)嚴(yán)格有效的方法對(duì)其保密性和完整性進(jìn)行分析和驗(yàn)證。安全策略研究的一個(gè)關(guān)鍵問題是：用易于理解的和精確的形式表達(dá)策略。因此，提出了利用Petri 網(wǎng)對(duì)安全策略進(jìn)行

4、描述，Petri 網(wǎng)不僅適合策略的表達(dá)，而且可用于系統(tǒng)分析，以確定所定義的機(jī)制是否符合策略定義。
　　 對(duì)于一個(gè)安全策略，首先建立基于Petri 網(wǎng)的形式化描述，然后就可以根據(jù)形式化的描述對(duì)實(shí)施了特定安全模型的進(jìn)程或系統(tǒng)進(jìn)行分析與驗(yàn)證。分別對(duì)Bell-LaPadula 保密性模型和Biba 完整性模型進(jìn)行了描述。給出了這兩個(gè)模型基于Petri 網(wǎng)的形式化定義，并對(duì)實(shí)施了這兩個(gè)安全模型的相應(yīng)示例進(jìn)程進(jìn)行了分析和驗(yàn)證。顯示出Petr

5、i 網(wǎng)不僅能夠用用易于理解的和精確的形式表達(dá)安全策略，而且可用于系統(tǒng)分析和驗(yàn)證。Petri 網(wǎng)的覆蓋圖則在自動(dòng)分析大型復(fù)雜系統(tǒng)方面很有用處。
　　 為了對(duì)實(shí)施了中國(guó)墻模型的系統(tǒng)進(jìn)行分析與驗(yàn)證，提出了一種基于有色Petri 網(wǎng)的混合安全策略分析方法。中國(guó)墻模型是一種兼顧保密性和完整性的混合安全模型。
　　 中國(guó)墻模型的顯著特征是自由選擇和強(qiáng)制性訪問控制的結(jié)合。首先，對(duì)中國(guó)墻模型進(jìn)行了非形式化的描述，并且將中國(guó)墻模型與其他安

6、全模型進(jìn)行了比較。然后，給出了中國(guó)墻模型基于有色Petri 網(wǎng)的形式化定義。其突出特征在于，引入了“控制庫(kù)所”的概念以解決跟蹤主體訪問記錄的問題。并且“控制庫(kù)所”代替訪問控制矩陣，與單個(gè)主體關(guān)聯(lián)，不需要集中存儲(chǔ)，更加適合在分布式環(huán)境下部署。最后，根據(jù)中國(guó)墻模型基于有色Petri 網(wǎng)的定義，通過對(duì)一個(gè)實(shí)施了中國(guó)墻模型的示例進(jìn)程進(jìn)行分析與驗(yàn)證，闡述了如何通過基于有色Petri 網(wǎng)的形式化定義和覆蓋圖分析和驗(yàn)證實(shí)施了中國(guó)墻模型的系統(tǒng)的行為。<

7、br>　　 當(dāng)前的互聯(lián)網(wǎng)正在經(jīng)歷著一些重要的變化，它已經(jīng)成為了一個(gè)Web 服務(wù)的載體，而不僅僅是一個(gè)信息的容器。Web 服務(wù)提供了一個(gè)語言中立，連接松散，獨(dú)立于平臺(tái)的方式，使得散布在互聯(lián)網(wǎng)上的各組織和企業(yè)內(nèi)部的應(yīng)用程序可以連接起來。Web服務(wù)合成可以讓我們將許多現(xiàn)有的Web 服務(wù)結(jié)合起來，形成一個(gè)新的，增值的Web服務(wù)?？煽康腤eb 服務(wù)合成需要建模的技術(shù)和工具。因此，提出了一個(gè)基于有色Petri網(wǎng)的Web 服務(wù)合成模型。這個(gè)模型為W

8、eb 服務(wù)合成提供了充分的表達(dá)能力，能夠直接變換為可執(zhí)行的合成定義，并且獨(dú)立于可執(zhí)行的合成語言?；赑etri 網(wǎng)的Web 服務(wù)合成模型還可以利用Petri 網(wǎng)的分析和驗(yàn)證能力對(duì)合成服務(wù)進(jìn)行安全分析和驗(yàn)證。
　　 首先，對(duì)Web 服務(wù)建立了有色Petri 網(wǎng)模型(服務(wù)網(wǎng))，然后在此定義的基礎(chǔ)上給出了四種基本W(wǎng)eb 服務(wù)合成結(jié)構(gòu)：順序結(jié)構(gòu)，并發(fā)結(jié)構(gòu)，選擇結(jié)構(gòu)，和循環(huán)結(jié)構(gòu)以及一種高級(jí)合成結(jié)構(gòu)置換結(jié)構(gòu)的形式化定義。并且還定義了一個(gè)具有

9、封閉性的Web 服務(wù)合成算法。最后，根據(jù)基于Petri 網(wǎng)的形式化驗(yàn)證方法對(duì)此Web 服務(wù)合成模型的可用性，保密性，完整性以及混合安全性進(jìn)行了分析和驗(yàn)證，得出了一些有用的結(jié)論。
　　 20年來，安全協(xié)議研究的進(jìn)展十分可喜，取得了豐富的研究成果。特別是20世紀(jì)90年代以來，研究取得突破性進(jìn)展，對(duì)安全協(xié)議若干本質(zhì)性的問題有了更為深刻的認(rèn)識(shí)。但是，這一領(lǐng)域還有許多問題有待解決。特別是形式化分析領(lǐng)域。因此，提出了一種基于有色Petri