基于程序語(yǔ)言的完整性安全模型.pdf

1、本研究針對(duì)系統(tǒng)的完整性需求，從分析系統(tǒng)完整性需求的實(shí)質(zhì)出發(fā)，對(duì)完整性進(jìn)行高度的抽象和定義，使用π-演算和類型系統(tǒng)為理論工具為系統(tǒng)完整性建模，建立一種通用的完整性安全模型。具體研究工作圍繞完整性安全模型中的兩大主題：信息流控制和系統(tǒng)行為屬性，主要包括以下四個(gè)方面的工作。 首先對(duì)六種不同的完整性定義進(jìn)行討論，指出各種定義之間的聯(lián)系與區(qū)別，并給出完整性安全的一種系統(tǒng)性定義，從而確立本研究的研究目標(biāo)。 其次，綜述若干經(jīng)典的完整性

2、模型：Biba模型、Lipner模型和ClarkWilson模型，并介紹幾種代表了完整性模型研究的新進(jìn)展的形式化模型：SLam演算的完整性模型、完整性的非功能性模型和分散式標(biāo)簽?zāi)Ｐ?。通過對(duì)現(xiàn)有完整性模型的討論，更加明確了本研究的技術(shù)路線。 第三，針對(duì)完整性信息流控制，構(gòu)造一種π-演算的安全類型系統(tǒng)，通過靜態(tài)類型檢驗(yàn)實(shí)現(xiàn)系統(tǒng)的完整性信息流控制。首先為π-演算建立具有完整性級(jí)別的類型系統(tǒng)，信息流控制的顆粒被抽象為π-演算中的名與進(jìn)程

3、，而訪問操作的原語(yǔ)就是π-演算的行為。然后建立該安全類型的子類規(guī)則和類型規(guī)則，這些規(guī)則體現(xiàn)了系統(tǒng)完整性策略對(duì)系統(tǒng)行為的限制，特定的就是Biba模型中的“不向上寫、不向下讀”信息流策略。接著，證明該類型系統(tǒng)的類型合理性，表明滿足初始安全策略的系統(tǒng)經(jīng)過不斷的演進(jìn)、交互，得到的系統(tǒng)依然滿足完整性要求，即系統(tǒng)滿足安全轉(zhuǎn)移要求。最后，將分散式標(biāo)簽?zāi)Ｐ蜆?gòu)造靈活有效的完整性等級(jí)標(biāo)簽，并應(yīng)用到我們構(gòu)造的類型系統(tǒng)中，形成方便的完整性控制。結(jié)論顯示，類型系

4、統(tǒng)的方法通過靜態(tài)類型檢驗(yàn)可高效地實(shí)現(xiàn)細(xì)顆粒度的信息流控制。 最后，針對(duì)完整性的系統(tǒng)行為屬性，通過對(duì)系統(tǒng)的行為和行為模式進(jìn)行規(guī)范、約束以達(dá)到系統(tǒng)的完整性需求。主要包括兩個(gè)方面內(nèi)容：使用π-演算刻畫系統(tǒng)行為屬性，定義一種系統(tǒng)的行為完整性規(guī)范，通過驗(yàn)證進(jìn)程的互模擬等價(jià)性可驗(yàn)證進(jìn)程的完整性屬性；構(gòu)造一種名為行為標(biāo)簽的分散式標(biāo)簽，它是對(duì)分散式標(biāo)簽?zāi)Ｐ偷臄U(kuò)展，在此基礎(chǔ)上描述多種職責(zé)分離策略，這些策略體現(xiàn)為行為標(biāo)簽的謂詞結(jié)構(gòu)，可通過靜態(tài)標(biāo)簽檢