安全系統(tǒng)形式化設(shè)計與分析研究.pdf

1、隨著計算機和因特網(wǎng)的應(yīng)用迅速普及與發(fā)展，信息安全已日益成為人們關(guān)注的焦點。本論文以國家信息系統(tǒng)等級保護標準為主要依據(jù)，基于進程代數(shù)等形式化方法，對安全模型設(shè)計、安全信息流分析以及原型系統(tǒng)實現(xiàn)等重要理論和實踐問題展開了研究，取得了如下研究成果：
　　 (1)建立了支持動態(tài)調(diào)節(jié)的保密性和完整性統(tǒng)一模型。為了滿足兼顧信息保密性和完整性保護的安全需求，本文提出一種基于多級安全策略的動態(tài)統(tǒng)一模型(簡稱DMUM)。模型以保密性和完整性作為安

2、全標識的兩個維度，主體當前安全標識根據(jù)客體安全標識和主體訪問權(quán)限的歷史過程進行動態(tài)調(diào)整，一方面實現(xiàn)了BLP模型和Biba模型的有機結(jié)合，另一方面通過對非可信主體實施安全級的非管理動態(tài)調(diào)節(jié)，使其無需完全依賴于可信主體的管理調(diào)節(jié)，從而能夠減少一些無法預(yù)料的安全風(fēng)險。同時，給出了可信主體的形式定義，推廣了多級可信主體概念，使得可信主體只在指定范圍內(nèi)實施讀寫權(quán)利，從而在多級安全策略范圍內(nèi)滿足可信主體的最小特權(quán)原則。通過一個實例說明了模型的有效性

3、和可用性。
　　 (2)提出了基于進程代數(shù)的非傳遞無干擾時間信息流分析方法。為了揭示安全降密等非傳遞安全策略系統(tǒng)中的隱蔽時間信息流，本文基于進程代數(shù)方法分析了非傳遞無干擾時間信息流的安全屬性。將可信域的概念引入時間安全進程代數(shù)(tSPA)，擴展了tSPA的表達能力，使其能模擬實際系統(tǒng)中的可信部分。接著以tSPA為工具將非傳遞無干擾模型由確定系統(tǒng)推廣到諸如實時系統(tǒng)之類的時間系統(tǒng)上，提出了非傳遞時間互擬強無干擾(I_tBSNNI)和

4、非傳遞時間互擬復(fù)合不可演繹(I_tBNDC)安全屬性。為了揭露出I_tBNDC在動態(tài)環(huán)境中不能暴露的安全隱患，提出了要求系統(tǒng)所有可達狀態(tài)都滿足I_tBSNNI的I_tSBSNNI屬性。以一個擴展的時間系統(tǒng)實例分析說明我們所提出的方法的有效性。
　　 (3)給出了面向隱蔽通道構(gòu)建的多級安全形式定義。針對目前多級安全策略形式定義與安全目標關(guān)系不清晰的問題，本文形式描述了面向隱蔽通道構(gòu)建的多級安全性。由于隱蔽通道是安全系統(tǒng)要盡量避免的

5、安全問題，因此，從隱蔽通道構(gòu)建的角度去定義安全性質(zhì)會更有助于人們對系統(tǒng)安全本質(zhì)問題的深入理解。鑒于面向隱蔽通道構(gòu)建的隔離安全性質(zhì)不具實用性，我們基于可傳遞性和非傳遞性安全策略的特點，將可信域概念引入該理論框架，提出了兩個關(guān)于傳遞與非傳遞安全性質(zhì)的推論，并給出了相應(yīng)的證明。
　　 在上述理論研究成果的基礎(chǔ)上，本文最后介紹了基于可信計算平臺的高安全級操作系統(tǒng)原型(圖靈安全操作系統(tǒng))的設(shè)計與實現(xiàn)。包括原型系統(tǒng)的設(shè)計思路以及功能劃分；強