安全操作系統(tǒng)原理與技術(shù)安徽理工大學(xué)計算機科學(xué)與工程學(xué)院

信息安全系

張柱講師7/19/2023第6章形式化方法與安全模型學(xué)習(xí)內(nèi)容: ①了解什么是形式化方法 ②了解形式化安全模型 ③掌握基于訪問控制矩陣的安全模型 ④掌握基于格的安全模型 ⑤了解其他安全模型本章重點： 基于訪問控制矩陣的安全模型、基于格的安全模型7/19/20232第6章形式化方法與安全模型(8課時)

6.1形式化方法1.定義所謂形式化方法，指的是使用特定的語言和推理來描述事物的方法。相對而言，非形式化的方法則是以自然語言和基于人們的常識來描述事物的方法。使用形式化的表示方法，尤其是使用一套簡單易懂的語義學(xué)符號來描述事物之間的關(guān)系，可以大大提高描述安全策略的精度，使用形式化的證明可以從理論上確保系統(tǒng)的安全策略能夠滿足系統(tǒng)的安全需求。2.通常，系統(tǒng)的不安全性源自于對用戶安全需求的錯誤理解或源自于系統(tǒng)的實現(xiàn)缺陷。保證系統(tǒng)安全性的主要策略是，制定一個符合用戶安全須由的安全策略模型，該模型必須同時考慮安全策略和其在自動信息系統(tǒng)中的實現(xiàn)過程。7/19/20233第6章形式化方法與安全模型(8課時)6.1形式化方法安全策略模型應(yīng)由如下兩個子模型組成：對安全的定義和一套操作的規(guī)則。為了說明形式化方法在安全系統(tǒng)的建立過程中所起的角色，有必要來對建立一個安全自動信息系統(tǒng)開發(fā)的各個階段進行詳細的描述，如圖。7/19/20234第6章形式化方法與安全模型(8課時)

6.1形式化方法高層策略目標(biāo)：用來指定設(shè)計和使用計算機系統(tǒng)來實現(xiàn)什么目標(biāo)；外部接口需求：是將高層策略目標(biāo)應(yīng)用于計算機系統(tǒng)的外部接口。內(nèi)部需求：用來約束系統(tǒng)實體或部件相互之間的關(guān)系。對安全的形式化定義，通常包含內(nèi)部需求和外部接口兩個方面。操作規(guī)則：用來解釋內(nèi)部需求是如何通過指定的訪問檢查和相關(guān)的行為措施來保證內(nèi)部需求的正確實施。高層設(shè)計：用來指定系統(tǒng)部件或被控的實體的行為以及TCB接口的復(fù)雜功能描述。代碼編寫，涉及到硬件接口的代碼，必須詳細了解硬件接口規(guī)范。7/19/20235第6章形式化方法與安全模型(8課時)

6.1形式化方法高層目標(biāo)指定的恰當(dāng)性對設(shè)計一個計算機系統(tǒng)尤其重要，其是否合適的判斷標(biāo)準(zhǔn)是，能否抵御威脅并且可以加以實現(xiàn)。系統(tǒng)的安全策略是否合適是使用該系統(tǒng)的組織的安全策略能否成功實施的關(guān)鍵。如果一個系統(tǒng)的安全策略的實施能夠達到系統(tǒng)事先制定的安全目標(biāo)，則該安全策略就是適當(dāng)?shù)?。有三種“形式化證明”方法：①數(shù)學(xué)證明；②機器證明；③Hilbert證明。數(shù)學(xué)證明依賴于使用數(shù)學(xué)語言來進行模型或范型的形式化，不允許自動化。7/19/20236第6章形式化方法與安全模型(8課時)

6.1形式化方法機器證明依賴于使用機器化的證明器，“檢查機”具有如下的特性：①接受輸入；②決定輸出；③如果成功，則該推測是該系列假設(shè)的有效結(jié)果。證明器能夠潛在的提升用戶效率。在操作系統(tǒng)的安全策略模型中，經(jīng)常需要自動機的協(xié)助。典型地，對安全的定義包含許多需求，這些需求通常以狀態(tài)不變式和狀態(tài)轉(zhuǎn)換約束的形式出現(xiàn)。特別地，一個需求只處理幾個狀態(tài)元素，任何操作規(guī)則對這些元素的細微的修改都會導(dǎo)致對需求的違反，因此，至多90%的必需的引理都可能是非常重要的。7/19/20237第6章形式化方法與安全模型(8課時)

