基于信息流分析的安全系統(tǒng)驗(yàn)證.pdf

1、計(jì)算機(jī)和網(wǎng)絡(luò)技術(shù)的迅猛發(fā)展，導(dǎo)致對(duì)計(jì)算機(jī)系統(tǒng)和開(kāi)放式的網(wǎng)絡(luò)系統(tǒng)的攻擊日益增多。系統(tǒng)和網(wǎng)絡(luò)之所以會(huì)受到各種各樣的攻擊，究其原因，最根本的是系統(tǒng)和網(wǎng)絡(luò)內(nèi)部存在各種安全缺陷。為此，人們?cè)O(shè)計(jì)了各種各樣的安全策略、安全模型來(lái)確保系統(tǒng)的安全性，并使用密碼協(xié)議來(lái)保證網(wǎng)絡(luò)通信的安全。在這些安全策略應(yīng)用到系統(tǒng)之前，我們必須驗(yàn)證它們是否能夠滿足其“聲稱”的安全目標(biāo)；同樣，我們也要對(duì)密碼協(xié)議進(jìn)行分析，檢驗(yàn)其是否存在潛在的、未知的安全漏洞。 不管是直接

2、的或間接的機(jī)密數(shù)據(jù)泄露，都可以看作是信息的非法流動(dòng)，因此可以采用信息流分析的方法，找出系統(tǒng)或網(wǎng)絡(luò)中潛在的各種安全問(wèn)題。信息流分析方法是信息安全領(lǐng)域較為本質(zhì)的一種方法。 本文首先介紹了非干擾信息流分析的一般方法，即非確定系統(tǒng)中的信息流非干擾分析技術(shù)；然后研究了概率系統(tǒng)和安全協(xié)議中的信息流性質(zhì)，以及這些安全性質(zhì)的驗(yàn)證方法：本文的主要?jiǎng)?chuàng)新工作如下： 1．基于非干擾信息流分析的概率系統(tǒng)安全驗(yàn)證方法實(shí)際系統(tǒng)中，攻擊者可以通過(guò)對(duì)系統(tǒng)

3、行為觀察進(jìn)行統(tǒng)計(jì)，然后根據(jù)統(tǒng)計(jì)的概率數(shù)據(jù)構(gòu)建概率隱蔽通道，導(dǎo)致機(jī)密數(shù)據(jù)的間接泄露。因此，本文在概率配置下研究了系統(tǒng)的安全性。首先本文對(duì)非確定系統(tǒng)中的分析工具SPA進(jìn)行擴(kuò)展，得到PSPA，用以描述概率系統(tǒng)的行為。本文提出了P_PBNDC性質(zhì)，并討論了其在動(dòng)態(tài)概率環(huán)境下的適用性，也給出了其不同語(yǔ)義等價(jià)下的特征描述，以及基于展開(kāi)條件的特征描述。本文在P_PBNDC性質(zhì)的基礎(chǔ)上，提出了S PBNDC和CP_PBNDC性質(zhì)，這些都是PBNDC性質(zhì)

4、的充分條件。本文還給出了這些PBNDC類性質(zhì)之間的關(guān)系。這些分析是很有意義的，因?yàn)楸疚奶岢龅倪@些概率系統(tǒng)中的信息流安全性質(zhì)能夠暴露出那些非確定系統(tǒng)信息流安全性質(zhì)無(wú)法暴露出的系統(tǒng)安全缺陷。 2．基于環(huán)境敏感信息流分析的安全協(xié)議驗(yàn)證方法為了能夠描述安全協(xié)議的行為，我們對(duì)SPA進(jìn)行擴(kuò)展，形成了CryptoSPA。本文在CryptoSPA的環(huán)境敏感標(biāo)記轉(zhuǎn)換系統(tǒng)語(yǔ)義模型下，定義了環(huán)境敏感的路徑等價(jià)和弱互擬等價(jià)關(guān)系，并提出了基于環(huán)境知識(shí)的一

5、般組合上不可演繹的性質(zhì)框架ESGNDC<'α><,△>。在此框架下，討論了NDC<'σ>、BNDC<'σ>以及P_PBNDC<'σ>性質(zhì)。本文還在ESGNDC<'α><,△>框架下，討論了安全協(xié)議中的機(jī)密性，認(rèn)證性和公平性，并指出了此框架也適合安全協(xié)議的活性分析。 3．通過(guò)模型檢查驗(yàn)證信息流性質(zhì)BNDC類性質(zhì)的定義中都有全程量詞，因此驗(yàn)證一個(gè)系統(tǒng)具有這些性質(zhì)是非常困難的。本文使用部分模型檢查的方法來(lái)對(duì)BNDC類性質(zhì)進(jìn)行驗(yàn)證。首先