信息流的語法標識及其屬性算術(shù)驗證的研究.pdf

1、為保證計算機系統(tǒng)中的信息機密性,自主訪問控制和強制訪問控制策略在計算機多級安全系統(tǒng)中得到了廣泛的應(yīng)用。然而,實施了這兩種策略的計算機系統(tǒng)仍存在安全隱患,如安全系統(tǒng)中的隱通道問題。高安全級進程可以利用隱通道向低安全級進程泄漏信息,對系統(tǒng)安全構(gòu)成巨大威脅。因此,對高安全等級的安全操作系統(tǒng),各種安全標準都要求進行隱通道分析。
　　 信息流控制方法是應(yīng)用廣泛的隱通道搜索方法,包括語法信息流分析方法和語義信息流分析方法。傳統(tǒng)的語法信息流分

2、析方法均基于實施機密性安全策略的信息流格模型,而格關(guān)系的傳遞特性使得該方法不能用來分析實施無傳遞性安全策略的系統(tǒng)的安全性。無干擾分析方法是一種嚴謹?shù)恼Z義信息流分析方法,目前主要采用“展開技術(shù)”對信息流安全屬性進行驗證,但是驗證這些安全屬性的“展開方法”是可靠但并不是完備的,此外有一些安全屬性不存在“展開條件”。
　　 本文的主要研究內(nèi)容包括:
　　 1.針對格模型不能描述非傳遞安全性策略的問題,提出同時適用非傳遞性和傳遞

3、性安全策略的語法信息流分析方法。首先將信息流語義附加在每條語句之后,然后定義一種稱為信息流時序圖的圖結(jié)構(gòu)來刻畫信息流發(fā)生的時序關(guān)系,并給出基于源程序的信息流時序圖的構(gòu)造方法。接著提出刪除規(guī)則來刪除信息流圖中多余的初始點、終止點和重復(fù)路徑,并開發(fā)出一種基于時序圖的隱蔽信息流的標識算法。另外,針對并發(fā)程序的并發(fā)特性,提出了一種簡化信息流時序圖的方法。在該方法下只要考慮并發(fā)進程之間特定的交互次序即可,而不需考慮所有可能的交互方式。
　　

4、 2.針對驗證前向可修正屬性的“展開方法”不完備的問題,提出一種可靠且完備的前向可修正屬性驗證方法。該方法根據(jù)前向可修正屬性的特點,提出該屬性相應(yīng)的確定型系統(tǒng)的雙徑雙構(gòu)造,在雙徑雙構(gòu)造結(jié)構(gòu)上分析前向可修正屬性的性質(zhì),將前向可修正屬性的驗證歸約為可達性問題,進一步給出該屬性的驗證算法。當屬性不成立時,算法可以給出使屬性失效的反例,從而解決前向可修正屬性“展開方法”不完備性的問題。
　　 3.針對驗證廣義不可推斷屬性的“展開方法”

5、不完備的問題,提出一種可靠且完備的廣義不可推斷屬性的驗證方法。該方法給出廣義不可推斷屬性反例的定義,根據(jù)廣義不可推斷屬性的特點,提出與該屬性相應(yīng)的確定型系統(tǒng)的單徑雙構(gòu)造,并基于圖結(jié)構(gòu)理論得出該屬性最短反例的上近似計算。然后采用證偽技術(shù),通過逐步搜索長度遞增的使廣義不可推斷屬性失效的反例來完成驗證過程,從而解決廣義不可推斷屬性“展開方法”不完備性的問題。進一步為提高驗證方法的時間效率和降低對內(nèi)存空間的需求,將反例搜索和上近似計算歸約為量化