6.1形式化方法除了得到形式化語義學(xué)的證明外，通過機器證明器的方法不大可能獲得太高的的安全級別保證。在這種情況下，一個公式A是一系列公式集B的有效結(jié)果，當(dāng)且僅當(dāng)每個滿足公式集B的解釋同樣滿足公式A。即不經(jīng)過形式化語義學(xué)的證明，證明器可能不夠安全并且有可能接受錯誤的假設(shè)。形式化語義學(xué)包括對公式功能的解釋以及對系統(tǒng)的證明方法是正確的相關(guān)證明。7/19/20238第6章形式化方法與安全模型(8課時)

6.2形式化安全模型形式化模型，指的是用形式化的方法來描述如何實現(xiàn)系統(tǒng)的安全要求，包括機密性、完整性和可用性。一個安全的計算機系統(tǒng)可以分為如下幾大部分：數(shù)據(jù)結(jié)構(gòu)、進程、用戶信息、I/O設(shè)備以及被控實體的安全屬性。標(biāo)識被控實體在設(shè)計一個安全模型中占據(jù)著重要地位，對于達到TCSEC規(guī)定的B2級或以上安全級的系統(tǒng)來說，被控實體必須包括所有的系統(tǒng)資源。系統(tǒng)包括顯式被控實體和隱式被控實體。數(shù)據(jù)結(jié)構(gòu)是一個數(shù)據(jù)倉庫，包含標(biāo)明系統(tǒng)內(nèi)部狀態(tài)的數(shù)據(jù)和值。系統(tǒng)中進程可以利用系統(tǒng)事先明確定義的允許的操作來對這些數(shù)據(jù)或值進行讀或?qū)懺L問。一個最小的數(shù)據(jù)結(jié)構(gòu)，同時也是顯式被控實體的存儲客體，存儲客體的安全屬性可能包括安全級和用戶訪問權(quán)限。7/19/20239第6章形式化方法與安全模型(8課時)

6.2形式化安全模型在包含安全級的模型中，在最小化的情況下，存儲客體具有唯一的安全級，存儲客體可能被組合起來形成多級數(shù)據(jù)結(jié)構(gòu)，其中每個客體被賦予自己的安全級。進程可創(chuàng)建、刪除存儲客體及其他進程以及與它們交互，還可以與I/O設(shè)備交互。顯式被控進程稱為“主體”。通常具有多種與它關(guān)聯(lián)的安全屬性，可能包括安全級、硬件安全屬性。在支持角色的程序中，系統(tǒng)用戶可履行制定角色的職責(zé)，一個用戶可以擁有多個角色，一個角色也可以包含多個用戶。用戶與系統(tǒng)設(shè)備的交互行為在模型中體現(xiàn)對I/O設(shè)備的約束。外部策略要求系統(tǒng)只有允許授權(quán)用戶才能訪問相應(yīng)的I/O設(shè)備。I/O設(shè)備封裝在TCB軟件內(nèi)，并被看作是被動實體。安全屬性可以顯式地與顯式受控實體相關(guān)聯(lián)，還有一些與系統(tǒng)環(huán)境相關(guān)的安全屬性。7/19/202310第6章形式化方法與安全模型(8課時)

