基于Petri網的安全策略分析與驗證方法研究.pdf

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

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

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

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

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

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

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

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

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