基于Petri網(wǎng)的信息流安全屬性的分析與驗證
2010-12-31 00:00:00陳松周從華鞠時光王基
計算機應(yīng)用研究 2010年12期
摘 要：信息流安全屬性的定義均基于不同的語義模型，很難作出比較，以Petri網(wǎng)作為描述安全系統(tǒng)的統(tǒng)一模型，在Petri網(wǎng)上定義四種常見的安全屬性，并分析它們之間的邏輯關(guān)系。在信息流安全屬性驗證方面，傳統(tǒng)的方法稱為展開方法，該方法適用于確定型系統(tǒng)，而對于非確定型系統(tǒng)，該方法是可靠的，但不完備。進(jìn)一步對Pe—tri網(wǎng)上已經(jīng)定義的四種屬性給出可靠完備的驗證算法，并開發(fā)出相應(yīng)的驗證工具。最后通過實例說明了驗證方法在搜索隱通道方面的應(yīng)用。關(guān)鍵詞：Petri網(wǎng)；無干擾屬性；廣義無干擾屬性；廣義非推斷屬性；可分離屬性