6.2形式化安全模型安全策略的主要方面反映在安全模型中包括策略的目標(biāo)、策略實施的場合和強度以及用戶分類的粒度等。在將安全策略進行形式化時，這些方面將反映在受控實體的安全屬性上。信息的策略是用來維護信息的安全屬性供系統(tǒng)和用戶使用，而訪問控制的策略限制系統(tǒng)中的主體對系統(tǒng)資源和資源所包含的信息的訪問。訪問控制屬性可以根據(jù)其控制的內(nèi)容進行分類：不嚴格的訪問控制屬性，只和受控實體相關(guān)；嚴格的訪問控制屬性則不僅與實體相關(guān)，還與其所包含的信息相關(guān)。大多數(shù)的安全策略是集中授權(quán)和分布式授權(quán)的混合體。7/19/202311第6章形式化方法與安全模型6.3基于訪問控制矩陣的安全模型6.3.1Lampson訪問控制矩陣模型利用狀態(tài)機模型來形式化描述對客體訪問的安全模型大多數(shù)是Lampson訪問控制矩陣模型的變體。在此模型中，客體被視為存儲器，訪問控制檢查不基于存儲在此容器內(nèi)的值，而是基于系統(tǒng)的狀態(tài)，系統(tǒng)狀態(tài)中與安全相關(guān)的要素概括在個訪問矩陣中。Lampson模型中，系統(tǒng)的狀態(tài)是由一個三元組(S,O,M)來決定，其中：S：表示系統(tǒng)中主體的集合，也是系統(tǒng)正在運行的程序集合；O：系統(tǒng)中客體的集合，客體是指主體行為的對象，即主體行為的直接承擔(dān)者。M：表示二維訪問矩陣，主體用行表示，客體用列表示，主、客體的交叉點表示主體對客體所擁有的訪問權(quán)限。7/19/202312第6章形式化方法與安全模型6.3.1Lampson訪問控制矩陣模型系統(tǒng)中狀態(tài)的改變?nèi)Q于訪問矩陣Ｍ的改變，獨立的狀態(tài)機構(gòu)成一個系統(tǒng)，因此訪問矩陣也可稱為系統(tǒng)的“狀態(tài)保護”。Lampson模型中訪問控制矩陣如圖：主體(Subjects)客體(Objects)file1file2file3SunnyOwn/Read/WriteReadWriteCloneReadOwn/Read/WriteReadRichardReadWriteOwn/Read/Write7/19/202313第6章形式化方法與安全模型6.3基于訪問控制矩陣的安全模型6.3.2Graham-Denning模型在Graham-Denning模型中，對主體集合S、目標(biāo)集合O、權(quán)利集合R和訪問控制矩陣A進行操作。矩陣中每個主體一行，每個主體以及每個目標(biāo)均有一列。一個主體對于另一個主體，或者一個目標(biāo)的權(quán)利利用矩陣元素的內(nèi)容來表示。對于每個目標(biāo)，標(biāo)明為“擁有者”的主體，有特殊的權(quán)利；對于每個主體，標(biāo)明為“控制者”的另一個主體，有特殊權(quán)利。在Graham-Denning模型中，有八個基本的保護權(quán)，這些權(quán)利被表示成主體能夠發(fā)出的命令，作用于其他主體或目標(biāo)。①創(chuàng)建目標(biāo)；②創(chuàng)立主體，刪除目標(biāo)，刪除主體；③讀訪問權(quán)；④授予訪問權(quán)；⑤刪除訪問權(quán)；⑥轉(zhuǎn)移訪問權(quán)。這些規(guī)則如圖所示。7/19/202314第6章形式化方法與安全模型6.3.2Graham-Denning模型命令條件作用創(chuàng)立目標(biāo)o－－在A中增加一個關(guān)于o的列，在A[x,o]處放入“擁有者”創(chuàng)立主體s－－在A中增加一個關(guān)于s的行，在A[x,s]處放入“控制”刪除目標(biāo)oA[x,o]中為“擁有者”刪除o對應(yīng)的列刪除主體sA[x,s]中為“控制”刪除s對應(yīng)的行S對o讀訪問權(quán)A[x,s]中的為“控制”A[x,o]中為“擁有者”將A[s,o]拷貝給x刪除s對o的訪問權(quán)rA[x,s]中的為“控制”或A[x,o]為“擁有者”從A[s,o]中去掉r給s授予對o的訪問權(quán)rA[x,o]中為“擁有者”從A[s,o]中增加r轉(zhuǎn)移對o的訪問權(quán)r或r*給sA[x,o]中為r*從A[s,o]中增加r或r*7/19/202315第6章形式化方法與安全模型6.3基于訪問控制矩陣的安全模型6.3.3HRU模型HRU模式是Graham-Denning模型的變體，在HRU模型中，基于“命令”來描述對主客體的訪問控制機制，其中每個命令含有“條件”和“基本操作”。命令結(jié)構(gòu)如下：7/19/202316第6章形式化方法與安全模型6.3.3HRU模型或者，如果m為0，命令格式為：其中，α是命令名，X1，…，Xk

