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

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

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

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

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

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