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

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

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

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

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