是形式參數(shù)，每個opi

是以下原語操作之一：①輸入權(quán)限r(nóng)到(Xs,Xo)中； ②從(Xs,Xo)中刪除權(quán)限r(nóng)；③創(chuàng)建主體Xs； ④創(chuàng)建客體Xo；⑤取消主體Xs； ⑥取消客體Xo。r(r1,…,rm)是普通權(quán)限，s(s1,…,sm)和o(o1,…,om)是1至k間的整數(shù)。7/19/202317第6章形式化方法與安全模型6.3.3HRU模型在HRU模型中，將系統(tǒng)的保護基于三元組(S,O,P),其中，S表示系統(tǒng)當(dāng)前的主體集，O表示當(dāng)前系統(tǒng)的客體集，并且S包含于O，p表示訪問控制矩陣，此矩陣中，行表示主體，列表示客體，P[S,O]是權(quán)限集R的一個子集，表示主體S對客體O擁有的權(quán)限，HRU模型中的訪問控制矩陣。主體客體Xs1Xs2Xs3Xo1Xo2Xo3Xs1控制擁有/掛起/恢復(fù)擁有擁有讀/擴展Xs2控制擴展擁有Xs3控制讀/寫寫讀…7/19/202318第6章形式化方法與安全模型6.3.3HRU模型在HRU模型中，創(chuàng)建CREATE、授予CONFER和撤銷REMOVE命令如下：1.創(chuàng)建(CREATE)進程可能創(chuàng)建客體，進程擁有對自己創(chuàng)建的客體的擁有權(quán)，表示如下：commandCREATE(process,file) createobjectfile enterowninto(process,file)end7/19/202319第6章形式化方法與安全模型6.3.3HRU模型2.授予(CONFER)文件的擁有者可以授予除“擁有”權(quán)限以外的任何權(quán)限給任何一個其他主體，表示如下：commandCONFER(owner,friend,file) ifownin(owner,file) thenenterrinto(friend,file)end此處，r表示讀、寫和執(zhí)行等權(quán)限7/19/202320第6章形式化方法與安全模型6.3.3HRU模型3.撤銷(REMOVE)文件的擁有者可以撤銷任何一個其他主體賦予此文件的權(quán)限，表示如下：commandREMOVE(owner,exfriend,file) ifownin(owner,file)and rin(exfriend,file) thendeleterfrom(exfriend,file)end7/19/202321第6章形式化方法與安全模型6.3.3HRU模型Harrison等得出兩個重要結(jié)論對保護系統(tǒng)的設(shè)計者有重要影響。①第一個結(jié)論適用于限定每條命令只包含一個操作時的情況?？梢耘卸ㄒ粋€給定的保護系統(tǒng)，從訪問控制矩陣的某一給定的初始配置出發(fā)，能否允許一給定的用戶獲得對一個給定目標(biāo)的給定的訪問權(quán)。②如果不限定每條命令只含一項操作，則一個給定的保護系統(tǒng)是否可參照一給定的權(quán)利問題是“不可”判定的。7/19/202322第6章形式化方法與安全模型(8課時)

6.4基于格的安全模型6.4.1Bell-LaPadula模型BLP模型是1973年創(chuàng)立的一種模擬符合軍事安全策略的計算機操作模型，也是最常使用的一種計算機多級安全模型。BLP模型是一種狀態(tài)機模型，它形式化地定義了系統(tǒng)、系統(tǒng)狀態(tài)以及系統(tǒng)狀態(tài)間的轉(zhuǎn)換規(guī)則，定義了安全的概念，并制定了一組安全特性，以此對系統(tǒng)狀態(tài)和狀態(tài)轉(zhuǎn)換規(guī)則進行限制和約束，使得對一個系統(tǒng)，如果它的初始狀態(tài)是安全的，并且經(jīng)過一系列的規(guī)則都保持安全性，則可以證明該系統(tǒng)是安全的。7/19/202323第6章形式化方法與安全模型(8課時)

