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

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

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