信息流圖分割算法的設(shè)計(jì)與信息流的PVS實(shí)現(xiàn).pdf

1、隱通道的危害在信息交流日漸重要的今天越來(lái)越突出，隱通道通過(guò)利用安全系統(tǒng)中具有較高安全級(jí)別的主體或進(jìn)程根據(jù)事先約定好的編碼方式，通過(guò)更改共享資源的屬性并使低安全級(jí)別的主體或進(jìn)程觀察到這種變化，來(lái)傳送違反系統(tǒng)安全策略的信息。因此，通過(guò)隱通道竊取機(jī)密信息的手段并不能被安全模型阻止，或者說(shuō)，安全模型對(duì)于通過(guò)隱通道進(jìn)行的信息攻擊無(wú)能為力。 由于一個(gè)大型多安全級(jí)軟件系統(tǒng)的信息傳遞關(guān)系非常復(fù)雜，在信息流圖的層面上直接進(jìn)行信息流分析并搜索隱通道

2、的工作量非常大，為進(jìn)一步提高搜索和分析隱通道的效率，本文在已經(jīng)提出信息流圖的基礎(chǔ)上提出一種將信息流圖分割成信息流森林的算法，該算法首先選定一棵父樹，然后通過(guò)邊割集中的弧置換父樹中的樹枝得到新樹，并能從理論上保證分割后得到的信息流森林正確繼承原圖的信息，即原圖中信息流既未被割裂也未丟失。通過(guò)對(duì)每棵信息流樹表示的信息流進(jìn)行分析即可取代對(duì)整個(gè)信息流圖的分析，從而有效降低了分析問(wèn)題的規(guī)模。 接著，本文引入PVS原型驗(yàn)證系統(tǒng)(Protot

3、ype Verification System)進(jìn)行信息流的隱通道研究。首先，利用PVS的規(guī)約語(yǔ)言描述信息流，并提出相應(yīng)的引理和定理。再用PVS定理證明器證明信息流中是否存在可能的隱通道。一個(gè)規(guī)約相當(dāng)于一套公理系統(tǒng)，提出一系列關(guān)于此公理系統(tǒng)的定理，如果規(guī)約是正確的，那么這些定理即成立。因此，在本研究中如果信息流中存在可能的隱通道，則PVS的證明將不能通過(guò)，如果信息流中不存在可能的隱通道，則PVS將完成既定的證明。 文中使用兩個(gè)經(jīng)