6.4.1Bell-LaPadula模型1.系統(tǒng)狀態(tài)的表示狀態(tài)是系統(tǒng)中元素的表示，它由主體、客體、訪問屬性、訪問矩陣以及標(biāo)識主體和客體的訪問類屬性的函數(shù)組成。狀態(tài)v∈V由一個有序的四元組(b,M,f,H)所表示，其中：標(biāo)識在某個特定的狀態(tài)下，哪些主體以何種訪問屬性訪問哪些客體，其中S是主體集，O為客體集，A={r,w,a,e}是訪問屬性集；M：表示訪問矩陣，其中元素表示主體Si對客體Oj具有的訪問權(quán)限；f∈F：表示訪問類函數(shù)，記作f=(fs,fo,fc),其中fs表示主體的安全級函數(shù)；fc表示主體當(dāng)前擁有的安全級函數(shù)；fo表示客體的安全級函數(shù)。H：是客體間的層次關(guān)系,即當(dāng)前客體的樹形結(jié)構(gòu)，Oj∈H(O)表示在此樹形結(jié)構(gòu)中，Oj為葉子節(jié)點，O為父節(jié)點。7/19/202324第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型元素H在

(其中PO表示O的冪子集)中，iff：①Oi≠Oj

＝>H(Oi)∩H(Oj)=Φ②不存在集合{O1,O2,…,Ow}使得對每個r，1≤r≤w，有Or+1∈H(Or)，且Ow+1＝O12.安全系統(tǒng)的定義定義規(guī)則ρ：R×V→D×V含義：給定一個請求和一個狀態(tài)，規(guī)則ρ決定系統(tǒng)產(chǎn)生一個響應(yīng)和下一個狀態(tài)。其中R為請求集，V為狀態(tài)集，D為判定集{yes,no,error,?}，yes表示請求被執(zhí)行，no表示請求被拒絕，error表示有多個規(guī)則適用于該請求-狀態(tài)對，?表示規(guī)則ρ不能處理該請求。7/19/202325第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型設(shè)是相對于R,D,V的一組規(guī)則集，關(guān)系定義為(Rk,Dm,v*,v)∈iffDm≠?，并且存在唯一的i，1≤i≤s，使得(Dm,v*)；而系統(tǒng)定義為(x,y,z)∈Σ(R,D,W,z0)，iff：對每個t∈T,(xt,yt,zt,zt-1)∈W，其中z0為初始狀態(tài)。系統(tǒng)Σ(R,D,W,z0)是一個安全系統(tǒng)，iff：系統(tǒng)的每個狀態(tài)(z0,z1,…,zn)均為為安全狀態(tài)。7/19/202326第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型3.模型幾個重要的公理①簡單安全性：狀態(tài)v=(b,M,f,H)滿足簡單安全性，對所有：其中，符號≥表示前者支配后者，即b(S:x1,x2,…,xn)表示b中主體S對其具有訪問權(quán)限xi(1≤i≤n)的所有客體集合。②*-特性：S’是S的一個子集，狀態(tài)v=(b,M,f,H)，滿足相對于S’的*-特性，記為*-propertyrelS’，iff對所有的7/19/202327第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型③自主安全性：狀態(tài)v=(b,M,f,H)，滿足自主安全特性，iff：對于所有的.④兼容性公理：狀態(tài)v(b,M,f,H)滿足兼容性，iff：對所有的o∈O，有：7/19/202328第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型4.狀態(tài)轉(zhuǎn)換規(guī)則規(guī)則ρ定義為,ρ：R×V→D×V。規(guī)則ρ保持系統(tǒng)安全狀態(tài)，iff：對所有的ρ(Rk,v)=(Dm,v*),有v是安全狀態(tài)，則v*是安全狀態(tài)，即：①規(guī)則ρ保持簡單安全性：即對所有的ρ(Rk,v)=(Dm,v*)，有v保持簡單安全性，則v*也保持安全性。②規(guī)則ρ保持*-特性：即對所有的ρ(Rk,v)=(Dm,v*)，有v保持*-特性，則v*也保持*-特性。③規(guī)則ρ保持自主安全性：即對所有的ρ(Rk,v)=(Dm,v*)，有v保持自主安全性，則v*也自主安全性。7/19/202329第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型5.模型的幾個重要定理定理1：對于每個初始狀態(tài)z0，系統(tǒng)Σ(R,D,W,z0)滿足簡單安全特性，iff：對每個行為(Ri,Dj,(b*,M*,f*,H*),(b,M,f,H))，關(guān)系W(ω)滿足：①對任意(S,O,x)∈b*-b滿足相對于f*的簡單安全性；②對任意(S,O,xρ)∈b不滿足相對于f*的簡單安全性的不在b*內(nèi)。定理2：對每個滿足相對于S’的*-特性的初始狀態(tài)z0，系統(tǒng)Σ(R,D,W,z0)滿足相對于S’的*-特性，iff：對每個行為(Ri,Dj,(b*,M*,f*,H*),(b,M,f,H))，關(guān)系W(ω)滿足：①對任意S∈S’，有：7/19/202330第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型②對任意S∈S’，有：定理3：系統(tǒng)Σ(R,D,W,z0)滿足自主安全特性，iff：z0滿足自主安全性，并且對每個行為(Ri,Dj,(b*,M*,f*,H*),(b,M,f,H))，關(guān)系W(ω)滿足：①對任意②對任意7/19/202331第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型推論(基本安全公理)：系統(tǒng)Σ(R,D,W,z0)是一個安全系統(tǒng)，iff：z0是一個安全狀態(tài)，并且對于每個動作，關(guān)系W滿足定理1，定理2和定理3。定理4：假設(shè)關(guān)系W是一套保持簡單安全特性的規(guī)則并且滿足簡單安全性，則系統(tǒng)Σ(R,D,W(ω),z0)滿足簡單安全特性。定理5：假設(shè)關(guān)系W是一套保持*-特性，并且z0滿足*-特性，則系統(tǒng)Σ(R,D,W(ω),z0)滿足*-特性。定理6：假設(shè)關(guān)系W是一套保持自主特性，并且z0滿足自主特性，則系統(tǒng)Σ(R,D,W(ω),z0)滿足簡單自主特性。7/19/202332第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型定理7：若v=(b,M,f,H)滿足簡單安全特性，并且

