基于程序設(shè)計(jì)語言的安全降密模型研究.pdf

1、本文研究使用基于程序設(shè)計(jì)語言的技術(shù)來控制信息安全降密，主要包括以下四方面的工作： 首先，針對(duì)動(dòng)態(tài)安全降密控制問題，提出動(dòng)態(tài)魯棒降密模型。建立包含機(jī)密性級(jí)別和完整性級(jí)別的安全格，然后從“哪兒”和“何時(shí)”的角度描述數(shù)據(jù)的完整性級(jí)別升級(jí)策略。該策略指定數(shù)據(jù)可從哪個(gè)完整性級(jí)別開始升級(jí)，又至哪個(gè)級(jí)別升級(jí)結(jié)束，以及每一步升級(jí)時(shí)要滿足的安全語義條件。雖然安全降密只能發(fā)生在高完整性級(jí)別的程序上下文中，但是不可信的低完整性數(shù)據(jù)就能以這種嚴(yán)格受限的

2、方式升級(jí)到高完整性級(jí)別以影響機(jī)密數(shù)據(jù)釋放。本文還設(shè)計(jì)了靈活的類型系統(tǒng)，允許開發(fā)者根據(jù)應(yīng)用需求和程序特點(diǎn)選擇合適的靜態(tài)條件分析技術(shù)(如數(shù)據(jù)流分析方法、抽象解釋等)引入類型檢查，用于推斷數(shù)據(jù)完整性級(jí)別升級(jí)時(shí)安全條件是否滿足。 其次，面向多線程程序中的信息流控制問題，本文基于強(qiáng)互模擬等價(jià)的方式定義了多線程環(huán)境下能同時(shí)處理信息降密和抹除的安全模型。它在任意線程調(diào)度方式下都是魯棒的，能精確地控制哪些信息才被允許釋放，使得降密機(jī)制不會(huì)被攻擊

3、者破壞而獲得多余的機(jī)密信息，并且能確保低安全級(jí)別信息被抹除后不會(huì)被攻擊者濫用。為了檢查程序是否滿足安全需求，本文構(gòu)造了實(shí)施同一安全策略的非轉(zhuǎn)換類型系統(tǒng)和轉(zhuǎn)換類型系統(tǒng)。前者簡(jiǎn)單地判斷一個(gè)給定的程序是否為良類型，而后者使用交叉拷貝技術(shù)消除由于線程之間互相競(jìng)爭(zhēng)執(zhí)行引起的內(nèi)部時(shí)間隱蔽通道。如果程序被非轉(zhuǎn)換類型系統(tǒng)判定為非良類型，可使用轉(zhuǎn)換類型系統(tǒng)嘗試將其轉(zhuǎn)換成一個(gè)具有相同語義的安全程序。如果還是沒有相應(yīng)的轉(zhuǎn)換類型規(guī)則能應(yīng)用到程序上，那么程序就會(huì)

4、被判定為不安全的。 接著，針對(duì)概率系統(tǒng)中的安全降密控制，本文將非傳遞無干擾信息流安全模型由確定系統(tǒng)推廣到概率系統(tǒng).為了模擬實(shí)際系統(tǒng)中的可信部分，將可信域的概念引入概率安全進(jìn)程代數(shù)，然后在弱概率互擬等價(jià)的基礎(chǔ)上提出了非傳遞概率互擬強(qiáng)無干擾(I_BSPNI)和非傳遞概率互擬復(fù)合不可演繹(I_PBNDC)安全屬性。為了揭露出I_PBNDC在動(dòng)態(tài)環(huán)境中不能暴露的安全隱患，提出了要求系統(tǒng)所有可達(dá)狀態(tài)都滿足I_PBNDC的持久I_PBNDC

5、屬性。接著使用基于單步狀態(tài)的展開條件定義了易于驗(yàn)證的強(qiáng)I_PBNDC屬性。本文還分析了一個(gè)實(shí)際概率路由系統(tǒng)上的非傳遞信息流安全屬性。 最后，面向概率時(shí)間系統(tǒng)中的安全降密控制問題，本文以概率時(shí)間自動(dòng)機(jī)為形式化工具將非傳遞無干擾模型擴(kuò)展到概率時(shí)間系統(tǒng)，使其能夠應(yīng)用于諸如實(shí)時(shí)系統(tǒng)之類的時(shí)間系統(tǒng)上的信息流分析。本文根據(jù)高安全域、低安全域和可信域劃分概率時(shí)間自動(dòng)機(jī)中的動(dòng)作集合，然后提出了非傳遞概率時(shí)間無干擾(I_PTNI)和非傳遞概率時(shí)間