基于一階邏輯的安全策略管理框架

基于一階邏輯的安全策略管理框架

近年來(lái)，信息安全研究領(lǐng)域從安全技術(shù)向安全管理的轉(zhuǎn)變?；趹?zhàn)略安全管理的研究是安全策略管理的重點(diǎn)。在安全策略管理的研究領(lǐng)域，如何表達(dá)安全策略，如何使用安全策略的重要性，以及安全策略本身的安全性，是三個(gè)基本和重要的問(wèn)題。從這三個(gè)基本問(wèn)題可以看出，安全策略的表達(dá)、安全策略的含義以及安全策略的確認(rèn)和驗(yàn)證揭示了三個(gè)重要的研究方向。在安全策略表達(dá)方面,目前的主流方法是使用形式化的語(yǔ)言描述安全策略.文獻(xiàn)對(duì)安全策略語(yǔ)言進(jìn)行了總結(jié),認(rèn)為基于邏輯的安全策略語(yǔ)言最容易被人們接受,文獻(xiàn)中提出的語(yǔ)言就是這類(lèi)語(yǔ)言.文獻(xiàn)首次設(shè)計(jì)了一種基于邏輯的分布式安全策略語(yǔ)言,其語(yǔ)法與擴(kuò)展型邏輯程序等價(jià),但沒(méi)有討論復(fù)雜查詢(xún)的計(jì)算方法,無(wú)法用于安全策略驗(yàn)證.文獻(xiàn)提出了一種基于分層邏輯程序的安全策略語(yǔ)言,稱(chēng)為FAF,它使用穩(wěn)定語(yǔ)義作為安全策略的語(yǔ)義.FAF嚴(yán)格限制“非”的使用,不支持負(fù)遞歸(negativerecursion),不支持量詞,描述的安全策略也不夠精煉,因而使用起來(lái)并不方便.由于已有的邏輯程序穩(wěn)定語(yǔ)義查詢(xún)算法的計(jì)算復(fù)雜度較高,因此FAF語(yǔ)義查詢(xún)效率較低.文獻(xiàn)使用約束邏輯程序表達(dá)安全策略,約束邏輯程序的約束域能夠方便地表達(dá)數(shù)值計(jì)算等特性,但其策略決策的計(jì)算復(fù)雜度較高.文獻(xiàn)基于動(dòng)態(tài)邏輯提出了一種可用于表達(dá)職責(zé)和動(dòng)態(tài)授權(quán)的安全策略語(yǔ)言,其安全策略驗(yàn)證問(wèn)題是不可判定的.文獻(xiàn)僅討論了安全策略語(yǔ)言的語(yǔ)法、語(yǔ)義及策略決策算法,并不支持安全策略驗(yàn)證這一關(guān)鍵特性.雖然目前已經(jīng)存在多種基于邏輯的安全策略語(yǔ)言,但這些語(yǔ)言基本上都是基于邏輯程序的,局限于邏輯程序的語(yǔ)法,某些情況下無(wú)法容易地描述出一些安全策略.文獻(xiàn)提出了一種基于一階邏輯的安全策略語(yǔ)言Lithium.為了有限度地支持量詞,Lithium對(duì)其語(yǔ)法進(jìn)行了嚴(yán)格的限制,普通管理人員難以理解,并且表達(dá)能力有限.但是,Lithium在用一階邏輯表達(dá)安全策略方面進(jìn)行了有益的嘗試.在安全策略語(yǔ)義查詢(xún)方面,安全策略究竟表達(dá)什么樣的語(yǔ)義(即所謂的正則語(yǔ)義)以及在該語(yǔ)義下的查詢(xún)算法是研究的重點(diǎn).事實(shí)上,如何定義安全策略的正則語(yǔ)義是一個(gè)非常復(fù)雜的問(wèn)題.現(xiàn)有的一些文獻(xiàn)一般僅討論具有特殊語(yǔ)法結(jié)構(gòu)的安全策略語(yǔ)言,從而可以容易地定義其語(yǔ)義.例如,文獻(xiàn)僅討論能夠表示成Datalog程序的安全策略,這是因?yàn)镈atalog程序具有公認(rèn)的正則語(yǔ)義.對(duì)于語(yǔ)法較為復(fù)雜的安全策略語(yǔ)言,其語(yǔ)義的研究往往被忽略了.例如,文獻(xiàn)中提出的安全策略語(yǔ)言要比文獻(xiàn)中提出的安全策略語(yǔ)言復(fù)雜得多,但卻沒(méi)有深入探討安全策略語(yǔ)義問(wèn)題.安全策略語(yǔ)義查詢(xún)算法的設(shè)計(jì)難度取決于安全策略語(yǔ)言的復(fù)雜程度,一般來(lái)說(shuō),安全策略語(yǔ)言越復(fù)雜,語(yǔ)義查詢(xún)算法的設(shè)計(jì)就越困難,計(jì)算復(fù)雜度也越高.因此,現(xiàn)有安全策略語(yǔ)言一般僅局限于具有特殊語(yǔ)法結(jié)構(gòu)的邏輯系統(tǒng).例如,文獻(xiàn)使用Datalog的語(yǔ)義查詢(xún)算法作為安全策略的語(yǔ)義查詢(xún)算法其計(jì)算復(fù)雜度是多項(xiàng)式級(jí)的.文獻(xiàn)則沒(méi)有明確地討論語(yǔ)義查詢(xún)問(wèn)題.在安全策略驗(yàn)證方面,目前已存在多種安全策略驗(yàn)證技術(shù).這些技術(shù)的基本思想是:首先將待驗(yàn)證安全策略轉(zhuǎn)換成抽象模型并通過(guò)形式化建模語(yǔ)言描述出來(lái),同時(shí)將待驗(yàn)證安全屬性轉(zhuǎn)換成形式化的安全屬性不變式,然后將它們輸入到驗(yàn)證工具中完成驗(yàn)證.這需要保證不同表達(dá)方式之間轉(zhuǎn)換的等價(jià)性,然而,(1)有時(shí)從理論上無(wú)法實(shí)現(xiàn)不同表達(dá)方式之間轉(zhuǎn)換的等價(jià)性;(2)即使可以從理論上保證轉(zhuǎn)換的等價(jià)性,但對(duì)于普通安全策略管理人員來(lái)說(shuō),保證實(shí)際轉(zhuǎn)換過(guò)程的等價(jià)性也是非常困難的;(3)安全策略驗(yàn)證算法和安全策略語(yǔ)義查詢(xún)算法采用的語(yǔ)義可能并不一致,從而有可能導(dǎo)致驗(yàn)證失效等問(wèn)題的產(chǎn)生.綜上所述,安全策略表達(dá)、語(yǔ)義查詢(xún)和安全策略驗(yàn)證之間是相互制約、相輔相成的.因此,在統(tǒng)一的安全策略管理框架中實(shí)現(xiàn)上述功能具有一定的優(yōu)勢(shì),但也面臨著巨大的挑戰(zhàn).現(xiàn)有安全策略語(yǔ)言大部分僅考慮到語(yǔ)義查詢(xún)問(wèn)題,而沒(méi)有考慮到安全策略驗(yàn)證問(wèn)題,而現(xiàn)有的驗(yàn)證技術(shù)又與安全策略語(yǔ)言嚴(yán)重脫節(jié),因而有可能存在驗(yàn)證失效等問(wèn)題.從公開(kāi)的文獻(xiàn)中還沒(méi)有發(fā)現(xiàn)將上述三者統(tǒng)一起來(lái)進(jìn)行形式化研究的成果,相關(guān)研究也不多見(jiàn),一般僅關(guān)注于某些特定類(lèi)型的安全策略,不具有普適性.例如,文獻(xiàn)介紹了一種在訪問(wèn)控制空間理論下研究系統(tǒng)特權(quán)安全問(wèn)題的方法,指出隱式授權(quán)可能導(dǎo)致系統(tǒng)存在不必要的特權(quán)濫用風(fēng)險(xiǎn).然而,隱式授權(quán)是現(xiàn)代安全策略系統(tǒng)中一種常用的授權(quán)方式,現(xiàn)有安全策略語(yǔ)言無(wú)一例外都支持隱式授權(quán).文獻(xiàn)使用一種稱(chēng)為快速構(gòu)造授權(quán)圖的算法檢測(cè)是否存在特權(quán)濫用,可以認(rèn)為這是一種特殊類(lèi)型的安全策略驗(yàn)證算法,但不支持負(fù)遞歸和非單調(diào)推理等特性.本文提出的方法可用于解決文獻(xiàn)中提出的問(wèn)題,且具有更好的通用性.基于上述考慮,本文提出了一種基于一階邏輯的安全策略管理框架WF-SPevf,可以在統(tǒng)一的良基語(yǔ)義下實(shí)現(xiàn)安全策略表達(dá)、語(yǔ)義查詢(xún)和驗(yàn)證.一階邏輯具有足夠強(qiáng)的表達(dá)能力,良基語(yǔ)義具備一系列優(yōu)良的特性(參見(jiàn)第1.2節(jié)和文獻(xiàn)),這使得WF-SPevf具有強(qiáng)大的表達(dá)能力,其所表達(dá)出的每個(gè)安全策略具有精確的語(yǔ)義定義方式和高效的語(yǔ)義查詢(xún)算法及驗(yàn)證算法.1預(yù)備知識(shí)本文假定讀者熟悉一階邏輯.為了便于閱讀,本節(jié)簡(jiǎn)要介紹本文所使用的各種術(shù)語(yǔ)、符號(hào)與約定.有關(guān)邏輯程序及其良基語(yǔ)義的詳細(xì)討論可參考文獻(xiàn).1.1常元符號(hào)的定義本文討論的一階邏輯系統(tǒng)的字母表Σ由下列7種類(lèi)型的符號(hào)集合構(gòu)成:(1)常元符號(hào)集;(2)變?cè)?hào)集;(3)函數(shù)符號(hào)集;(4)謂詞符號(hào)集;(5)邏輯連接符集C={~,∧,∨,←,?,};(6)量題符號(hào)集{?,?};(7)標(biāo)點(diǎn)符號(hào)集.本文所用術(shù)語(yǔ),如項(xiàng)、原子、文字、表達(dá)式、自由變?cè)?、約束變?cè)㈤]式、Herbrand域、Herbrand基、Herbrand解釋、語(yǔ)義等的詳細(xì)定義可參考文獻(xiàn).為了簡(jiǎn)單起見(jiàn),本文約定:(1)Σ為有限集;(2)所有常元符號(hào)都用首字母小寫(xiě)的字符串表示;(3)所有變?cè)?hào)都用首字母大寫(xiě)的字符串表示;(4)函數(shù)符號(hào)集為空集;(5)所有謂詞符號(hào)也都用首字母小寫(xiě)的字符串表示;(6)等符號(hào)表示變?cè)蛄?等符號(hào)表示常元序列,等符號(hào)表示項(xiàng)序列;(7)設(shè)X1,…,Xm為一階邏輯表達(dá)式F中全部的自由變?cè)?則?X1...?Xn(F)稱(chēng)為F的全稱(chēng)閉式,簡(jiǎn)寫(xiě)為?(F),?X1...?Xn(F)稱(chēng)為F的存在閉式,簡(jiǎn)寫(xiě)為?(F).定義1(二值語(yǔ)義).設(shè)Fs為由若干個(gè)一階邏輯表達(dá)式構(gòu)成的集合,HBsF為Fs上的Herbrand基,I為Fs上的Herbrand解釋(即I為基本原子集合且I?HBFs).如果Fs中的每個(gè)表達(dá)式G在I中的真值都為真,即IG,則I是Fs的一個(gè)二值Herbrand語(yǔ)義,簡(jiǎn)稱(chēng)為二值語(yǔ)義.1.2邏輯形式的真值解釋擴(kuò)展型邏輯程序是一種語(yǔ)法受限的一階邏輯系統(tǒng).每個(gè)邏輯程序都由一系列的規(guī)則構(gòu)成,每個(gè)規(guī)則都具有A←L1∧…∧Lm形式的邏輯表達(dá)式,它等價(jià)于閉式?(A∨~L1∨…∨~Lm),一般寫(xiě)成A←L1,…,Lm的形式.這里,A為原子,稱(chēng)為規(guī)則頭部;Li為文字,m≥0,{L1,…,Lm}稱(chēng)為規(guī)則體部.特別地,不含變?cè)囊?guī)則稱(chēng)為基本規(guī)則.文獻(xiàn)從模型論的角度給出了通過(guò)三值邏輯定義擴(kuò)展型邏輯程序良基語(yǔ)義的方法.不同于二值邏輯,三值邏輯認(rèn)為,人們對(duì)客觀世界的認(rèn)識(shí)是不完全的,存在一些既無(wú)法給出肯定判斷也無(wú)法給出否定判斷的事實(shí),其真值是“未定義的”.有關(guān)三值邏輯的詳細(xì)描述可參考文獻(xiàn).定義2(三值解釋).設(shè)L為一階邏輯語(yǔ)言,HUL為L(zhǎng)上的Herbrand域,HBL為L(zhǎng)上的Herbrand基,T?HBL,F?HBL,且T∩F=?,則序偶I=<T;F>為定義在L上的三值Herbrand解釋,簡(jiǎn)稱(chēng)為三值解釋.這里,T中每個(gè)基本原子的真值為“真”,F中每個(gè)基本原子的真值為“假”,U=HBL-(T∪F)中每個(gè)基本原子的真值為“未定義”.如果HBL=T∪F,則I蛻變成二值解釋.每個(gè)二值解釋I2都可以轉(zhuǎn)化成一個(gè)三值解釋I=<I2;HBL-I2>.三值解釋I=<T;F>可以等價(jià)地看成定義在HBL上的全函數(shù)I:如公式(1)所示:定義在L上的每個(gè)邏輯表達(dá)式的真值可遞歸地定義為如下形式:定義3(邏輯表達(dá)式的真值).設(shè)I=<T;F>為定義在L上的一個(gè)三值解釋,則(1)如果A是基本原子,則II(A)=I(A);(2)如果S是閉式,則II(~S)=1-II(S);(3)如果S和G都為閉式,則(4)對(duì)于任意的邏輯表達(dá)式S,若X是S的一個(gè)自由變?cè)?則由定義3可知,三值邏輯中的“←”和二值邏輯中的“←”是不同的.在二值邏輯中,S←G和S∨~G等價(jià),而在三值邏輯中,II(S←G)和max(II(S),1-II(G))并不恒等,因而S←G和S∨~G并不等價(jià).為了平滑三值邏輯和經(jīng)典二值邏輯之間的差異,本文引入一個(gè)新的邏輯連接符“”,并且規(guī)定SG等價(jià)于S∨~G.定義4(三值語(yǔ)義).不防設(shè)擴(kuò)展型邏輯程序P中的規(guī)則都是基本規(guī)則(否則將其實(shí)例化),則三值解釋M是P的三值語(yǔ)義,當(dāng)且僅當(dāng)對(duì)于P中任一基本規(guī)則A←L1,…,Lm,公式(2)都成立.顯然,每個(gè)二值語(yǔ)義都唯一對(duì)應(yīng)著一個(gè)三值語(yǔ)義.因此,若無(wú)特殊說(shuō)明,下文中的語(yǔ)義指的都是三值語(yǔ)義.由定義4可知,每個(gè)擴(kuò)展型邏輯程序至少有一個(gè)三值語(yǔ)義Φ=<?;?>,也可能有多個(gè)三值語(yǔ)義.研究人員普遍認(rèn)為良基語(yǔ)義是比較合理的三值語(yǔ)義,具有一系列良好的特性:(1)每個(gè)邏輯程序都具有唯一的良基語(yǔ)義;(2)良基語(yǔ)義和一系列特殊類(lèi)型邏輯程序公認(rèn)的正則語(yǔ)義等同.例如,分層邏輯程序的良基語(yǔ)義等同于其完美語(yǔ)義,而完美語(yǔ)義被認(rèn)為是分層邏輯程序的正則語(yǔ)義;(3)良基語(yǔ)義具備支撐性語(yǔ)義特性.所謂支撐性語(yǔ)義,是指該語(yǔ)義中任意一個(gè)基本文字都是由擴(kuò)展型邏輯程序中某個(gè)相應(yīng)的規(guī)則推理得到的.這一特性保證了安全策略描述安全需求的有效性;(4)存在高效的基于良基語(yǔ)義的語(yǔ)義查詢(xún)算法,如SLG算法,具備良好的實(shí)用性.因此本文選擇良基語(yǔ)義作為擴(kuò)展型邏輯程序的正則語(yǔ)義.SLG算法是由StonyBrook大學(xué)的Chen和Warren等人提出的一種高效的基于良基語(yǔ)義的邏輯程序語(yǔ)義查詢(xún)算法.文獻(xiàn)詳細(xì)討論了SLG算法及其計(jì)算復(fù)雜度、可靠性和完備性等問(wèn)題:SLG算法的計(jì)算復(fù)雜度是多項(xiàng)式級(jí)的;對(duì)于non-Floundering查詢(xún),SLG算法是可靠的和完備的;對(duì)于Floundering查詢(xún),SLG算法是可靠的,但不是完備的.所謂Floundering查詢(xún),是指SLG算法在消解查詢(xún)目標(biāo)的過(guò)程中,如果按照某種原則選取出的子目標(biāo)是負(fù)文字,且不是基本文字,則稱(chēng)這樣的查詢(xún)?yōu)镕loundering查詢(xún).從公開(kāi)的研究資料來(lái)看,幾乎所有的語(yǔ)義查詢(xún)算法都無(wú)法保證Floundering查詢(xún)的完備性.有關(guān)Floundering及non-Floundering查詢(xún)的詳細(xì)討論超出了本文的范圍,但SLG算法在語(yǔ)義查詢(xún)的過(guò)程中具備判定一個(gè)查詢(xún)是否為Floundering查詢(xún)的能力.如果SLG斷定某個(gè)查詢(xún)是Floundering查詢(xún),則報(bào)警并給出原因,然后退出語(yǔ)義查詢(xún)過(guò)程.XSB系統(tǒng)是目前被廣泛認(rèn)可而又有效的實(shí)現(xiàn)SLG算法的邏輯程序引擎.2擴(kuò)展型邏輯系統(tǒng)的安全策略鑒于已有安全策略語(yǔ)言描述能力及對(duì)安全策略驗(yàn)證支持上的不足,本文基于一階邏輯提出了一種支持安全策略驗(yàn)證的新型安全策略語(yǔ)言,簡(jiǎn)記為SPL.從語(yǔ)法形式上來(lái)看,SPL兼容絕大數(shù)現(xiàn)有的安全策略語(yǔ)言,并且比它們具有更強(qiáng)的描述能力.定義5(規(guī)則).設(shè)Wff為不含“←”邏輯連接符的一階邏輯表達(dá)式,A為原子,則稱(chēng)公式(3)形式的邏輯表達(dá)式為規(guī)則.公式(3)一般簡(jiǎn)寫(xiě)成A←Wff的形式.若Wff為空,則可簡(jiǎn)寫(xiě)成A←或A.此時(shí),A也稱(chēng)為事實(shí).定義6(安全策略).在本文中,由有限個(gè)公式(3)形式的規(guī)則構(gòu)成的集合稱(chēng)為安全策略.給定安全策略SP,它通過(guò)下列方式唯一地定義了一個(gè)與SP對(duì)應(yīng)的一階邏輯系統(tǒng)LSP:(1)在SP中出現(xiàn)的所有常元符號(hào)構(gòu)成LSP的常元符號(hào)集;(2)在SP中出現(xiàn)的所有謂詞符號(hào)構(gòu)成LSP的謂詞符號(hào)集;(3)函數(shù)符號(hào)集為空集.因而,LSP也可簡(jiǎn)記為SP.上述類(lèi)型的邏輯系統(tǒng)中使用的一階語(yǔ)言,稱(chēng)為安全策略語(yǔ)言,簡(jiǎn)記為SPL.由定義6可知,每個(gè)擴(kuò)展型邏輯程序都是一個(gè)SPL安全策略.由定義6還可以知道,SPL兼容絕大多數(shù)已有的安全策略語(yǔ)言.例如,它兼容文獻(xiàn)中提出的安全策略語(yǔ)言.安全策略語(yǔ)言關(guān)注兩個(gè)方面的表達(dá)能力:總體表達(dá)能力和個(gè)體表達(dá)能力.前者指通過(guò)規(guī)則的不同組合最終能夠達(dá)到的表達(dá)能力,一般直接稱(chēng)為表達(dá)能力;后者是指單個(gè)規(guī)則最終能夠達(dá)到的表達(dá)能力,一般簡(jiǎn)稱(chēng)為描述能力.從安全策略管理的角度來(lái)看,具有相同表達(dá)能力的兩種安全策略語(yǔ)言,描述能力越強(qiáng)的安全策略語(yǔ)言越容易受到安全管理人員的歡迎.由于安全策略語(yǔ)言直接面向安全管理員,因而目前的研究都非常注重安全策略語(yǔ)言的描述能力.對(duì)于任意給定的安全策略SP,設(shè)LSP為其對(duì)應(yīng)的一階邏輯系統(tǒng),F(LSP)為L(zhǎng)SP能夠表達(dá)的所有一階邏輯表達(dá)式的集合,SP(LSP)為L(zhǎng)SP能夠表達(dá)的所有安全策略規(guī)則的集合,LP(LSP)為L(zhǎng)SP能夠表達(dá)的所有邏輯程序規(guī)則的集合.由定義5可知,SP(LSP)?F(LSP).同樣,由第1.2節(jié)的內(nèi)容可知,LP(LSP)?SP(LSP).因而,從語(yǔ)法的角度來(lái)看,SPL的描述能力弱于相應(yīng)的一階邏輯語(yǔ)言,但強(qiáng)于相應(yīng)的邏輯程序語(yǔ)言.此外,由本文定理2和定理3不難發(fā)現(xiàn),SPL的表達(dá)能力等價(jià)于擴(kuò)展邏輯程序的表達(dá)能力.3計(jì)算后續(xù)轉(zhuǎn)換運(yùn)算直接定義安全策略語(yǔ)義面臨著巨大困難,為此,本文首先將安全策略轉(zhuǎn)換成擴(kuò)展型邏輯程序,然后利用擴(kuò)展型邏輯程序的良基語(yǔ)義定義安全策略的良基語(yǔ)義.算法1通過(guò)轉(zhuǎn)換運(yùn)算(1)至轉(zhuǎn)換運(yùn)算(10),將安全策略中的規(guī)則轉(zhuǎn)換成擴(kuò)展型邏輯程序中的規(guī)則,從而將安全策略轉(zhuǎn)換成擴(kuò)展型邏輯程序.算法1.安全策略轉(zhuǎn)換(securitypolicytransformation).定理1證明了算法1的可終止性和計(jì)算復(fù)雜度.這里,|Wff|為表達(dá)式Wff中的原子數(shù)目、“”連接符號(hào)數(shù)目、“∨”連接符號(hào)數(shù)目、“?”連接符號(hào)數(shù)目、“?”連接符號(hào)數(shù)目及“~”連接符號(hào)數(shù)目之和,稱(chēng)為表達(dá)式Wff的尺寸若SP為一個(gè)安全策略,則稱(chēng)|SP|=∑r∈SP|r|為SP的尺寸.定理1(算法1的可終止性).對(duì)于任意給定的安全策略SP,算法1可在有限步內(nèi)執(zhí)行完畢,并且其轉(zhuǎn)換結(jié)果是一個(gè)擴(kuò)展型邏輯程序.設(shè)SP中規(guī)則數(shù)目為v,“∨”連接符號(hào)數(shù)目為m,“?”連接符號(hào)數(shù)目為n,u=max{|r||r∈SP},k為使得u≤2k的最小值,則最壞情況下,算法1總的轉(zhuǎn)換次數(shù)不大于v?2u-1+m+n;平均情況下,算法1總的轉(zhuǎn)換次數(shù)不大于v?(u+k?2k-1),因而具有較好的實(shí)用價(jià)值.證明:設(shè)A←Wff為SP中的任一規(guī)則,算法1應(yīng)用于A←Wff的轉(zhuǎn)換運(yùn)算為τ,同時(shí),τ將SP轉(zhuǎn)換為SPτ.1)若τ為轉(zhuǎn)換運(yùn)算(1)、轉(zhuǎn)換運(yùn)算(2)、轉(zhuǎn)換運(yùn)算(4)或轉(zhuǎn)換運(yùn)算(10),則得到兩個(gè)新規(guī)則,設(shè)為A1←Wff1和A2←Wff2.不難發(fā)現(xiàn),|Wff1≤i≤2|<|Wff|;2)若τ為轉(zhuǎn)換運(yùn)算(3)、轉(zhuǎn)換運(yùn)算(6)或轉(zhuǎn)換運(yùn)算(9),則得到一個(gè)新規(guī)則,設(shè)為A1←Wff1.不難發(fā)現(xiàn),|Wff1|<|Wff|因而|SPτ|<|SP|;3)若τ為轉(zhuǎn)換運(yùn)算(8),則得到一個(gè)新規(guī)則,設(shè)為A1←Wff1,容易看出,|Wff1|=|Wff|.但轉(zhuǎn)換運(yùn)算(8)后面緊跟著的轉(zhuǎn)換運(yùn)算一定是轉(zhuǎn)換運(yùn)算(9),設(shè)其轉(zhuǎn)換結(jié)果為A2←Wff2,容易看出,|Wff2|<|Wff1|=|Wff|;4)若τ為轉(zhuǎn)換運(yùn)算(5),則所得結(jié)果一定為一個(gè)新規(guī)則,設(shè)為A1←Wff1,容易看出,|Wff1|=|Wff|.若無(wú)后續(xù)轉(zhuǎn)換運(yùn)算可作用于SPτ,則轉(zhuǎn)換結(jié)束,即算法1可在有限次轉(zhuǎn)換運(yùn)算后終止;否則,在所有后續(xù)轉(zhuǎn)換運(yùn)算中轉(zhuǎn)換運(yùn)算(5)最多出現(xiàn)m-1次.這是因?yàn)?每應(yīng)用一次轉(zhuǎn)換運(yùn)算(5),都會(huì)使得原SP中“∨”連接符號(hào)至少減少一個(gè),而所有其他的轉(zhuǎn)換運(yùn)算都不會(huì)引入“∨”連接符號(hào);5)若τ為轉(zhuǎn)換運(yùn)算(7),則得到一個(gè)新規(guī)則,設(shè)為A1←Wff1,容易看出,|Wff1|=|Wff|+1.但轉(zhuǎn)換運(yùn)算(7)后面緊跟著的轉(zhuǎn)換運(yùn)算一定是轉(zhuǎn)換運(yùn)算(10),設(shè)其轉(zhuǎn)換結(jié)果為A2←Wff2和A3←Wff3,并且|Wff2|≤|Wff1|-1=|Wff|,|Wff3|≤|Wff1|-1=|Wff|.同樣,若無(wú)后續(xù)轉(zhuǎn)換運(yùn)算可作用于SPτ,則轉(zhuǎn)換結(jié)束;否則,在所有后續(xù)轉(zhuǎn)換運(yùn)算中,轉(zhuǎn)換運(yùn)算(7)最多出現(xiàn)n-1次.這是因?yàn)?每應(yīng)用一次轉(zhuǎn)換運(yùn)算(7),都會(huì)使得原SP中“?”連接符至少減少一個(gè),而所有其他的轉(zhuǎn)換運(yùn)算都不會(huì)引入“?”連接符號(hào).綜合上述步驟1)~步驟5)的分析可知,轉(zhuǎn)換運(yùn)算τ要么使得|Wffi|<|Wff|(即轉(zhuǎn)換得到的新規(guī)則的尺寸小于原規(guī)則的尺寸),要么使得|SPτ|=|SP|.由于使得|SPτ|=|SP|的轉(zhuǎn)換運(yùn)算τ在整個(gè)轉(zhuǎn)換運(yùn)算序列中最多出現(xiàn)m+n次,因而對(duì)于任一安全策略SP,算法1一定可在有限步轉(zhuǎn)換運(yùn)算后將其轉(zhuǎn)換成邏輯程序SP′并終止.如果SP′不是邏輯程序,則SP′中一定存在可以繼續(xù)應(yīng)用轉(zhuǎn)換運(yùn)算的規(guī)則,因而算法1還沒(méi)有終止,這顯然是矛盾的.在極端情況下,算法1選擇的轉(zhuǎn)換運(yùn)算序列中的每個(gè)轉(zhuǎn)換運(yùn)算都使一個(gè)尺寸為i的規(guī)則分裂為尺寸為i-1的兩個(gè)規(guī)則.因而,針對(duì)每個(gè)規(guī)則的轉(zhuǎn)換運(yùn)算序列最大長(zhǎng)度不超過(guò)v?2u-1+m+n,轉(zhuǎn)換結(jié)果SP′中規(guī)則數(shù)目最多不超過(guò)v?u個(gè).在現(xiàn)實(shí)世界中,這種極端情況極其罕見(jiàn),因而轉(zhuǎn)換運(yùn)算序列長(zhǎng)度的平均值更具有參考價(jià)值.在平均情況下,算法1針對(duì)每個(gè)規(guī)則選擇的轉(zhuǎn)換運(yùn)算序列中的每個(gè)轉(zhuǎn)換運(yùn)算,使一個(gè)尺寸為i的規(guī)則轉(zhuǎn)換成尺寸為i-1的另一個(gè)規(guī)則,或分裂為尺寸為?i/2?的兩個(gè)規(guī)則,因而總的轉(zhuǎn)換次數(shù)不超過(guò)這個(gè)值非常接近于(k+1)?u?v.□由下述引理1~引理4可以看出算法1中轉(zhuǎn)換運(yùn)算(1)~轉(zhuǎn)換運(yùn)算(10)的正確性.引理1.下述表達(dá)式在三值邏輯中是恒等式:證明:利用定義3即可完成證明.設(shè)I為三值解釋.(1)II(~~V)≡1-II(~V)≡1-(1-II(V))≡II(V);(2)II(~(V∧W))≡1-II(V∧W)≡1-min(II(V),II(W))≡max(1-II(V),1-II(W))≡II(~V∨~W);(3)II(~(V∨W))≡1-II(V∨W)≡1-max(II(V),II(W))≡min(1-II(V),1-II(W))≡II(~V)∧II(~W);(6)由“”邏輯連接符的含義可立即得到II(VW)≡II(V∨~W).□引理2.設(shè)r:A←WH∧(V∧W)∧WT,r1:A←WH∧V∧WT,r2:A←WH∧W∧WT,I=<T;F>為三值解釋.I是r的語(yǔ)義,當(dāng)且僅當(dāng)I是r1和r2的語(yǔ)義.證明:“?”的證明:不妨設(shè)A為一個(gè)基本原子.(1)若A∈T,即II(A)=1,由II的定義可知,II(A)≥II(WH∧V∧WT)且II(A)≥II(WH∧W∧WT).由定義3可知,II(r1)=1,II(r2)=1,因而I是r1和r2的語(yǔ)義;引理4.設(shè)r:A←WH∧~?XW∧WT,r1:A←WH∧~p(Y1,…,Yk)∧WT,r2:p(Y1,…,Yk)←?XW,I=<T;F>為三值解釋.這里p/k為新引入的k-元謂詞,它不在表達(dá)式A,WH,~?XW及WT中出現(xiàn),Y1,…,Yk為?XW中的全部自由變?cè)?那么,I是r的語(yǔ)義,當(dāng)且僅當(dāng)I′=<T′;F′>是r1和r2的語(yǔ)義.這里,綜上所述,若I是r的語(yǔ)義,則I′是r1和r2的語(yǔ)義.“?”的證明過(guò)程與“?”證明的逆過(guò)程類(lèi)似,這里不再贅述.□定理2說(shuō)明,算法1在轉(zhuǎn)換安全策略的過(guò)程中引入的新謂詞雖然向原安全策略的語(yǔ)義中增加了一些新的基本原子,但這對(duì)原安全策略的語(yǔ)義并不構(gòu)成實(shí)質(zhì)性的影響,因而是可靠的.定理3說(shuō)明,算法1具有保持安全策略語(yǔ)義的能力,因而是完備的.由引理1~引理4,容易證明算法1的可靠性和完備性.定理2(算法1的可靠性).設(shè)SP為一個(gè)安全策略,SP經(jīng)算法1轉(zhuǎn)換后所得結(jié)果為SP′,M′=<T′;F′>為SP的一個(gè)三值語(yǔ)義,N為轉(zhuǎn)換過(guò)程中由轉(zhuǎn)換運(yùn)算(10)新引入的所有謂詞構(gòu)成的集合,則M=<T;F>是SP的一個(gè)三值語(yǔ)義.這里,證明:由M′=<T′;F′>為三值模型可得,T′∩F′=?,容易看出T?T′,F?F′,因而T∩F=?.由引理1~引理4可直接推導(dǎo)出,SP中的每個(gè)規(guī)則在M′=<T′;F′>中的真值都為真.由于集合T和F僅是從T′和F′中去除了那些對(duì)SP中規(guī)則的真值賦值不會(huì)產(chǎn)生影響的基本原子(這是因?yàn)檫@些原子所對(duì)應(yīng)的謂詞都是在轉(zhuǎn)換過(guò)程中新引入的),因而SP中的每個(gè)規(guī)則在M中的真值也都為真.綜上所述,M=?T;F?是SP的一個(gè)三值語(yǔ)義.□定理3(算法1的完備性).設(shè)SP為安全策略,M=<T;F>為SP的三值語(yǔ)義,SP經(jīng)算法1轉(zhuǎn)換后所得結(jié)果SP′則存在M′=<T′;F′>,其中,T?T′?HBSP′,F?F′?HBSP′,M′是SP′的三值語(yǔ)義.證明:由定理1可知,算法1可在有限步內(nèi)轉(zhuǎn)換完畢.設(shè)算法1應(yīng)用于SP總的轉(zhuǎn)換次數(shù)為m,且這些轉(zhuǎn)換運(yùn)算構(gòu)成的序列依次為τ1,...,τm.設(shè)SP經(jīng)過(guò)前i-1次轉(zhuǎn)換后所得到的安全策略記為SPi-1,令M0=M,Mi=<Ti;Fi>構(gòu)造方法如下所示:1)若τi為轉(zhuǎn)換運(yùn)算(1)~轉(zhuǎn)換運(yùn)算(9),令Mi=Mi-1.由引理1~引理3可知,若Mi-1是SPi-1的語(yǔ)義,則Mi是SPi的語(yǔ)義;2)若τi為轉(zhuǎn)換運(yùn)算(10),則被轉(zhuǎn)換的規(guī)則為A←WH∧~?XW∧WT,pi/k為新引入的k-元謂詞,Y1,…,Yk為?XW中的全部自由變?cè)?令Mi=<Ti;Fi>,其中,由引理4可知,若Mi-1是SPi-1的語(yǔ)義,則Mi是SPi的語(yǔ)義.□定理2和定理3保證了通過(guò)擴(kuò)展型邏輯程序的良基語(yǔ)義定義安全策略語(yǔ)義的合理性.定義7(安全策略的良基語(yǔ)義).設(shè)SP為安全策略,SP經(jīng)算法1轉(zhuǎn)換后所得結(jié)果為SP′,M′=<T′;F′>為SP的良基語(yǔ)義,N為轉(zhuǎn)換過(guò)程中由轉(zhuǎn)換運(yùn)算(10)新引入的所有謂詞構(gòu)成的集合,則稱(chēng)M=<T;F>是SP的良基語(yǔ)義這里,4查詢(xún)目標(biāo)的語(yǔ)義查詢(xún)問(wèn)題的求解本節(jié)討論基于良基語(yǔ)義的安全策略語(yǔ)義查詢(xún)問(wèn)題,進(jìn)而構(gòu)造出安全策略決策算法和驗(yàn)證算法.首先討論查詢(xún)目標(biāo)為←p(t)形式的表達(dá)式(即基本查詢(xún)目標(biāo))時(shí)安全策略語(yǔ)義查詢(xún)問(wèn)題,并給出相應(yīng)的算法,該算法可應(yīng)用于安全策略決策等方面;其次,討論查詢(xún)目標(biāo)為一階邏輯表達(dá)式(即復(fù)雜查詢(xún)目標(biāo))時(shí)安全策略語(yǔ)義查詢(xún)問(wèn)題,并給出相應(yīng)的算法,該算法可應(yīng)用于安全策略驗(yàn)證等方面.4.1u3000結(jié)論設(shè)SP為安全策略,M為SP的良基語(yǔ)義,p/n為SP中的一個(gè)謂詞,為n元原子.那么存在哪些n元基本置換θ可以使得θ為SP關(guān)于M的邏輯結(jié)果呢?這個(gè)問(wèn)題稱(chēng)為安全策略基本查詢(xún)問(wèn)題.本節(jié)基于算法1給出了一種安全策略基本查詢(xún)問(wèn)題的求解方法,其基本思想如算法2所示.這里,R為SLG算法返回的查詢(xún)結(jié)果.SLG算法和XSB系統(tǒng)的相關(guān)信息可參考文獻(xiàn).(1)如果R=?,則說(shuō)明不存在基本置換使得原子在SP的良基語(yǔ)義中成立.由于本文認(rèn)為良基語(yǔ)義是擴(kuò)展型邏輯程序的正則語(yǔ)義,因而可以斷言,?在SP中是不成立的;(2)如果R≠?,則說(shuō)明存在基本置換使得原子在SP的良基語(yǔ)義中成立,因而可以斷言,?在SP中是成立的;(3)如果XSB系統(tǒng)返回Floundering警告,則無(wú)法判定在SP中是否成立.算法2.安全策略語(yǔ)義基本查詢(xún)算法.定理4(安全策略基本查詢(xún)算法的可靠性和完備性).θ是SP相對(duì)于M的邏輯結(jié)果,當(dāng)且僅當(dāng)θ是SP′相對(duì)于其良基語(yǔ)義M′的邏輯結(jié)果.證明:由算法1的可靠性(定理2)和完備性(定理3)可直接得證.□安全策略語(yǔ)義基本查詢(xún)算法經(jīng)過(guò)簡(jiǎn)單變換后可處理←形式的查詢(xún)目標(biāo),主要用于策略決策等方面.4.2安全策略驗(yàn)證算法安全屬性不變式通常是比較復(fù)雜的一階邏輯表達(dá)式,安全策略語(yǔ)義基本查詢(xún)算法只能處理形式較為簡(jiǎn)單的(僅含有一個(gè)原子的)查詢(xún)目標(biāo),因而無(wú)法滿足安全策略驗(yàn)證的需求.為了解決安全策略驗(yàn)證問(wèn)題,本節(jié)首先給出了將安全策略復(fù)雜查詢(xún)問(wèn)題轉(zhuǎn)化為安全策略簡(jiǎn)單查詢(xún)問(wèn)題的算法(參見(jiàn)算法3),并且證明了該算法的可靠性和完備性;其次,利用安全策略語(yǔ)義基本查詢(xún)算法構(gòu)造出安全策略復(fù)雜查詢(xún)算法,該算法主要用于安全策略驗(yàn)證,因而本文稱(chēng)其為安全策略驗(yàn)證算法.由于安全策略驗(yàn)證算法是基于安全策略語(yǔ)義基本查詢(xún)算法的,因而安全策略驗(yàn)證和安全策略決策使用相同的語(yǔ)義,可有效避免本文引言中提到的驗(yàn)證失效等問(wèn)題的產(chǎn)生.算法3.安全策略復(fù)雜查詢(xún)轉(zhuǎn)換.設(shè)SP為安全策略,M為SP的良基語(yǔ)義,Q為不含“←”的任意形式的一階邏輯表達(dá)式,X1,…,Xn為Q中的全部自由變?cè)?那么存在哪些n元基本置換可以使得Q為SP關(guān)于M的邏輯結(jié)果呢?這個(gè)問(wèn)題稱(chēng)為安全策略復(fù)雜查詢(xún)問(wèn)題,記為<SP,Q>.設(shè)ans/n為一個(gè)未在SP中出現(xiàn)過(guò)的n元謂詞符號(hào),則算法3可以將<SP,Q>轉(zhuǎn)換成另一個(gè)等價(jià)的安全策略基本查詢(xún)問(wèn)題<SP″,ans(X1,…,Xn)>.這里,SP″為擴(kuò)展型邏輯程序.定理5證明了算法3的可靠性和完備性.定理6證明了算法3的可終止性.定理5(算法3的可靠性和完備性).在算法3中,設(shè)M=?T;F?是SP的良基語(yǔ)義,令則有:(1)M′=<T′;F′>是擴(kuò)展型邏輯程序SP′的良基語(yǔ)義;(2)IM(?(Q))=1當(dāng)且僅當(dāng)IM′(?(ans(X1,...,Xn)))=1.證明:(1)由文獻(xiàn)的定義3.3及T′和F′的構(gòu)造方法可直接得出M′是SP′的良基語(yǔ)義,即上面的(1)成立(2)“?”的證明:由于M′是SP′的語(yǔ)義,則IM′(ans(X1,...,Xn)←Q)=1.若IM(?(Q))=1,易知IM′(?(Q))=1,即存在基本置換θ={X1a1,...,Xnan}使得IM′(Q|X1a1,...,Xnan)=1.由定義3可知:即IM′(ans(a1,...,an))≡IM′(?(ans(X1,...,Xn)))=1.反之,若IM′(?(ans(X1,...,Xn)))=1,不妨設(shè)IM′(ans(a1,...,an))=1.這里,a1,...,an∈HUSP.由于ans(a1,…,an)僅能由規(guī)則ans(X1,…,Xn)←Q推導(dǎo)出來(lái),并且M′是SP′的良基語(yǔ)義,因而IM′(Q|X1a1,...,Xnan)=1.由M′=<T′;F′>構(gòu)造方法可知,IM(Q|X1a1,...,Xnan)=1,即IM(?(Q))=1.“?”的證明與“?”證明的逆過(guò)程類(lèi)似,這里不再贅述.□定理6(算法3的可終止性).算法3可在有限步內(nèi)轉(zhuǎn)換完畢,其總的轉(zhuǎn)換次數(shù)是多項(xiàng)式級(jí)的.證明:該結(jié)論是定理1的直接推論.□至此,本文給出了將安全策略轉(zhuǎn)換成擴(kuò)展型邏輯程序及將安全策略查詢(xún)問(wèn)題轉(zhuǎn)換成擴(kuò)展型邏輯程序查詢(xún)問(wèn)題的算法,并且證明了這些算法在良基語(yǔ)義下的可終止性、可靠性和完備性.下面將利用這些結(jié)論構(gòu)建安全策略驗(yàn)證算法.為了使驗(yàn)證算法具有足夠高的效率,本文假設(shè):(1)安全策略中每個(gè)規(guī)則A←Wff的Wff中不含有任何函數(shù)符號(hào);(2)待驗(yàn)證的安全屬性都可以表示成一個(gè)不含邏輯連接符“←”和函數(shù)符號(hào)的一階邏輯表達(dá)式;(3)為了保證安全策略驗(yàn)證過(guò)程的可靠性和完備性,每個(gè)待驗(yàn)證的安全屬性都是一個(gè)non-Floundering查詢(xún)對(duì)于那些無(wú)法表示成non-Floundering查詢(xún)的安全屬性,則不在本文考慮的范圍之內(nèi).安全策略驗(yàn)證算法的結(jié)構(gòu)如算法4所示.在該算法中,首先利用算法3,將安全策略SP和待驗(yàn)證的安全屬性不變式Q構(gòu)成的安全策略復(fù)雜查詢(xún)問(wèn)題?SP,Q?轉(zhuǎn)換成安全策略簡(jiǎn)單查詢(xún)問(wèn)題<SP″,ans(X1,…,Xn)>.由于SP″是擴(kuò)展型邏輯程序,ans(X1,…,Xn)是基本查詢(xún)目標(biāo),因而XSB系統(tǒng)可高效地計(jì)算它并返回查詢(xún)結(jié)果R:(1)如果R=?,則說(shuō)明不存在基本置換使得安全屬性不變式Q在SP的良基語(yǔ)義中成立.由于本文認(rèn)為良基語(yǔ)義是擴(kuò)展型邏輯程序的正則語(yǔ)義,因而可以斷言,?(Q)在SP中是不成立的;(2)如果R≠?,則說(shuō)明存在基本置換使得Q在SP的良基語(yǔ)義中成立,因而?(Q)在SP中成立;(3)如果XSB系統(tǒng)返回Floundering警告,則說(shuō)明無(wú)法判定?(Q)在SP中是否成立.算法4.安全策略驗(yàn)證算法.定理7(安全策略查詢(xún)算法的可靠性和完備性).設(shè)M是SP的良基語(yǔ)義,則?(Q)是SP相對(duì)于M的邏輯結(jié)果當(dāng)且僅當(dāng)?(ans(X1,…,Xn))是SP″相對(duì)于其良基語(yǔ)義M″的邏輯結(jié)果.證明:該結(jié)論是定理5的直接推論.□至此,我們已經(jīng)完成了安全策略語(yǔ)言的設(shè)計(jì)、安全策略語(yǔ)義的定義及安全策略語(yǔ)義查詢(xún)算法和驗(yàn)證算法的設(shè)計(jì).接下來(lái),我們將這些研究成果組合起來(lái),形成一個(gè)切實(shí)可用的安全策略管理框架WF-SPevf.5wf-spevf的使用WF-SPevf的整體架構(gòu)如圖1所示,可在統(tǒng)一的安全策略良基語(yǔ)義下實(shí)現(xiàn)以下主要功能:·安全策略表達(dá):安全管理員根據(jù)系統(tǒng)安全需求,通過(guò)安全策略語(yǔ)言SPL制定安全策略,并存儲(chǔ)到策略庫(kù)中;·安全策略查詢(xún):信息系統(tǒng)根據(jù)具體應(yīng)用場(chǎng)景形成基本查詢(xún)目標(biāo)提交給WF-SPevf.WF-SPevf根據(jù)安全策略及查詢(xún)目標(biāo),通過(guò)安全策略語(yǔ)義基本查詢(xún)算法計(jì)算出查詢(xún)結(jié)果并反饋給信息系統(tǒng);·安全屬性表達(dá):安全專(zhuān)家根據(jù)系統(tǒng)特性提煉出系統(tǒng)應(yīng)具備的安全屬性,然后通過(guò)安全策略語(yǔ)言SPL表達(dá)出來(lái),形成安全屬性不變式.值得注意的是,WF-SPevf使用相同的語(yǔ)言表達(dá)安全屬性和安全策略,這是WF-Spevf與其他安全策略驗(yàn)證工具的一個(gè)顯著不同點(diǎn);·安全策略驗(yàn)證:WF-SPevf根據(jù)安全策略和安全屬性不變式,自動(dòng)地驗(yàn)證兩者之間的符合性.如果安全策略滿足安全屬性不變式,則驗(yàn)證通過(guò);否則,安全策略中存在錯(cuò)誤或不足.此時(shí),WF-SPevf提供完整的出錯(cuò)原因,以便于安全管理員調(diào)試安全策略.值得注意的是,安全策略驗(yàn)證和安全策略查詢(xún)使用相同的語(yǔ)義,這是WF-Spevf與其他驗(yàn)證技術(shù)最重要的區(qū)別.由于安全屬性不變式本質(zhì)上是一階邏輯表達(dá)式,因此WF-SPevf還可用于其他能夠表達(dá)成一階邏輯表達(dá)式的屬性判定問(wèn)題,如策略沖突檢測(cè)等.在WF-SPevf中,安全策略語(yǔ)言、安全策略語(yǔ)義查詢(xún)算法和安全策略驗(yàn)證算法構(gòu)成一個(gè)有機(jī)的整體.它們?cè)诮y(tǒng)一的語(yǔ)義下對(duì)外提供策略表達(dá)、策略決策、策略驗(yàn)證等服務(wù).WF-SPevf具備強(qiáng)大的描述能力、高效的策略決策算法及強(qiáng)健的策略驗(yàn)證能力.與現(xiàn)有的安全策略框架相比,具有鮮明的特色.因此有理由相信,WF-SPevf可為管理人員提供快捷、方便和易用的安全策略管理服務(wù).下面通過(guò)實(shí)例說(shuō)明WF-SPevf的使用方法.設(shè)信息系統(tǒng)中存在由下列規(guī)則構(gòu)成的信息流安全策略:規(guī)則1.對(duì)于任意給定的用戶(hù)U和文件F(每個(gè)文件至少具有一個(gè)祖先目錄),如果F的安全級(jí)別不支配U的安全級(jí)別,同時(shí)至少有一個(gè)管理員允許U讀取F的所有祖先目錄,且沒(méi)有管理員禁止U讀取F的任一祖先目錄,則允許U讀取F.規(guī)則2.對(duì)于任意給定的用戶(hù)U和文件F,如果U的安全級(jí)別不支配F的安全級(jí)別,則允許U寫(xiě)F.規(guī)則3.系統(tǒng)中已有的實(shí)體(用戶(hù)或文件)及其安全級(jí)別分別為(f1,b),(f2,u),(f3,d),(s1,d),(s2,u),(s3,a),其中,fi為文件,sj為用戶(hù).規(guī)則4.安全級(jí)別L={a,b,u,d,e}之間的支配關(guān)系如圖2(a)所示,它們構(gòu)成格.規(guī)則5.文件夾t為文件f1≤i≤3的祖先,且管理員adm1和adm2授予用戶(hù)s1和s2讀取文件夾t的權(quán)限.(1)用SPL表示安全策略文獻(xiàn)中提出的安全策略語(yǔ)言不支持量詞,無(wú)法簡(jiǎn)單地表示上述安全策略.然而,SPL可簡(jiǎn)單地將上述安全策略表示成下列形式:其中,R1對(duì)應(yīng)規(guī)則1,R2對(duì)應(yīng)規(guī)則2,C1~C6對(duì)應(yīng)規(guī)則3,D1~D6對(duì)應(yīng)規(guī)則4,E1~E6對(duì)應(yīng)規(guī)則5.permit/3,ancestor/2authen/2,authoz/4,deny/4,secLevel/2和?/2都為謂詞符號(hào),表達(dá)的含義是不言自明的.(2)安全策略決策判斷P是否允許s1讀取f1的過(guò)程如下(參見(jiàn)算法2):首先,利用算法1將P轉(zhuǎn)換成擴(kuò)展型邏輯程序P′;然后,利用XSB系統(tǒng)評(píng)估查詢(xún)<P′,permit(s1,f1,read)>,即可獲得最終的判決結(jié)果.利用算法1轉(zhuǎn)換P中R1的過(guò)程如下所示:連續(xù)3次應(yīng)用轉(zhuǎn)換運(yùn)算(9)后,R1可被轉(zhuǎn)換成公式(4)所示的規(guī)則:應(yīng)用轉(zhuǎn)換運(yùn)算(7),公式(4)所示的規(guī)則可轉(zhuǎn)換成公式(5)所示的規(guī)則:應(yīng)用轉(zhuǎn)換運(yùn)算(10),公式(5)所示的規(guī)則可轉(zhuǎn)換成公式(6)和公式(7)所示的兩個(gè)規(guī)則:已經(jīng)沒(méi)有轉(zhuǎn)換運(yùn)算可應(yīng)用于公式(6).應(yīng)用轉(zhuǎn)換運(yùn)算(9),公式(7)所示的規(guī)則可轉(zhuǎn)換為公式(8)所示的規(guī)則:應(yīng)用轉(zhuǎn)換運(yùn)算(3),公式(8)所示的規(guī)則可轉(zhuǎn)換成公式(9)所示的規(guī)則:應(yīng)用轉(zhuǎn)換運(yùn)算(1),公式(9)所示規(guī)則可轉(zhuǎn)換成公式(10)和公式(11)所示的兩個(gè)規(guī)則:已經(jīng)沒(méi)有轉(zhuǎn)換運(yùn)算可應(yīng)用于公式(10).應(yīng)用轉(zhuǎn)換運(yùn)算(9),公式(11)所示規(guī)則可轉(zhuǎn)換成公式(12)所示的規(guī)則:已經(jīng)沒(méi)有轉(zhuǎn)換運(yùn)算可應(yīng)用于公式(12),轉(zhuǎn)換過(guò)程結(jié)束,因而R1被轉(zhuǎn)換成3個(gè)擴(kuò)展型邏輯程序規(guī)則{T1,T2,T3}最終,算法1將P轉(zhuǎn)換成擴(kuò)展型邏輯程序P′=(P-{R1})∪{T1,T2,T3}.將P轉(zhuǎn)換成P′后,利用XSB邏輯程序查詢(xún)引擎評(píng)估查詢(xún)<P′,permit(s1,f1,read)>,查詢(xún)結(jié)果集為空集,具體的查詢(xún)?cè)u(píng)估過(guò)程參見(jiàn)文獻(xiàn).這說(shuō)明,P不允許s1直接讀取f1,如圖2(b)所示.(3)安全屬性驗(yàn)證P是一個(gè)信息流安全策略.從信息流的角度來(lái)看,為了保護(hù)機(jī)密性,高安全級(jí)別客體中的信息應(yīng)無(wú)法流向低安全級(jí)別的客體,即P應(yīng)該能夠滿足SPL安全屬性不變式Q:這里,安全屬性不變式Q表示“高安全級(jí)別客體中的信息應(yīng)無(wú)法流向低安全級(jí)別的客體”.為了判定P是否滿足Q,需要向原安全策略P中加入下列兩個(gè)用于刻畫(huà)信息流向的規(guī)則:V1:canFlowTo(O1,O2)←permit(S,O1,read),permit(S,O2,write),V2:canFlowTo(O1,O3)←canFlowTo(O1,O2),canFlowTo(O2,O3),其中,規(guī)則V1表示,對(duì)于給定的用戶(hù)S、客體O1和O2,如果S能夠讀取O1,同時(shí)S能夠向O2中寫(xiě)入信息,則O1中的信息能夠流向O2;規(guī)則V2表示信息流向具有傳遞性.顯然,將V1和V2加入P中不會(huì)改變P原有的安全屬性.令P″=P∪{V1,V2},驗(yàn)證P是否滿足Q的過(guò)程如下所示(參見(jiàn)算法4):首先,利用算法3將復(fù)雜查詢(xún)<P″,Q>轉(zhuǎn)換成基本查詢(xún)<Pflow,tmp>.由算法3和算法1容易得到擴(kuò)展型邏輯程序Pflow,其中,tmp和p是在轉(zhuǎn)換<P″,Q>的過(guò)程中新引入的0元