，則v*=(b*,M,f,H)滿足簡單安全性，iff：①(x=eorx=a)or②(x=rorx=w)andfs(S)≥fo(O)定理8：若v=(b,M,f,H)滿足相對于

的*-特性，并且對任意的

并且

,b*=b∪{(S,O,x)}，則v*=(b*,M,f,H)滿足相對于S’的*-特性，iff：①ifx=athenfo(O)≥fc(S)

②ifx=wthenfo(O)=fc(S)

③ifx=rthenfc(S)

≥fo(O)7/19/202333第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型定理9：若v=(b,M,f,H)滿足自主安全特性，并且

，則v*=(b*,M,f,H)滿足自主安全性，iff：x∈Mij定理10：設(shè)ρ為規(guī)則，且ρ(Rk,v)=(Dm,v*),其中v=(b,M,f,H)，v*＝(b*,M*,f*,H*)，則有：①如果，且f*=f，則規(guī)則ρ保持簡單安全性；②如果，且f*=f，則規(guī)則ρ保持*-特性；③如果，且對任意的i、j，f有，則ρ保持自主安全性；④如果，且f*=f，且對任意的i、j，有，則ρ保持安全狀態(tài)。7/19/202334第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型6.對BLP模型的爭論1)McLean的+-特性及其基本安全定理McLean的基礎(chǔ)：給定一個已知為不安全的假定系統(tǒng)，通過“基本安全定理”能夠證明該不安全的系統(tǒng)是安全的。定義1：狀態(tài)(b,M,f)滿足+-特性，當(dāng)且僅當(dāng)對每個主體s∈S，下列條件成立：①②也就是說，+-特性對主體S和客體O成立，當(dāng)且僅當(dāng)主體S的安全級別支配客體O的安全級別。狀態(tài)滿足+-特性，當(dāng)且僅當(dāng)對于每個三元組(S,O,x)，主體S和客體O都保持+-特性。7/19/202335第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型定理11(McLean)：對任何一個安全狀態(tài)z0，系統(tǒng)Σ(R,D,W,z0)相對于

