信息流的語(yǔ)法標(biāo)識(shí)及其屬性算術(shù)驗(yàn)證的研究.pdf

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

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

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

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

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