概率時間安全進(jìn)程代數(shù)及其無干擾性分析

概率時間安全進(jìn)程代數(shù)及其無干擾性分析

在多級安全系統(tǒng)中，訪問控制策略，并確定不同安全級之間的通信行為。它可以有效地控制隱性非法信息流，防止低級安全級和高級安全級之間的直接非法通信。然而，惡意特洛伊木馬程序和事件可以通過系統(tǒng)中可能存在的隱藏通道（中間通道）間接傳輸信息，并接收高安全級實(shí)體的機(jī)密信息。顯式和隱式的信息通信,都可看作是不同安全級進(jìn)程間信息的流動,而且信息流分析對所有的信息流動進(jìn)行分析和控制.因此,信息流分析能更好地刻畫和控制不同安全級主體間信息的傳遞.在信息流分析的研究中,文獻(xiàn)提出了無干擾(non-interference)的概念.無干擾可理解為低安全級主體不能通過觀察高安全級主體的動作推導(dǎo)出任何信息.它為分析隱蔽通道提供了有效的手段.大量文獻(xiàn)基于無干擾性分析了系統(tǒng)的安全性,進(jìn)而提出了若干基于無干擾的信息流安全屬性.但是,它們無法捕獲通過控制動作執(zhí)行的概率或特定動作執(zhí)行的時間來構(gòu)造的隱蔽通道.因此在文獻(xiàn)和文獻(xiàn)中分別引入了時間配置和概率配置,對原有理論進(jìn)行了擴(kuò)展,使其具備描述時間信息和概率信息,分析時間隱蔽通道和概率隱蔽通道的能力.但是,攻擊者可以同時利用概率和時間信息來構(gòu)造更復(fù)雜的隱蔽通道以逃避檢測,這樣的隱蔽通道稱為概率時間隱蔽通道.僅考慮概率信息或時間信息的信息流安全屬性無法對這樣的隱蔽通道進(jìn)行捕獲.一個系統(tǒng)經(jīng)過概率信息流分析或時間信息流動分析沒有發(fā)現(xiàn)隱蔽通道,并不意味著是安全的.孤立地從概率信息或時間信息上分析,無法捕獲概率時間隱蔽通道.因此須有一個統(tǒng)一的框架,同時考慮概率和時間信息,對概率時間信息流進(jìn)行分析.安全進(jìn)程代數(shù)(securityprocessalgebra,SPA)是進(jìn)行信息流安全性分析最經(jīng)典的方法之一,它能分析多級安全系統(tǒng)中信息流安全屬性,但是它僅針對非確定性行為,無法描述動作的概率信息和時間信息.因此文獻(xiàn)在概率配置下對其進(jìn)行了擴(kuò)展,提出了概率安全進(jìn)程代數(shù)PSPA,使其具備描述概率行為的能力.但是在概率環(huán)境下安全的系統(tǒng),若考慮了時間因素,則仍可能出現(xiàn)安全問題.因此有必要同時考慮系統(tǒng)的概率和時間因素.為研究概率時間配置下的系統(tǒng)行為,本文在此基礎(chǔ)上進(jìn)行擴(kuò)展,提出概率時間安全進(jìn)程代數(shù)ptSPA(probabilistictimeSPA),使其能夠同時描述概率信息和時間信息.基于ptSPA,描述系統(tǒng)的概率、時間行為,分析概率時間信息流的安全屬性.文本的主要貢獻(xiàn)包括:1)定義了概率時間系統(tǒng)下的安全進(jìn)程代數(shù)ptSPA;2)擴(kuò)展了在概率時間系統(tǒng)下信息流相關(guān)的無干擾屬性;3)證明了概率時間系統(tǒng)中的屬性與概率系統(tǒng)中的屬性、時間系統(tǒng)中的屬性的關(guān)系;4)為基于進(jìn)程代數(shù)分析時間概率系統(tǒng)提供了一種理論基礎(chǔ).1ppsq在文獻(xiàn)中,Focardi和Gorrieri以CCS為基礎(chǔ),引入CSP中的隱藏算子和限制算子,提出了安全進(jìn)程代數(shù)SPA,文獻(xiàn)利用SPA對非確定系統(tǒng)建模,并對其信息流安全屬性進(jìn)行分析.隨后在文獻(xiàn)中,Aldini以SPA為基礎(chǔ),基于生成反應(yīng)轉(zhuǎn)移系統(tǒng)(generative-reactivetransitionsystems,GRTS),提出了概率安全進(jìn)程代數(shù)PSPA,并對信息流的若干概率安全屬性進(jìn)行了分析.本節(jié)以PSPA為基礎(chǔ),提出概率時間安全進(jìn)程代數(shù)ptSPA.本節(jié)首先簡要介紹GRTS模型,然后在GRTS模型下給出ptSPA的語法及操作語義,而后在ptSPA中引入概率時間互擬等價的概念,并證明相關(guān)命題.本節(jié)的主要工作為后續(xù)章節(jié)提供理論基礎(chǔ).1.1生成反應(yīng)轉(zhuǎn)移系統(tǒng)本文選用GRTS作為概率模型.該模型可同時表達(dá)概率信息和外部環(huán)境的非確定性特征.GRTS可以看作標(biāo)簽轉(zhuǎn)移系統(tǒng)的一個擴(kuò)展,它的標(biāo)簽由輸入動作、輸出動作和概率組成.在GRTS中輸出動作為生成動作,由于其行為是主動的,因此它基于概率分布自動地生成要執(zhí)行的動作.輸入動作為反應(yīng)動作,由于其行為是根據(jù)外部環(huán)境被動地按概率分布作出的反應(yīng),依賴于外部環(huán)境,因此它的動作選擇是非確定的,所以反應(yīng)動作是不完全動作,它必須要和其他系統(tǒng)組件的生成動作進(jìn)行同步才能構(gòu)成封閉系統(tǒng).可被P執(zhí)行的生成動作的轉(zhuǎn)移概率之和,以進(jìn)行歸一化處理.在P‖pSQ中可被P執(zhí)行的生成動作集合為GS,Q={a∈AΤype|a?S∨(a∈S∧Qa*→)},其中S?ATpey-{τ},Q∈ξ.P和Q若能在a*上或a與a*上同步,則它們同步的時間為這2個動作時延時間的較大者,時延小的動作阻塞地等待時延大的動作執(zhí)行.P/pL表示以p的概率隱藏進(jìn)程P在動作集L中的動作.隱藏算子P/pa將類型為a的生成動作和反應(yīng)動作轉(zhuǎn)換為內(nèi)部動作τ,并根據(jù)如下規(guī)則修改概率分布:1)若P既能執(zhí)行生成動作a,也能執(zhí)行反應(yīng)動作a*,則P/pa按概率p選擇由反應(yīng)動作a*轉(zhuǎn)換而得的τ,以1-p選擇生成動作a;2)若P不能執(zhí)行反應(yīng)動作或生成動作a*,則不考慮P/pa中的概率p.表1中未給出限制算子P\pL的語義,因為P\pL可由P‖pL0而得.P‖pL0表示P和0與同步集L中的動作同步,若執(zhí)行L中的動作,系統(tǒng)將發(fā)生死鎖.即阻止P中L的執(zhí)行.例1.考慮如下項:P2≡((νt1(a)+qνt2(b))+q′νt3(c*))‖p{c}νt4(c).它的左邊進(jìn)程執(zhí)行2個不需同步的生成動作a和b,和一個需要與右邊的生成動作同步的反應(yīng)動作c*.在選擇組合的情況下,2個進(jìn)程都能執(zhí)行某些生成動作,執(zhí)行左邊進(jìn)程的概率是p,執(zhí)行右邊進(jìn)程的概率是1-p.因為(νt1(a)+qνt2(b))執(zhí)行生成動作a的概率是q,執(zhí)行生成動作b的概率為1-q(根據(jù)組合選擇的概率機(jī)制,不考慮q′),項P2執(zhí)行νt1(a)的概率為p·q,執(zhí)行動作νt2(b)的概率為p(1-q),執(zhí)行動作νmax(t3,t4)(c)的概率為1-p.1.3概率時間安全進(jìn)程代數(shù)的弱互擬等價互相似是一種行為等價,它使得在驗證一個系統(tǒng)的某個屬性時,可以通過尋找滿足該屬性的其他系統(tǒng),然后比較這2個系統(tǒng)之間的互相似性來驗證待測系統(tǒng)是否滿足這個屬性.2個系統(tǒng)A和A′互相似,當(dāng)其中一個系統(tǒng)執(zhí)行某個動作到達(dá)某個狀態(tài)s時,另一個系統(tǒng)可通過執(zhí)行同樣的動作來模擬這一步,到達(dá)狀態(tài)s′,使得s與s′仍然互相似.2個系統(tǒng)間的互擬即基于這種一步步模擬的思想.弱互擬是不考慮內(nèi)部動作的互擬,因此當(dāng)一個系統(tǒng)在模擬另一個系統(tǒng)的一個動作時,這個系統(tǒng)可以在執(zhí)行這個動作的前后執(zhí)行若干步內(nèi)部動作.為了抽象掉內(nèi)部動作τ,Milner引入了可觀察步驟的概念,它由一個可見動作α和任意數(shù)量的內(nèi)部動作組成.這樣的動作通過弱轉(zhuǎn)移關(guān)系?來描述,定義α?=(τ→)*α→(τ→)*,其中→是強(qiáng)轉(zhuǎn)移關(guān)系.將內(nèi)部觀察步驟定義為τ?=(τ→)*,易知弱內(nèi)部轉(zhuǎn)移τ?可以不執(zhí)行任何內(nèi)部動作.Baier和Hermanns引入了Prob(s,τ*,s′)表示從狀態(tài)s執(zhí)行若干內(nèi)部動作后,到達(dá)s′的概率來代替Miller的弱內(nèi)部轉(zhuǎn)移sτ?s′.通過概率Prob(s,α*,s′)表示從s執(zhí)行若干可見動作后,到達(dá)的概率來定義sα?s′.首先給出弱互擬(weakbisimulatioin)基于非確定算子的經(jīng)典定義.定義2.對于給定的二元關(guān)系R?ξnd×ξnd,若(P,Q)∈R,對所有的a∈Act,有:1)當(dāng)Ρa→Ρ′,則存在Q′∈ξnd,使得Qa?Q′,且(P′,Q′)∈R.2)當(dāng)Qa→Q′,則存在P′∈ξnd,使得Ρa?Ρ′,且(P′,Q′)∈R.則稱R是弱互擬的,其中ξnd表示非確定性進(jìn)程.當(dāng)存在(P,Q)∈R,其中R是一個弱互擬關(guān)系,R,Q∈ξnd,則稱項P,Q弱互擬等價,記為P≈BQ.容易證明≈B是一個等價關(guān)系.受文獻(xiàn)啟發(fā),本節(jié)引入Prob(P,νt(α*),P′)來表示進(jìn)程P經(jīng)過若干動作或時間后到達(dá)進(jìn)程P′的概率,其中α∈((Σ∪{τ})×Π).定義3.設(shè)C為從進(jìn)程P經(jīng)νt(τ*α)可達(dá)的進(jìn)程集.記Prob(P,νt(τ*α),C)為從P通過序列νt(τ*α)到C中的項的概率.Ρrob(Ρ,νt(τ*α),C)={1,α=τ∧Ρ∈C;∑Q∈ξΡrob(Ρ,νt′(τ),Q)Ρrob(Q,νt″(τ*),C),α=τ∧Ρ?C;∑Q∈ξΡrob(Ρ,νt′(τ),Q)Ρrob(Q,νt″(τ*α,C))+Ρrob(Q,νΔt(α),C),α=Σ×Π.定義4.概率時間弱互擬.對于給定的二元關(guān)系R?ξ×ξ.若(P,Q)∈R,P′,Q′∈C,有:Ρrob(Ρ,νt(τ*α),C)=Ρrob(Q,νt(τ*α),C)且Ρt→Ρ′,Qt→Q′?(Ρ′,Q′)∈R,則稱關(guān)系R為概率時間弱互擬關(guān)系.稱滿足(P,Q)∈R的進(jìn)程P和Q概率時間弱互擬等價,記為≈PTB.定義5.若P∈ξ是一個概率時間配置下的進(jìn)程,在忽略P中所有時間信息,并重新計算因去掉時間信息而得到的相同動作的概率分布后,得到的進(jìn)程記為untime(P).在忽略P中所有概率信息后,得到的進(jìn)程記為unprob(P).定理1.令≈TB表示時間弱互擬,≈PB表示概率弱互擬.若P≈PTBQ,則unprob(P)≈TBunprob(Q),untime(P)≈PBuntime(Q)(時間弱互擬≈TB及概率弱互擬≈PB的概念分別見文獻(xiàn)).證明.因為P≈PTBQ,有Prob(P,νt(τ*α),C)=Prob(Q,νt(τ*α),C),其中C∈S/R.因此若對某個P′∈C,有Prob(P,νt(α),P′)>0,則存在Q′∈C,Prob(Q,νt(α),Q′)>0,使得Prob(P,νt(α),P′)=Prob(Q,νt(α),Q′),即P經(jīng)過νt(α)到達(dá)P′的概率與Q經(jīng)過νt(α)到達(dá)Q′的概率相等.因此存在:unprob(Ρ)→νt(α)unprob(Ρ′);unprob(Q)→νt(α)unprob(Q′).由于P′和Q′都屬于C,易知unprob(P)和unprob(Q)都屬于CTB.則有(unprob(P′),unprob(Q′))∈RTB,因此,unprob(P)≈TBunprob(Q).同理可證unprob(P)≈PBunprob(Q).證畢.2概率時間隱蔽通道本節(jié)在概率時間環(huán)境下對文獻(xiàn)中的非確定性無干擾理論、文獻(xiàn)中的概率無干擾理論及文獻(xiàn)中的時間無干擾理論進(jìn)行擴(kuò)展,分析了概率時間信息流安全屬性,在此基礎(chǔ)上指出了原有屬性無法描述的概率時間隱蔽通道.2.1概率時間互擬強(qiáng)無干擾PTBSNI屬性在信息流安全屬性的分析中,文獻(xiàn)提出了BSNNI(bisimulationstrongnondeterministicnoninterference)安全屬性.BSNNI指出,若低安全級觀察者觀察到系統(tǒng)隱藏高安全級動作所表現(xiàn)出的執(zhí)行軌跡與系統(tǒng)限制高安全級動作所表現(xiàn)出的執(zhí)行軌跡等價,則低安全級用戶無法通過觀察這兩者的差別來捕獲系統(tǒng)的信息泄露.文獻(xiàn)分別在概率和時間環(huán)境下,對BSNNI進(jìn)行了擴(kuò)展,提出BSPNI和tSNNI屬性.但是,BSPNI屬性僅能捕獲概率隱蔽通道,tSNNI僅能捕獲時間隱蔽通道.以上2個屬性都無法描述概率時間隱蔽通道,因此在文獻(xiàn)的基礎(chǔ)上,在概率時間環(huán)境下提出概率時間互擬強(qiáng)無干擾(probabilisticandtimedbisimulationstrongnoninterference,PTBSNI)屬性.定義6.設(shè)P∈ξ,若P/ATypeH≈PTBP\ATypeH,則稱P∈PTBSNI.與BSNNI,BSPNI,tBSSNI屬性相比,PTBSNI同時考慮了概率和時間因素,以判斷低安全級用戶的概率時間視圖是否獨(dú)立于高安全級用戶的行為.例2.考慮進(jìn)程:P≡(τ.ν1(l).0+0.80τ.ν6(l).0)+0.88h.(τ.ν11(l).0+0.5τ.ν17.l.0).由于P/ATypeH≡(τ.ν1(l).0+0.80τ.ν6(l).0)+0.88τ.(τ.ν11(l).0+0.5τ.ν17(l).0)ue06dPTBν1(l).0+0.80τ.ν6(l).0≡P\ATypeH,因此P?PTBSNI.當(dāng)隱藏高安全級動作時,進(jìn)程P將以0.88的概率執(zhí)行τ.ν1(l).0+0.80τ.ν6(l).0,以0.12的概率執(zhí)行τ.(τ.ν11(l).0+0.5τ.ν17(l).0).而當(dāng)阻止高安全級動作執(zhí)行時,進(jìn)程P將以1的概率動作τ.ν1(l).0+0.80τ.ν6(l).0.所以,低安全級主體可以通過觀察l執(zhí)行時間及概率來判斷進(jìn)程P是否執(zhí)行了動作h.因此,進(jìn)程P是不安全的,它存在概率時間隱蔽通道.攻擊者可以通過P/ATypeH表示發(fā)送0,通過P\ATypeH發(fā)送1來隱蔽地傳遞信息.而若不考慮時間配置,僅僅考慮概率的情況,untime(P)/ATypeH≡(τ.l.0+0.80τ.l.0)+0.88τ.(τ.l.0+0.5τ.l.0)=l.0≈PBl.0=l.0+0.80l.0≡untime(P)\ATypeH.無論h是否執(zhí)行,l.0都將以1的概率執(zhí)行.攻擊者無法區(qū)分untime(P)/ATypeH及untime(P)\ATypeH.因此untime(P)∈BSPNI,此時不存在隱蔽通道.例3.考慮進(jìn)程:P≡(τ.ν1(l).0+0.80τ.ν6(l).0)+0.88h.(τ.ν1(l).0+0.5τ.ν6(l).0).因為P≡(τ.ν1(l).0+0.80τ.ν6(l).0)+0.88τ.(τ.ν1(l).0+0.5τ.ν6(l).0)=τ.ν1(l).0+0.764τ.ν6(l).0ue06dτ.ν1(l).0+0.80τ.ν6(l).0≈PTBP\ATypeH.因此P?PTBSNI,隱藏高安全級動作時,系統(tǒng)執(zhí)行τ.ν1(l).0的概率為0.88×0.80+0.12×0.50=0.764,執(zhí)行τ.ν6(l).0的概率為0.88×0.20+0.12×0.50=0.236.而限制高安全級動作執(zhí)行時,系統(tǒng)執(zhí)行τ.ν1(l).0的概率為0.80,執(zhí)行τ.ν6(l).0的概率為0.20.因此通過判斷τ.ν1(l).0及τ.ν6(l).0的執(zhí)行概率,可以區(qū)分出系統(tǒng)是否執(zhí)行了高安全級動作h.低安全級的攻擊者可以通過觀察執(zhí)行概率的不同來接收高安全級攻擊者發(fā)送的信息,這是一種概率時間隱蔽通道.若此處不考慮概率信息,有:unprob(P)/ATypeH≡(τ.ν1(l).0+τ.ν6(l).0)+τ.(τ.ν1(l).0+τ.ν6(l).0)=τ.ν1(l).0+τ.ν6(l).0≈TBτ.ν1(l).0+τ.ν6(l).0≡unprob(P)\ATypeH.不管高安全級動作h是否執(zhí)行,低安全級用戶都觀察到相同的視圖,即系統(tǒng)非確定性地執(zhí)行τ.ν1(l).0或τ.ν6(l).0.因此unprob(P)∈tBSNNI,即不考慮概率信息,該系統(tǒng)不存在隱蔽通道.以上2例說明,若一個進(jìn)程在不存在時間隱蔽通道和概率隱蔽通道的情況下,是可能存在概率時間隱蔽通道的.雖然基于時間或概率安全進(jìn)程代數(shù)提出的某些安全屬性可以捕獲經(jīng)典安全代數(shù)無法捕獲的那些不易發(fā)現(xiàn)的時間隱蔽通道和概率隱蔽通道,但是它們無法發(fā)現(xiàn)同時考慮時間和概率信息的情況下構(gòu)造的概率事件隱蔽通道,而TBSPNI屬性能夠發(fā)現(xiàn)這樣的隱蔽通道.命題1.PTBSNI?tBSNNI,PTBSNI?BSPNI.證明.由定理1知若P≈PTBQ,則unprob(P)≈TBunprob(Q),untime(P)≈PBuntime(Q).由于P∈PTBSNI,有P/ATypeH≈PTBP\ATypeH,因此有unprob(P/ATypeH)≈TBunprob(P\ATypeH),又由于unprob(P/ATypeH)=unprob(P)/ATypeH,及unprob(P\ATypeH)=unprob(P)\ATypeH.因此可得unprob(P)/ATypeH)≈TBunprob(P)\ATypeH),從而證得unprob(P)∈tBSNNI,因此PTBSNI?tBSNNI.同理可證untime(P)∈BSPNI,因此PTBSNI?BSPNI.證畢.2.2低安全級用戶概率時間視線PTBSNI屬性針對進(jìn)程P獨(dú)立執(zhí)行的情況,判斷低安全級用戶是否能通過P的低安全級視圖區(qū)分高安全級動作是否執(zhí)行來捕獲概率時間隱蔽通道.但是當(dāng)進(jìn)程P與其他惡意的高安全級進(jìn)程交互執(zhí)行時,低安全級用戶能夠從進(jìn)程行為的低安全級視圖中,演繹推導(dǎo)出高安全級行為的概率時間信息,而PTBSNI無法描述進(jìn)程交互的場景.因此提出概率時間互擬組合不可演繹屬性(probabilistictimedbisimulationnondeducibilityoncomposition,PTBNDC)來描述進(jìn)程交互場景下低安全級用戶通過低安全級概率時間視圖發(fā)現(xiàn)概率時間隱蔽通道.BNDC(bisimulationnondeducibilityoncomposition)屬性用于捕獲系統(tǒng)與其他高安全級進(jìn)程進(jìn)行交互時發(fā)生的信息泄露.文獻(xiàn)分別在概率和時間環(huán)境下,對BNDC進(jìn)行擴(kuò)展.提出了PBNDC和tBNDC屬性.本節(jié)同時考慮概率時間條件,提出PTBNDC屬性.定義7.設(shè)P∈ξ,?Λ∈ξH,若P\ATypeH≈PTB((P‖pSΛ)/S)\ATypeH成立,則稱P∈PTBNDC,其中S?STypeH.P\ATypeH表示低安全級用戶觀察P時的視圖,((P‖pSΛ)/S)\ATypeH表示低安全級用戶觀察進(jìn)程P與任意的高安全級進(jìn)程Λ并發(fā)交互后的視圖.若低安全級主體觀察P單獨(dú)執(zhí)行時的行為與P和其他高安全級動作交互后的行為等價,則P滿足PTBNDC屬性.即若進(jìn)程滿足PBNDC性質(zhì),則該進(jìn)程與任何高級進(jìn)程并發(fā)交互時不改變低安全級用戶的概率時間視圖,低安全級用戶的概率時間視圖,不會因進(jìn)程是否與其他高安全級進(jìn)程并發(fā)交互而發(fā)生改變.例4.考慮進(jìn)程:P≡τ.(τ.l1.0+0.80h.ν1(l2).0)+0.80τ.(h.l1.0+0.80τ.ν5(l2).0).假設(shè)P與惡意的高安全級進(jìn)程Λ=h*.0進(jìn)行交互,設(shè)S={h},因為:((P‖pSΛ)/S)\ATypeH=τ.(τ.l1.0+0.80τ.ν1(l2).0)+0.80τ.(τ.l1.0+0.80τ.ν5(l2).0)ue06dPTBτ.(τ.l1.0+0.80τ.ν5(l2).0)≡P\ATypeH,因此,P?PTBNDC.當(dāng)P與惡意進(jìn)程交互時,低安全級的觀察者能夠發(fā)現(xiàn)τ.l1.0+0.80τ.ν1(l2).0及τ.(τ.l1.0+0.80τ.ν5(l2).0)分別以0.80和0.20的概率執(zhí)行.而P不與惡意進(jìn)程交互時,低安全級的觀察者發(fā)現(xiàn)τ.(τ.l1.0+0.80τ.ν5(l2).0)以1的概率執(zhí)行.圖1(a)表示進(jìn)程P的束圖,圖1(b)表示低安全級用戶觀察到的P與Λ=h*.0交互視圖,圖1(c)表示P不與Λ=h*.0交互時低安全級用戶的視圖.低安全級用戶觀察到視圖1(b)(c)的不同,從而可推導(dǎo)出P是否發(fā)生了交互,從而通過控制P與Λ的交互行為來傳遞信息.低安全級用戶通過觀察圖1(b)(c)的不同來區(qū)分并接收傳遞的信息,構(gòu)造概率時間隱蔽通道.若不考慮對動作l2的延時,則untime(P)≡τ.(τ.l1.0+0.80h.l2).0)+0.80τ.(h.l1.0+0.80τ.0),有:((untime(P)‖pSΛ)/S)\ATypeH=τ.(τ.l1.0+0.80τ.l2.0)+0.80τ.(τ.l1+0.80τ.l2)=τ.l1.0+0.80τ.l2.0=τ.τ.l1.0+0.80τ.τ.l2.0≈untime(P)\ATypeH.因此untime(P)∈PBNDC.即不考慮時間信息,進(jìn)程untime(P)滿足PBDNC,其不存在概率隱蔽通道.圖1(d)給出了((untime(P)‖pSΛ)/S)\ATypeH及untime(P)\ATypeH的束圖.不管P是否與Λ交互,低安全級用戶在概率配置下觀察到的視圖都如圖1(d)所示.例5.考慮進(jìn)程:P≡(l.(τ.0+qτ.νt(l).0)+pl.0)+rl.h.l.0).如圖2(a)所示,若進(jìn)程P和惡意進(jìn)程Λ=h*.0交互,低安全級用戶觀察到的視圖為((P‖pSΛ)/S)\ATypeH=(l.(τ.0+qτ.νt(l).0)+pl.0)+rl.τ.0)(如圖2(b)所示),若P不和進(jìn)程Λ交互,則低安全級用戶觀察到的視圖為P\ATypeH=l.(τ.0+qτ.νt(l).0)+pl.0(如圖2(c)所示),因此P?PTBNDC.如圖2所示,P與Λ交互時,低安全級用戶觀察到l.τ.0的概率為p×q×r+1-r,而P不與Λ交互時,低安全級用戶觀察到l.τ.0的概率為p×q×r.因此P通過控制與惡意進(jìn)程的交互向低安全級用戶泄露信息.如用((P‖pSΛ)/S)\ATypeH表示傳輸信息1,用P\ATypeH表示傳輸信息0,低安全級用戶通過觀察l.τ.0出現(xiàn)的頻率來獲得高安全級向低安全級用戶泄露的信息.而若不考慮概率信息,有:unprob(P)≡(l.(τ.0+τ.νt(l).0)+l.0)+l.h.l.0).文獻(xiàn)指出其滿足tBNDC屬性,即在不考慮概率的情況下,unprob(P)不存在隱蔽通道.以上2個例子說明,一個進(jìn)程與其他惡意進(jìn)程并發(fā)交互時,利用同步動作造成的死鎖或延時,讓低安全級的接收者感受到這種變化,即該進(jìn)程是否與其他特定的惡意進(jìn)程正在進(jìn)行并發(fā)同步,來獲得該進(jìn)程向低安全級用戶傳遞的隱含信息.BNDC,PBNDC,tBNDC屬性分別在非確定配置、概率配置、時間配置下討論了隱蔽傳輸?shù)姆绞?但是例4和例5分別指出了在滿足PBNDC,tBNDC屬性的情況下,若同時考慮概率和時間信息,可構(gòu)造出新的隱蔽通道,而這樣的隱蔽通道可以被PTBNDC屬性所捕獲.命題2.PTBNDC?tBNDC,PTBNDC?PBNDC.證明.由于P∈PTBNDC,有P/ATypeH≈PTB((P‖pSΛ)/S)\ATypeH,因此由定理1有unprob(P/ATypeH)≈TBunprob(((P‖pSΛ)/S)\ATypeH),易知:unprob(P/ATypeH)=unprob(P)/ATypeH;unprob(((P‖pSΛ)/S)\ATypeH)=unprob((P‖pSΛ)/S)\ATypeH=(unprob(P)‖pSunprob(Λ))/unprob(S)\ATypeH.因此可得:unprob(P)/ATypeH)≈(unprob(P)‖pSunprob(Λ))/unprob(S)\ATypeH.從而證得:unprob(P)∈tBNDC,因此PTBNDC?tBNDC.同理可證:unprob(P)∈BSPNI,得PTBNDC?PBNDC.證畢.命題3.PTBNDC?PTBSNI.證明.進(jìn)程P∈PTBNDC,因此有P\ATypeH≈PTB((P‖pSΛ)/S)\ATypeH,Λ∈ATypeH為另一個高安全級進(jìn)程.若Λ∈ATypeH為空進(jìn)程.則((P‖pSΛ)/S)\ATypeH≈PTBP/ATypeH.P\ATypeH≈PTBP/ATypeH,有P∈TBSPNI,所以有PTBNDC?PTBSNI成立.證畢.2.3spbtndc屬性由于在PTBNDC的定義中存在全稱量詞,對于判斷一個進(jìn)程不滿足PTBNDC屬性只需構(gòu)造一個Λ的反例,使得((P‖pSΛ)/S)\ATypeHue06dPTBP/ATypeH.但若驗證一個進(jìn)程滿足PTBNDC屬性卻需要對所有潛在進(jìn)程進(jìn)行考慮.這是非常困難的,因此為解決這個問題,基于文獻(xiàn)的思想,提出強(qiáng)概率時間互擬組合不可演繹屬性(strongprobabilistictimedbisimulationnondeducibilityoncomposition,SPTBNDC).該屬性將PTBNDC條件中?Λ∈ξH,限定在進(jìn)程P的后續(xù)可推導(dǎo)的進(jìn)程中.定義8.設(shè)P∈ξ,α∈ATypeH∪≥0,p∈則P∈SPTBNDC當(dāng)且僅當(dāng)ue02fP′∈Der(P),ue02fP″,P′α,→ue5c6pP″,有P′\ATypeH≈PTBP″\ATypeH,其中Der(P)表示進(jìn)程P的后續(xù)狀態(tài).在定義7中,為驗證進(jìn)程滿足PTBNDC屬性,須檢查所有的交互進(jìn)程Λ∈ξH,而定義8僅須檢查有限的進(jìn)程?P′∈Der(P)即可.低安全級用戶不能通過觀察到的系統(tǒng)行為,判斷高安全級動作在某個時間點(diǎn)執(zhí)行過.低安全級用戶觀察到的系統(tǒng)行為不受前一狀態(tài)高安全級動作的影響.命題4.若P∈SPTBNDC,?P′∈Der(P),P′是SPTBNDC的.證明.SPTBNDC屬性要求進(jìn)程在每個可達(dá)狀態(tài)都滿足PTBNDC.由于Ρ→α,pΡ′?Der(Ρ)?Der(Ρ′).所以易知P′∈STPBNDC.證畢.命題5.SPTBNDC?SPBNDC,SPTBNDC?TSBSBSNNI.證明.由于P∈SPTBNDC,則?P′∈Der(P),?P″,有P′/ATypeH≈PTBP″\ATypeH.易知untime(P′/ATypeH)≈PBuntime(P″\ATypeH).對?untime(P′)∈Der(untime(P)),?untime(P″),有untime(Ρ′)→α,puntime(Ρ″),其中α∈ATypeH,則untime(P′)/ATypeH≈PBuntime(P″\ATypeH,因此有untime(P)∈SPNBDC,得SPTBNDC?SPBNDC.同理可得SPTBNDC?TSBSNNI.證畢.由命題1～5,給出如下各屬性的包含關(guān)系圖,如圖3所示.在概率時間配置下,若進(jìn)程P∈PTSBNDC,則有P∈PTBNDC,P∈PTBSNI;若不考慮概率配置,則unprob(P)∈TSBSNNI,unprob(P)∈TSBSNNI;若不考慮時間配置,僅考慮概率配置,則untime(P)∈PBNDC,untime(P)∈BSPNI.3routing文獻(xiàn)使用OSI網(wǎng)絡(luò)層的消息接口處理器(interfacemessageprocessor,IMP)路由機(jī)制作為實(shí)例,利用概率進(jìn)程代數(shù)對其概率信息流安全性進(jìn)行了分析.文獻(xiàn)在文獻(xiàn)的基礎(chǔ)上研究了P_PBNDC等屬性,并利用概率進(jìn)程代數(shù)在該實(shí)例上分析了P_PBNDC,指出IMP不滿足P_PBNDC性.文獻(xiàn)在文獻(xiàn)的基礎(chǔ)上,提出了I_tBSNNI等屬性,也利用該實(shí)例對其提出的時間配置下的屬性進(jìn)行了分析,指出其方法能夠應(yīng)用在系統(tǒng)的非傳遞無干擾安全屬性分析中.IMP用于路由機(jī)制,負(fù)責(zé)在網(wǎng)絡(luò)層中基于包的目的地址來決定到達(dá)的包由哪條輸出鏈路進(jìn)行傳輸.由于篇幅原因,其原型詳細(xì)描述見文獻(xiàn).本文首先利用ptSPA對IMP在概率時間配置下進(jìn)行建模.IMP?(Arrivals‖p1SRouter‖p2Channels)\{idle}:Arrivals?Arrivala∥12Arrivalb;Channels?Channela‖vChannelb;Router?(Queues‖S1∪ISwitch‖IIdle;Idle?νΔt(idle.Idle);S1={accepta,acceptb};I={idle};Idle?νΔt(idle.Idle);Queues?(Queuea‖IQueueb);S2a?{senda,busya},S2b?{sendb,busyb};Arrivalx?νtxr(reveivex).Arrivalx+rxνtxw(waitx).Arrivalx+νtrb*(reveiveb*).Arrivalx′;Queuex?νtxr*(reveivex*).νtxa*(acceptx*).Queuex+νtxi*(idle*).Queuex;Managerx?νtxa(acceptx).Manager′x+νtxi(idle*).Managerx;M