滿足+-特性，iff：對任一行為(Ri,Dj,(b,a,f)(b’,a’,f’))，關(guān)系W(ω)滿足(對任意s∈S’)：①對任意(S,O,x)∈b-b’滿足相對于S’的+-特性；②對任意(S,O,x)∈b’不滿足相對于S’的+-特性的不在b’內(nèi)。定理12(McLean基本安全定理)：系統(tǒng)Σ(R,D,W,z0)是一個安全系統(tǒng)，iff：z0是安全的，且關(guān)系W(ω)滿足定理1、定理2和定理11中的條件。7/19/202336第6章形式化方法與安全模型(8課時)6.4.1Bell-LaPadula模型2)McLean的系統(tǒng)Z以及更多的問題系統(tǒng)Z具有弱寧靜特性，并且以此支持一個動作，當(dāng)某一主體對任意客體請求任意類型的訪問時，系統(tǒng)首先將所有主體和客體降到最低安全級別，然后在訪問控制矩陣中添加訪問權(quán)限，并允許訪問。定理13：如果z0是一個安全狀態(tài)，而且W中的每個動作都滿足替代版的簡單安全條件、*-特性和自主安全特性，那么系統(tǒng)Σ(R,D,W,z0)就是一個安全系統(tǒng)。實例，系統(tǒng)Z中有兩個安全級別HIGH和LOW，HIGH>LOW。初始狀態(tài)有一個主體s和一個客體o，在初始狀態(tài)下fsc(s)＝LOW且foc(o)=HIGH，a[s,o]={w},且b(S,O,w)。當(dāng)S對O請求讀取時，規(guī)則將系統(tǒng)轉(zhuǎn)換到一個狀態(tài)，在該狀態(tài)下foc(o)=LOW,(s,o,r)∈b’,a’[s,o]={r,w}。但是由于(s,o,r)∈b’-b且fsc(s)<foc(o),就產(chǎn)生了非法訪問。7/19/202337第6章形式化方法與安全模型(8課時)

6.4基于格的安全模型6.4.2D.Denning模型1.概述信息流模型是訪問控制模型的變形，這類模型不檢查主體對客體的存取，而試圖從一個客體到另一個客體的信息傳輸過程，根據(jù)兩個客體的安全屬性決定操作是否進行。信息流分析能夠保證操作系統(tǒng)模型在對敏感信息存取時不會將數(shù)據(jù)泄露給所調(diào)用的模塊。7/19/202338第6章形式化方法與安全模型(8課時)

6.4.2D.Denning模型2.格結(jié)構(gòu)有界格是一個有限的偏序集，有最小上界和最大下界操作符的數(shù)學(xué)結(jié)構(gòu)，關(guān)系(S,→,+,*)是格，必須具有如下性質(zhì)：①(S,→)是一個偏序集；②S是有限的；③S有下界L，對于S中的所有A，有L→A；④+是S上的最小上界操作符；⑤*是S上的最大下界操作符。7/19/202339第6章形式化方法與安全模型(8課時)6.4.2D.Denning模型3.典型的格結(jié)構(gòu)例如線性優(yōu)先權(quán)格，描述了n個類之間的線性次序，對所有i,j∈[0,n-1],i+j=max(i,j),i*j=min(i,j),L=0,H=n-1。當(dāng)n=2時，非機密為0，機密為1。當(dāng)n=4時，可用于普通軍事安全問題，非機密為0，機密為1，秘密為2，絕密為3。7/19/202340第6章形式化方法與安全模型(8課時)6.4.2D.Denning模型例如：描述了2n(n=3)個子集之間的包含關(guān)系，箭頭代表所有權(quán)關(guān)系。該圖推廣到任何的n值，且可以用于有如下特性的系統(tǒng)：信息只能流向與出發(fā)點的類至少有相同的所有權(quán)的類。7/19/202341第6章形式化方法與安全模型(8課時)6.4.2D.Denning模型假定程序有m個輸入?yún)?shù)x1,x2,…xm和n個輸出參數(shù)y1,y2,…,yn，使得每個輸出參數(shù)只決定于某些輸入。所有權(quán)格可以從X={x1,x2,…xm}的子集構(gòu)造。和每個輸入xi相聯(lián)系的類是氮元素集合#