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

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

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

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

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