基于Petri網(wǎng)的信息流安全屬性的驗證與可組合性研究.pdf

1、隨著國家、社會對計算機和網(wǎng)絡(luò)技術(shù)的依賴程度日益增長，信息安全問題越來越重要。訪問控制機制是保護(hù)信息機密性、完整性的重要手段，但即使實施了強制訪問控制機制的安全系統(tǒng)中仍然會發(fā)生高安全級信息向低安全級用戶泄漏的隱通道問題。信息的泄露本質(zhì)上是信息的非法流動，因此信息流分析技術(shù)一直被用來尋找系統(tǒng)中潛在的各種信息泄露問題。該技術(shù)定義信息流安全屬性刻畫信息的合法流動，通過驗證系統(tǒng)是否滿足信息流安全屬性來判斷系統(tǒng)中是否存信息泄露，從而防止信息流向未被

2、授權(quán)的用戶。
　　 傳統(tǒng)的信息流分析技術(shù)采用“展開方法”來驗證信息流安全屬性，但該方法僅適用于確定型系統(tǒng)，而對非確定型系統(tǒng)，該方法是可靠的，但不完備。本文以Petri網(wǎng)作為安全系統(tǒng)的模型，對安全屬性設(shè)計了一套完備的驗證算法。該算法主要通過計算Petri網(wǎng)的可達(dá)圖實現(xiàn)，為了降低可達(dá)圖的計算量，設(shè)計了Petri網(wǎng)上保持安全屬性的化簡規(guī)則。進(jìn)一步針對系統(tǒng)均由很多個子系統(tǒng)組成，給出了保持安全屬性的組合模式，從而只需分析子系統(tǒng)是否滿足安全

3、屬性即可。本文的具體研究內(nèi)容包括：
　　 1.提出Petri網(wǎng)上信息流安全屬性的可靠完備的驗證算法。首先以Petri網(wǎng)作為安全系統(tǒng)的模型，對信息流安全屬性進(jìn)行形式化定義，然后基于Petri網(wǎng)的可達(dá)圖開發(fā)完備的安全屬性驗證方法。該方法從初始狀態(tài)出發(fā)，計算Petri網(wǎng)中所有可執(zhí)行變遷所引發(fā)的狀態(tài)集合，通過分析變遷序列的執(zhí)行對結(jié)果狀態(tài)集的影響，來判斷安全屬性是否成立。完備的算法使我們既能判斷屬性成立，亦能判斷屬性不成立。
　　

4、 2.提出Petri網(wǎng)的化簡規(guī)則，并給出化簡規(guī)則保持安全屬性不變的證明。針對基于可達(dá)圖的驗證算法存在狀態(tài)空間爆炸問題，提出三種Petri網(wǎng)的化簡規(guī)則：庫所化簡規(guī)則，變遷化簡規(guī)則，綜合化簡規(guī)則。這些規(guī)則剔除了Petri網(wǎng)中對驗證安全屬性沒有影響的庫所和變遷，從而使系統(tǒng)需要進(jìn)行驗證的可達(dá)圖得到精簡。為了說明化簡規(guī)則的正確性，我們證明了對信息流安全屬性，精簡后的系統(tǒng)與原系統(tǒng)是等價的。
　　 3.提出Petri網(wǎng)上保持信息流安全屬性的可