應(yīng)用類通信安全模型的構(gòu)造與實現(xiàn)

應(yīng)用類通信安全模型的構(gòu)造與實現(xiàn)

1操作系統(tǒng)安全結(jié)構(gòu)框架操作系統(tǒng)是所有應(yīng)用程序正確操作的基礎(chǔ)。最初的操作系統(tǒng)主要面向編程用戶。隨著工程技術(shù)和網(wǎng)絡(luò)技術(shù)的發(fā)展，出現(xiàn)了大量面向公眾的應(yīng)用程序系統(tǒng)。由于應(yīng)用程序編輯對用戶的安全需求的不確定性，使應(yīng)用信息系統(tǒng)與操作系統(tǒng)安全分離。為了引導(dǎo)用戶，操作系統(tǒng)應(yīng)該積極為應(yīng)用程序提供有效的安全機制，這是必須解決的問題。為描述方便,將操作系統(tǒng)上運行的應(yīng)用系統(tǒng)抽象為應(yīng)用類.支持應(yīng)用類安全的操作系統(tǒng)安全結(jié)構(gòu)框架由安全通道和安全協(xié)調(diào)器組成.安全通道的主要目標是保證只有授權(quán)的用戶使用正確的應(yīng)用類對數(shù)據(jù)集合進行合法的操作.安全協(xié)調(diào)器的主要目標是保證應(yīng)用類接收或發(fā)送數(shù)據(jù)的保密性和完整性,使之符合整個系統(tǒng)的安全需求.在安全框架中,操作系統(tǒng)通過執(zhí)行為每個應(yīng)用類建立的安全策略,在用戶、應(yīng)用類以及數(shù)據(jù)集合間建立一條安全通道.在應(yīng)用類之間動態(tài)和靜態(tài)交互信息的情況下,通過實施應(yīng)用類通信安全模型協(xié)調(diào)應(yīng)用類之間的通信,保證應(yīng)用類通信的安全.2生成保護函數(shù)約定1.S是主體集合,O是客體集合,A是訪問方式集合,ST是可信主體集合,S′是不可信主體集合S′=S-ST,C為保密性等級集合,W為完整性等級集合,CW為安全等級集合,CW∶={(c,w)|c∈C,w∈W}.定義1.系統(tǒng)狀態(tài)v:集合V中元素,v∈V=(B×M×F×I×H).當前存取集B:B∈(S×O×A).訪問控制集合A:A={r,w,e,a}.其中,r表示可讀不可寫方式,a表示可寫不可讀方式,w表示可讀且可寫方式,e表示不可讀且不可寫(可執(zhí)行)方式.存取控制矩陣:M={M|M是矩陣∧M中元素Mij是主體Si對客體Oj的訪問權(quán)限集合}.保密級函數(shù)F:由3個分量組成,fs為主體最大保密級函數(shù),fs(s)∈C表示主體s的最大保密級;fc為主體當前保密級函數(shù),fc(s)∈C表示主體s當前的保密級;fo為客體保密級函數(shù),fo(o)∈C表示客體o的保密級.完整級函數(shù)I:由3個分量組成,is為主體最大完整級函數(shù);is(s)∈W表示主體s的最大完整級;ic為主體當前完整級函數(shù),ic(s)∈W表示主體s當前的完整級;io為客體完整級函數(shù),io(o)∈W表示客體o的完整級.定義2.完整性規(guī)則集合IVP:完整性規(guī)則ivp∈IVP是客體到{YES,NO}的映射,其中YES=1,NO=0.YES表示符合完整性規(guī)則,NO表示不符合完整性規(guī)則.函數(shù)k:k是IVP和CW間的映射.?ivp∈IVP,有且僅有惟一的k(ivp)∈CW.安全級cw∈CW對應(yīng)的完整性規(guī)則集合cwivp,cwivp={ivp|k(ivp)=cw,ivp(IVP}.定義3.安全代理集合DS:DS∶={DS|DS?S}.函數(shù)m:m是DS和CW間的一一映射.?ds∈DS,有且僅有惟一的k(ds)∈CW;?cw=(c,w)∈CW,有且僅有惟一的m-1(cw)∈DS.安全代理ds:安全級cw=(c,w)對應(yīng)的安全代理為ds:ds=m-1(cw)且fc(ds)=c,ic(ds)=w,fs(ds)=SESYSTEMHIGH,is(ds)=INSYSTEMHIGH.SESYSTEMHIGH:表示系統(tǒng)的最大保密安全級;INSYSTEMHIGH表示系統(tǒng)的最大完整安全級.約定2.rq(Si?Οj?xˉ)2.rq(Si?Oj?xˉ)表示主體Si對客體Oj的xˉ訪問請求.(1)系統(tǒng)狀態(tài)#-特性公理1(ss-特性).一系統(tǒng)狀態(tài)v=(b,M,f,i,H)滿足簡單安全性iff,對任意b=(s?o?xˉ)∈B:①xˉ=e或a,或②xˉ=r或w且fs(s)≥fo(o).公理2(*-特性).一系統(tǒng)狀態(tài)v=(b,M,f,i,H)對于主體集S′?S滿足*性iff,對任意b=(s?o?xˉ)∈B:①xˉ=a→fc(s)≤fo(o);②xˉ=w→fc(s)=fo(o);③xˉ=r→fc(s)≥fo(o).公理3(ds-特性).一系統(tǒng)狀態(tài)v=(b,M,f,i,H)滿足自主安全性iff,對每個b=(si?oj?xˉ)∈B?xˉ∈Μij.公理4(ac-特性)激活公理.物體可從死去物體中保存任何主體不能存取死亡客體,即對每個死亡對象o∈Ο?(s?o?xˉ)?B.新激活對象的重寫性一個新激活對象被賦予一個與其以前活動無關(guān)的初始狀態(tài).新激活對象的安全級別對于每個被主體s激活的客體o,fo(o)≥fc(s).對象刪除規(guī)則對于每個被主體s刪除的客體o,fc(s)≥fo(o).(2)相關(guān)規(guī)則公理5(ss-特性).一系統(tǒng)狀態(tài)v=(b,M,f,i,H)滿足簡單安全性iff,對任意b=(s?o?xˉ)∈B:①xˉ=r或e,或②xˉ=a或w且is(s)≥io(o).公理6(*-特性).一系統(tǒng)狀態(tài)v=(b,M,f,i,H)對于主體集S′?S滿足*性iff,對任意b=(s?o?xˉ)∈B:①xˉ=a→is(s)≥io(o);②xˉ=w→is(s)=io(o);③xˉ=r→is(s)≤io(o).公理7(ds-特性).一系統(tǒng)狀態(tài)v=(b,M,f,i,H)滿足自主安全性iff,對每個b=(si?oj?xˉ)∈B?xˉ∈Μij.公理8(ac-特性)激活公理.①主體對死亡客體可存取性:任何主體不能存取死亡客體,即對每個死亡對象o∈Ο?(s?o?xˉ)∈B.②新激活客體的重寫性:一個新激活對象被賦予一個與其以前活動無關(guān)的初始狀態(tài).③新激活客體的安全級:對于每個被主體s激活的客體o,io(o)≤ic(s).④客體刪除規(guī)則:對于每個被主體s刪除的客體o,ic(s)≤io(o).2.1模型的構(gòu)造方法規(guī)則1.對任意b=(s?o?xˉ)∈B:①xˉ=a→fc(s)≤fo(o),ic(s)≥io(o);或者fc(s)≤fo(o),ic(s)≤io(o)且滿足規(guī)則2;②xˉ=w→fc(s)=fo(o),ic(s)=io(o);或者fc(s)=fo(o),ic(s)≤io(o)且滿足規(guī)則2;或者fc(s)=fo(o),ic(s)≥io(o)且滿足規(guī)則3;③xˉ=r→fc(s)≥fo(o),ic(s)≤io(o);或者fc(s)≥fo(o),ic(s)≥io(o)且滿足規(guī)則3.規(guī)則2.在(b,M,f,i,H)狀態(tài),a∈Mij∈M,fc(Si)≤fo(Oj),ic(Si)≤io(Oj)時,對rq(Si,Oj,a)的處理.①Si激活客體O′j,O′j的安全級為cw1=(fo(O′j),io(O′j))且fo(O′j)=fc(Si),io(O′j)=ic(Si).對rq(Si,O′j,a)授權(quán),構(gòu)造b*1,使得b*1={(Si,O′j,a)}∪b,進入(b*1,M,f,i,H)狀態(tài).②安全級cw2=(fo(Oj),io(Oj))對應(yīng)的完整性規(guī)則集為cw2ivp.if?ivp(cw2ivp,ivp(O′j)=YESthen進入步驟③elseSi刪除客體O′j,拒絕rq(Si,Oj,a).③構(gòu)造i*,使得io(O′j)=io(Oj).④安全級cw2對應(yīng)的安全代理為S′i.⑤對rq(S′i,O′j,r)授權(quán),構(gòu)造b*2,使得b*2={(S′i,O′j,r)}∪b*1,進入(b*2,M,f,i*,H)狀態(tài).⑥對rq(S′i,Oj,a)授權(quán),構(gòu)造b*3,使得b*3={(S′i,Oj,a)}∪b*2,進入(b*3,M,f,i*,H)狀態(tài).⑦S′i刪除O′j.規(guī)則3.在(b,M,f,i,H)狀態(tài),r∈Mij∈M,fc(Si)≥fo(Oj),ic(Si)≥io(Oj)時,對rq(Si,Oj,r)的處理.①安全級cw1=(fo(Oj),io(Oj))對應(yīng)的安全代理為S′i.②對rq(S′i,Oj,r)授權(quán),構(gòu)造b*1,使得b*1={(S′i,Oj,r)}∪b,進入(b*1,M,f,i,H)狀態(tài).③S′i激活客體O′j,O′j的安全級為cw2=(fo(O′j),io(O′j)),fo(O′j)=fo(Oj),io(O′j)=io(Oj).對rq(S′i,O′j,a)授權(quán),構(gòu)造b*2,使得b*2={(S′i,O′j,a)}∪b*1,進入(b*2,M,f,i,H)狀態(tài).④安全級cw2=(fc(Si),ic(Si))對應(yīng)的完整性規(guī)則集為cw2ivp.(高保密、高完整性)if?ivp∈cw2ivp,ivp(O′j)=YESthen進入步驟⑤elseS′i刪除客體O′j,拒絕rq(Si,Oj,r).⑤構(gòu)造i*,使得io(O′j)=ic(Si).⑥對rq(Si,O′j,r)授權(quán),構(gòu)造b*3,使得b*3={(Si,O′j,r)}∪b*2,進入(b*3,M,f,i*,H)狀態(tài).⑦Si刪除客體O′j.2.2模型的推論和定理證明定理1.若狀態(tài)(b,M,f,i,H)滿足BLP公理,則由規(guī)則2得到的狀態(tài)(b*3,M,f,i*,H)滿足BLP公理.證明.①設(shè)(Sl?Οk?xˉ)∈b*1?ΙFSl=SiAΝDΟk=Ο′j,由規(guī)則2步驟①,則xˉ=a.ΙFSl≠SiΟRΟk≠Ο′j,則(Sl?Οk?xˉ)∈b.因此(b*1,M,f,i,H)滿足公理1.設(shè)(Sl?Οk?xˉ)∈b*2?ΙFSl=S′iAΝDΟk=Ο′j,由規(guī)則2步驟①,fo(O′j)=fc(Si),由定義5fs(S′i)=SESYSTEMHIGH,則fs(S′i)≥fo(O′j).IFSl≠S′iOROk≠O′j,則(Sl?Οk?xˉ)∈b*1.因此,(b*2,M,f,i*,H)滿足公理1.設(shè)(Sl?Οk?xˉ)∈b*3?ΙFSl=S′iAΝDΟk=Ο′j,由規(guī)則2的步驟⑥,則xˉ=a.ΙFSl≠S′iΟRΟk≠Οj,則(Sl?Οk?xˉ)∈b*2.因此,(b*3,M,f,i*,H)滿足公理1.②設(shè)(Sl?Οk?xˉ)∈b*1?ΙFSl=SiAΝDΟk=Ο′j,則由規(guī)則2的步驟①xˉ=a∈Μij=Μlk.ΙFSl≠SiΟRΟk≠Ο′j,則(Sl?Οk?xˉ)∈b?xˉ∈Μij.因此,(b*1,M,f,i,H)滿足公理3.設(shè)(Sl?Οk?xˉ)∈b*2?ΙFSl=S′iAΝDΟk=Ο′j,則由規(guī)則2的步驟⑤xˉ=r∈Μij=Μlk.ΙFSl≠S′iΟRΟk≠Ο′j,則(Sl?Οk?xˉ)∈b*1?xˉ∈Μij.因此,(b*2,M,f,i*,H)滿足公理3.設(shè)(Sl?Οk?xˉ)∈b*3?ΙFSl=S′iAΝDΟk=Οj,由規(guī)則2的步驟⑥則xˉ=a∈Μij=Μlk.ΙFSl≠S′iΟRΟk≠Οj,則(Sl?Οk?xˉ)∈b*2?x∈Μij.因此,(b*3,M,f,i*,H)滿足公理3.③1)設(shè)(Sl,Ok,a)∈b*1,IFSl=SiANDOk=O′j,由規(guī)則2的步驟①fo(O′j)=fc(Si).IFSl≠SiOROk≠O′j,則(Sl,Ok,a)∈b.因此,(b*1,M,f,i,H)滿足公理2①.設(shè)(Sl,Ok,a)∈b*2,由規(guī)則2的步驟⑤(Sl,Ok,a)∈b*1.因此,(b*2,M,f,i*,H)滿足公理2①.設(shè)(Sl,Ok,a)∈b*3,IFSl=S′iANDOk=Oj,由規(guī)則2的步驟②,fc(S′i)=fo(Oj).IFSl≠S′iOROk≠Oj,則(Sl,Ok,a)∈b*2.因此,(b*3,M,f,i*,H)滿足公理2①.2)設(shè)(Sl,Ok,w)∈b*1,則(Sl,Ok,w)∈b.同理設(shè)(Sl,Ok,w)∈b*2,(Sl,Ok,w)∈b*3,則(Sl,Ok,w)∈b.因此,(b*3,M,f,i*,H)滿足公理2②.3)設(shè)(Sl,Ok,r)∈b*1,則(Sl,Ok,r)∈b.因此,(b*1,M,f,i,H)滿足公理2③.設(shè)(Sl,Ok,r)∈b*2,IFSl=S′iANDOk=O′j,由規(guī)則2的步驟②,fc(S′i)=fo(Oj),由規(guī)則2的步驟①,fo(O′j)=fc(Si),由規(guī)則2的條件,fc(Si)≤fo(Oj),則fo(O′j)≤fc(S′i).IFSl≠S′iOROk≠O′j,則(Sl,Ok,r)∈b*1.因此,(b*2,M,f,i*,H)滿足公理2③.設(shè)(Sl,Ok,r)∈b*3,則(Sl,Ok,r)∈b*2.因此,(b*3,M,f,i*,H)滿足公理2③.④由規(guī)則2的步驟①,fo(O′j)=fc(Si),因此,Si激活O′j符合公理4③.由規(guī)則2的步驟②,fo(O′j)=fc(Si),因此,Si刪除客體O′j符合公理4④.由規(guī)則2的步驟⑦,fo(O′j)≤fc(S′i),因此,S′i刪除客體O′j符合公理4④.綜合①～④規(guī)則2得到的狀態(tài)(b*3,M,f,i*,H)滿足BLP公理.定理2.若狀態(tài)(b,M,f,i,H)滿足BLP公理,則由規(guī)則3得到的狀態(tài)(b*3,M,f,i*,H)滿足BLP公理.證明.與定理1類似,不再詳述.定理3.模型符合BLP模型.證明.規(guī)則1中保密性與公理2相同,且規(guī)則2和規(guī)則3滿足BLP公理,因此模型符合BLP模型.定理4.若狀態(tài)(b,M,f,i,H)滿足Biba公理,則由規(guī)則3得到的狀態(tài)(b*3,M,f,i*,H)滿足Biba公理.證明.①設(shè)(Sl?Οk?xˉ)∈b*1?ΙFSl=S′iAΝDΟk=Οj,由規(guī)則3的步驟②則xˉ=r.ΙFSl≠S′iΟRΟk≠Οj,則(Sl?Οk?xˉ)∈b.因此,(b*1,M,f,i,H)滿足公理5.設(shè)(Sl?Οk?xˉ)∈b*2?ΙFSl=S′iAΝDΟk=Ο′j,由規(guī)則3步驟③中io(O′j)=io(Oj),由定義5is(S′i)=INSYSTEMHIGH,所以is(S′i)≥io(O′j).IFSl≠S′iOROk≠O′j,則(Sl?Οk?xˉ)∈b*1.因此,(b*2,M,f,i*,H)滿足公理5.設(shè)(Sl?Οk?xˉ)∈b*3?ΙFSl=SiAΝDΟk=Ο′j,由規(guī)則3的步驟⑥則xˉ=r.ΙFSl≠SiΟRΟk≠Ο′j,則(Sl?Οk?xˉ)∈b*2.因此,(b*3,M,f,i*,H)滿足公理5.②設(shè)(Sl?Οk?xˉ)∈b*1?ΙFSl=S′iAΝDΟk=Οj,則由規(guī)則3的步驟②xˉ=r∈Μij=Μlk.ΙFSl≠S′iΟRΟk≠Οj,則(Sl?Οk?xˉ)∈b?x∈Μij.因此,(b*1,M,f,i,H)滿足公理7.設(shè)(Sl?Οk?xˉ)∈b*2?ΙFSl=S′iAΝDΟk=Ο′j,則由規(guī)則3的步驟③xˉ=a∈Μij=Μlk.ΙFSl≠S′iΟRΟk≠Ο′j,則(Sl,Ok,x)∈b*1,x∈Mij.因此(b*2,M,f,i*,H)滿足公理7.設(shè)(Sl,Ok,x)∈b*3,IFSl=SiANDOk=O′j,由規(guī)則3的步驟⑥,則xˉ=r∈Μij=Μlk.ΙFSl≠SiΟRΟk≠Ο′j,則(Sl,Ok,x)∈b*2,x∈Mij.因此,(b*3,M,f,i*,H)滿足公理7.③1)設(shè)(Sl,Ok,a)∈b*1,由規(guī)則3的步驟②(Sl,Ok,a)∈b.因此,(b*1,M,f,i,H)滿足公理6①.設(shè)(Sl,Ok,a)∈b*2,IFSl=S′iANDOk=O′j,由規(guī)則3的步驟①,ic(S′i)=io(Oj),由規(guī)則3的步驟③,io(O′j)=io(Oj),則ic(S′i)=io(O′j).IFSl≠S′iOROk≠O′j,則(Sl,Ok,a)∈b*1.因此,(b*2,M,f,i*,H)滿足公理6①.設(shè)(Sl,Ok,a)∈b*3,由規(guī)則3的步驟⑥,(Sl,Ok,a)∈b*2.因此,(b*3,M,f,i*,H)滿足公理6①.2)設(shè)(Sl,Ok,w)∈b*1,則(Sl,Ok,w)∈b.同理,設(shè)(Sl,Ok,w)∈b*2,(Sl,Ok,w)∈b*3,則(Sl,Ok,w)∈b.因此,(b*3,M,f,i*,H)滿足公理6②.3)設(shè)(Sl,Ok,r)∈b*1,若Si=S′i且Ok=Oj,由規(guī)則3的步驟①,ic(S′i)=io(Oj).IFSl=S′iANDOk=Oj,則(Sl,Ok,r)∈b.因此,(b*1,M,f,i,H)滿足公理6③.設(shè)(Sl,Ok,r)∈b*2,由規(guī)則3的步驟③,(Sl,Ok,r)∈b*1.因此,(b*2,M,f,i*,H)滿足公理6③.設(shè)(Sl,Ok,r)∈b*3,IFSl=SiANDOk=O′j,由規(guī)則3的步驟⑤,io(O′j)=ic(Si).IFSl≠SiOROk≠O′j,則(Sl,Ok,r)∈b*2.因此,(b*3,M,f,i*,H)滿足公理6③.④由規(guī)則3的步驟③,ic(S′i)=io(O′j)=io(Oj),因此,Si激活O′j符合公理8③.由規(guī)則3的步驟④,ic(S′i)=io(O′j)=io(Oj),因此,Si刪除客體O′j符合公理8④.由規(guī)則3的步驟⑤,⑦,io(O′j)=ic(Si),因此,S′i刪除客體O′j符合公理8④.綜合①～④,規(guī)則3得到的狀態(tài)(b*3,M,f,i*,H)滿足Biba公理.定理5.若狀態(tài)(b,M,f,i,H)滿足Biba公理,則由規(guī)則2得到的狀態(tài)(b*3,M,f,i*,H)滿足Biba公理.證明.與定理4類似,不再詳述.定理6.模型符合BiBa模型.證明.根據(jù)規(guī)則1①?xˉ=a→fc(s)≤fo(o)?ic(s)≥io(o)與公理6①相同;fc(s)≤fo(o),ic(s)≤io(o)且滿足規(guī)則2,規(guī)則2由定理5證明符合Biba公理.根據(jù)規(guī)則1②?xˉ=w→fc(s)=fo(o)?ic(s)=io(o)與公理6②相同;fc(s)=fo(o),ic(s)≤io(o)且滿足規(guī)則2,規(guī)則2由定理5證明符合Biba公理;fc(s)=fo(o),ic(s)≥io(o)且滿足規(guī)則3,規(guī)則3由定理4證明符合Biba公理.根據(jù)規(guī)則1③?xˉ=r→fc(s)≥fo(o)?ic(s)≤io(o)與公理6③相同;fc(s)≥fo(o),ic(s)≥io(o)且滿足規(guī)則3,規(guī)則3由定理4證明符合Biba公理.因此模型符合Biba模型.3模型實現(xiàn)與測試目前瀏覽器/服務(wù)器(B/S)應(yīng)用是軍隊電子辦公應(yīng)用的主要模式,B端和S端通過FTP協(xié)議實現(xiàn)文電的傳遞.B/S應(yīng)用模式可用生產(chǎn)者-消費者模型來表示.在用戶固定以及網(wǎng)絡(luò)邊界明確的文電傳輸應(yīng)用環(huán)境中,操作系統(tǒng)安全框架從控制信息發(fā)送的源頭-B端的安全來保證文電傳輸應(yīng)用的安全性.為實現(xiàn)支持文電傳輸應(yīng)用類安全的操作系統(tǒng)安全結(jié)構(gòu)框架,將運行在Linux上的瀏覽器Mozilla和服務(wù)器ProFTPD分別抽象為瀏覽器類(MC)和服務(wù)器類(PC).MC讀PC對應(yīng)FTP協(xié)議請求消息中的RETR操作,MC寫PC對應(yīng)FTP協(xié)議請求消息中的STOR操作.文電傳輸應(yīng)用類安全通信模型的實現(xiàn)由協(xié)議分析器、訪問控制器和完整性檢驗器組成.文電傳輸應(yīng)用中安全級別的標識由(保密性級別、完整性級別)組成,MC的安全級別由啟動瀏覽器用戶的安全級別決定.在文電傳輸應(yīng)用中,MC用戶既是信息的生產(chǎn)者又是信息的消費者,因此由MC產(chǎn)生信息的安全級別標識必須傳遞到PC,以便訪問控制器在MC消費信息時進行訪問控制.完整性規(guī)則檢驗器提供