張 帆 , 徐明迪 , 趙涵捷 , 張 聰 , 劉小麗 , 胡方寧

1(武漢輕工大學(xué) 數(shù)學(xué)與計(jì)算機(jī)學(xué)院,湖北 武漢 430023)

2(School of Electrical and Computer Engineering,Jacobs University,Bremen 28759,Germany)

3(武漢數(shù)字工程研究所,湖北 武漢 430205)

4(東華大學(xué) 電機(jī)系,臺(tái)灣 花蓮 08 153719)

5(宜蘭大學(xué) 資訊工程系,臺(tái)灣 宜蘭 02 415271)

6(暨南大學(xué) 信息科學(xué)技術(shù)學(xué)院,廣東 廣州 510632)

7(暨南大學(xué) 網(wǎng)絡(luò)空間安全學(xué)院,廣東 廣州 510632)

可信計(jì)算經(jīng)過長(zhǎng)期發(fā)展,取得了令人矚目的成果[1?24].隨著可信計(jì)算成為高價(jià)值體系結(jié)構(gòu)(如可信云等)的關(guān)鍵安全支撐技術(shù)之一,其自身安全性面臨著更高的挑戰(zhàn).在這些挑戰(zhàn)中,本文關(guān)注于如下3 個(gè)問題.

(1) 第1 個(gè)問題是:當(dāng)前可信計(jì)算缺少理論支撐,且理論研究與實(shí)踐應(yīng)用部分脫節(jié).

可信計(jì)算在誕生之初即面臨著“實(shí)踐超前于理論”的情況[1],經(jīng)過近20 年的發(fā)展,仍然沒有從數(shù)學(xué)上建立一個(gè)較為完善的可信計(jì)算模型.理論上,可信計(jì)算首先要明確定義“可信”.當(dāng)前主流的定義包括“完整性”[3]、“行為符合預(yù)期”[3]和“可靠+安全”[1]等幾種不同形式.已有的工作大多從單一的角度研究可信[4?24],而并沒有考慮建立一個(gè)統(tǒng)一的、涵蓋以上3 種不同定義的模型.另一方面,即便理論上取得了一些成果,這些成果也難以應(yīng)用到實(shí)踐當(dāng)中.以國內(nèi)廣受關(guān)注的無干擾模型在可信計(jì)算領(lǐng)域的研究為例[22?24],由于幾乎沒有工作解決無干擾屬性自動(dòng)化驗(yàn)證的難題[25?27],使得大多理論成果并不能實(shí)際應(yīng)用于實(shí)時(shí)信息系統(tǒng),如進(jìn)程信任鏈傳遞[22]、可信度量[23]等當(dāng)中.理論成果和實(shí)踐應(yīng)用之間仍然存在著較大差距.

(2) 第2 個(gè)問題是:當(dāng)前的可信度量屬于“被動(dòng)發(fā)現(xiàn)”機(jī)制,缺少“主動(dòng)防御”能力.

根據(jù)可信計(jì)算標(biāo)準(zhǔn),可信計(jì)算有三大核心功能:度量、存儲(chǔ)和報(bào)告,三者協(xié)同運(yùn)作確保了第三方能夠可靠地判定本機(jī)的可信性.其基本過程是:本機(jī)在運(yùn)行的過程中不斷度量自身的可信性,并將度量結(jié)果存儲(chǔ)到專用安全芯片TPM(trusted platform module)和內(nèi)存log 當(dāng)中.當(dāng)其他機(jī)器想與本機(jī)通信時(shí),由本機(jī)將存儲(chǔ)的度量結(jié)果報(bào)告給對(duì)方,并由對(duì)方來判定本機(jī)的可信性.上述過程是一種“事后被動(dòng)發(fā)現(xiàn)”機(jī)制,換句話說,這種機(jī)制只能確保其他機(jī)器可靠地判定本機(jī)是否被攻擊而處于不可信狀態(tài),但卻無法及時(shí)檢測(cè)到機(jī)器被攻擊的情況.事實(shí)上,“事前防御、事中審計(jì)、事后發(fā)現(xiàn)”應(yīng)當(dāng)作為環(huán)環(huán)相扣的整體.然而,現(xiàn)有的可信度量側(cè)重于“事后被動(dòng)發(fā)現(xiàn)”、而缺少“事前主動(dòng)防御”的研究工作.

(3) 第3 個(gè)問題是:可信計(jì)算如何在層出不窮的攻擊手段下可靠地實(shí)現(xiàn)可信度量.

可信計(jì)算“度量、存儲(chǔ)和報(bào)告”三大核心功能中,度量居于基礎(chǔ)地位,存儲(chǔ)和報(bào)告的內(nèi)容均來自于度量的結(jié)果.隨著新型攻擊方法(如ROP[28]等)層出不窮、傳統(tǒng)攻擊不斷應(yīng)用包括多態(tài)/混淆/變形/編碼等在內(nèi)的多種對(duì)抗手段以及未公開攻擊機(jī)理的威脅等,使得度量信息系統(tǒng)的可信性變得日益復(fù)雜和困難.特別地,運(yùn)行時(shí)(runtime)度量才能真正反映系統(tǒng)行為的可信性[1],但這對(duì)度量的實(shí)時(shí)性提出了很高的要求.

針對(duì)上述問題,本文提出了一種基于無干擾理論的軟件實(shí)時(shí)可信度量與防護(hù)方法,主要貢獻(xiàn)如下:

(1) 針對(duì)問題(1)和問題(2),首先,利用無干擾模型解釋了主流可信定義——即“完整性”“行為符合預(yù)期”和“可靠+安全”——的數(shù)學(xué)涵義(參見第2.2 節(jié)的定義9);其次,通過將系統(tǒng)調(diào)用看做原子動(dòng)作,提出了基于無干擾的實(shí)時(shí)可信度量與防護(hù)方法,其基本思想是:根據(jù)不同系統(tǒng)調(diào)用所屬安全域之間的無干擾關(guān)系,建立軟件預(yù)期行為EB(expected behavior),并利用無干擾模型判定軟件真實(shí)行為與預(yù)期行為之間的一致性,從而實(shí)現(xiàn)對(duì)軟件的實(shí)時(shí)可信度量與主動(dòng)防護(hù)(參見第3 節(jié));最后,給出了實(shí)時(shí)可信性判定算法(參見第3.5 節(jié)的算法1),算法的時(shí)間復(fù)雜性為O(1).

(2) 針對(duì)問題3,本文基于如下觀察:絕大多數(shù)攻擊都需要前后相繼的兩個(gè)步驟,即首先定位可利用的漏洞,然后通過漏洞執(zhí)行攻擊代碼(shellcode).打斷以上環(huán)環(huán)相扣的任何一步,就可以有效地防御攻擊.本文從第2 步入手,注意到攻擊代碼幾乎都需要系統(tǒng)調(diào)用的支持,因而不論是何種類型的攻擊,我們只需要利用系統(tǒng)調(diào)用序列構(gòu)建代碼的真實(shí)行為,利用系統(tǒng)調(diào)用安全域之間的無干擾關(guān)系刻畫軟件的預(yù)期行為EB,即可以通過判定當(dāng)前代碼的真實(shí)行為與預(yù)期行為EB 之間是否存在偏差來度量是否發(fā)生了攻擊.實(shí)驗(yàn)結(jié)果表明:方法是有效的,其不僅能夠?qū)崟r(shí)度量到新型攻擊如ROP 等,而且可以有效地發(fā)現(xiàn)多態(tài)、混淆、變形和編碼等多種傳統(tǒng)對(duì)抗方法所生成的攻擊代碼,理論上也可以防御未知機(jī)理攻擊(只要其利用系統(tǒng)調(diào)用實(shí)現(xiàn)攻擊).

(3) 所提出的方法無需任何學(xué)習(xí)訓(xùn)練過程,無需任何先驗(yàn)知識(shí).使用者亦不必關(guān)心底層理論機(jī)制,只要給出安全策略即可,具體來說,只需要根據(jù)實(shí)際安全需求,依照預(yù)期行為規(guī)范EBS(expected behavior specification)語法編寫EBS(參見第3.3 節(jié)和附錄),系統(tǒng)即可實(shí)現(xiàn)實(shí)時(shí)可信度量與防護(hù).

1 相關(guān)研究工作

1.1 可信度量相關(guān)研究工作

國際上第一個(gè)基于TCG(trusted computing group)標(biāo)準(zhǔn)的完整性度量架構(gòu)是IMA[4].IMA 是一種“加載時(shí)度量”,這種度量方式只能說明軟件沒有被篡改(哈希不變),并不能說明軟件運(yùn)行時(shí)的動(dòng)態(tài)行為是否可信.隨后,卡內(nèi)基梅隆大學(xué)的Shi 等人提出了為分布式系統(tǒng)建立可信環(huán)境的BIND 框架[5].BIND 把完整性度量對(duì)象的范圍縮小到關(guān)鍵代碼段,并對(duì)關(guān)鍵代碼段的每一組數(shù)據(jù)生成一個(gè)認(rèn)證器,實(shí)現(xiàn)了細(xì)粒度的動(dòng)態(tài)度量驗(yàn)證.但BIND 需要事先確定關(guān)鍵代碼段,并建立關(guān)鍵代碼段和輸入數(shù)據(jù)/輸出數(shù)據(jù)之間的綁定關(guān)系.這種綁定與本文是有差別的:本文對(duì)進(jìn)程所綁定的是基于系統(tǒng)調(diào)用描述的預(yù)期行為EB,同時(shí),綁定過程也無需確定關(guān)鍵代碼段.在IMA 的基礎(chǔ)上,Jaeger 等人通過引入CW-Lite 模型設(shè)計(jì)了PRIMA 架構(gòu)[6],實(shí)現(xiàn)了運(yùn)行時(shí)度量.但PRIMA 所基于的CWLite 模型缺少形式化驗(yàn)證能力,因而無法形式化地對(duì)系統(tǒng)設(shè)計(jì)進(jìn)行可信驗(yàn)證.從內(nèi)核完整的角度,Loscocco 等人[7]提出了Linux 內(nèi)核完整性監(jiān)視器LKIM,用以監(jiān)控Linux 內(nèi)核運(yùn)行時(shí)關(guān)鍵數(shù)據(jù)結(jié)構(gòu)的動(dòng)態(tài)完整性;Carbone等人[8]實(shí)現(xiàn)了KOP 系統(tǒng),用以監(jiān)控內(nèi)核指針對(duì)象的動(dòng)態(tài)完整性.LKIM 和KOP 的貢獻(xiàn)在于它們對(duì)于可信計(jì)算平臺(tái)的關(guān)鍵基礎(chǔ)軟件(操作系統(tǒng))的動(dòng)態(tài)完整性度量具有重要的意義,不足之處在于它們無法擴(kuò)展到一般應(yīng)用程序.針對(duì)云計(jì)算環(huán)境下的動(dòng)態(tài)完整性度量問題,Schiffman 等人[9]實(shí)現(xiàn)了VMV(virtual machine verifier).VMV 能夠?qū)μ摂M機(jī)及其內(nèi)部的應(yīng)用程序進(jìn)行動(dòng)態(tài)完整性度量,以確保云端計(jì)算的可信性.不過,VMV 構(gòu)建的基礎(chǔ)仍然是PRIMA[6],從而缺少形式化驗(yàn)證能力.從軟件運(yùn)行時(shí)的局部結(jié)構(gòu)化約束完整性和全局不變式完整性入手,Kil 等人[10]提出了一種基于完整性動(dòng)態(tài)屬性的遠(yuǎn)程證明系統(tǒng)ReDAS.ReDAS 需要一個(gè)學(xué)習(xí)訓(xùn)練過程,這使得它只能局限于度量經(jīng)過訓(xùn)練的軟件.Xu 等人[11]通過將系統(tǒng)的可信性歸結(jié)為系統(tǒng)狀態(tài)變化的可信性,提出了一個(gè)遠(yuǎn)程證明框架DR@FT.但DR@FT 只能適用于基于Clark-Wilson 或CW-Lite 模型的完整性度量框架,因而也無法驗(yàn)證自身設(shè)計(jì)架構(gòu)的可信性.John 等人[12]發(fā)現(xiàn):在Dell Latitude E6400 Laptop 上,可信度量根核CRTM(core root of trust measurement)的實(shí)現(xiàn)沒有滿足TPM PC 規(guī)范和NIST 800-155 指導(dǎo)規(guī)范,這使得攻擊者可以回放偽造的度量結(jié)果給TPM,從而導(dǎo)致證明方錯(cuò)誤地認(rèn)為本機(jī)被攻擊過的BIOS 仍然處于“干凈可信”的狀態(tài).該方法側(cè)重于解決CRTM 和信任鏈傳遞的安全性問題,而并非針對(duì)軟件行為的實(shí)時(shí)度量.針對(duì)動(dòng)態(tài)度量時(shí)動(dòng)態(tài)可信度量根DRTM(dynamic root of trust for measurement)的存在性(activated/enabled)攻擊問題,Zhang 等人[13]提出了一種強(qiáng)制性、最小化、用戶參與的解決方案.但該方案只確保DRTM 確實(shí)存在(activated),同樣不涉及軟件行為的實(shí)時(shí)度量.Abera 等人[14]設(shè)計(jì)并實(shí)現(xiàn)了控制流證明C-FLAT(control flow attestation)架構(gòu),通過軟件的控制流路徑,而不是源碼,來證明軟件的可信性,嘗試為物聯(lián)網(wǎng)設(shè)備上的遠(yuǎn)程證明提供一種解決方案.針對(duì)越來越深入的硬件可信度量和防護(hù)方法,Zhang 等人[15]提出了一種化整為零的攻擊技術(shù),以繞過現(xiàn)有的硬件檢查措施,其基本思想是:將整體的、惡意的硬件功能分解成零散的、正常的子模塊,在子模塊通過可信驗(yàn)證之后再將其組合成整體,以實(shí)現(xiàn)惡意硬件功能.由于硬件層位于系統(tǒng)調(diào)用層之下,因而本文無法對(duì)這種攻擊進(jìn)行檢測(cè)和防御.Matetic 等人[16]提出了一種稱為ROTE 的分布式回滾保護(hù)機(jī)制,攻擊者若要利用惡意回歸攻擊破壞Intel SGX 等安全機(jī)制下的信息完整性,就必須將ROTE 分布式平臺(tái)中的所有參與者同時(shí)回滾到初始狀態(tài),這大大增加了攻擊的難度.

國內(nèi)對(duì)于可信度量相關(guān)問題也展開了深入的研究.為了解決可信平臺(tái)模塊TPM 在云計(jì)算、網(wǎng)絡(luò)功能虛擬化等場(chǎng)景下低成本可信擴(kuò)展和前向安全問題,余發(fā)江等人[17]提出了一種動(dòng)態(tài)信任擴(kuò)展方法,有效保證了虛擬可信平臺(tái)模塊vTPM 的可信性,為虛擬環(huán)境下的度量、存儲(chǔ)、報(bào)告、密碼、證書等功能構(gòu)建了可靠的硬件基礎(chǔ).鄧良等人[18,19]用ring 0 層的內(nèi)可信基(inner TCB)替代傳統(tǒng)的虛擬機(jī)監(jiān)視器,實(shí)現(xiàn)對(duì)內(nèi)核代碼和控制流的完整性度量以及對(duì)硬件操作和軟件行為的驗(yàn)證,有效保證了上層應(yīng)用的安全,且開銷很小.林杰等人[20]針對(duì)虛擬機(jī)軟件的完整性問題,提出了一種利用關(guān)鍵數(shù)據(jù)結(jié)構(gòu)內(nèi)存映射和地址動(dòng)態(tài)轉(zhuǎn)換技術(shù),實(shí)現(xiàn)對(duì)上層應(yīng)用運(yùn)行時(shí)完整性度量的方法.與本文工作相比,上述完整性度量方法[18?20]的共有問題在于其無法回答軟件(即便代碼和數(shù)據(jù)被度量是完整的)在運(yùn)行過程中是否會(huì)出現(xiàn)不可信的行為.陳志鋒等人[21]基于內(nèi)存取證技術(shù)提出了一種內(nèi)核實(shí)時(shí)完整性度量方法.與本文相比,本文針對(duì)上層軟件,陳志鋒等人[21]針對(duì)的內(nèi)核,兩者的研究對(duì)象并不一致.另一方面,若將文獻(xiàn)[21]的技術(shù)應(yīng)用于上層應(yīng)用,其需要“完整性基準(zhǔn)庫”,換句話說,文獻(xiàn)[21]需要一個(gè)學(xué)習(xí)訓(xùn)練的過程,對(duì)于未經(jīng)學(xué)習(xí)的軟件可能無法準(zhǔn)確實(shí)施度量.相反,本文的方法無需學(xué)習(xí)訓(xùn)練,只要編寫好軟件預(yù)期行為規(guī)范,即可以度量任何軟件的實(shí)時(shí)行為.理論上,甚至還可以發(fā)現(xiàn)未知攻擊.張興等人[22,23]利用無干擾模型,對(duì)信任鏈傳遞[22]以及進(jìn)程[23]的可信性度量問題進(jìn)行了研究.他們工作的重要性在于首次將無干擾模型應(yīng)用于可信計(jì)算領(lǐng)域,但不足之處是沒有給出可實(shí)踐的方法,而如何將無干擾模型應(yīng)用于實(shí)踐,一直是無干擾研究的一個(gè)關(guān)鍵所在.

1.2 無干擾及其應(yīng)用相關(guān)研究工作

Goguen 等人[29]以狀態(tài)機(jī)的形式首先引入了傳遞無干擾的概念,隨后,Rushby 建立了標(biāo)準(zhǔn)的非傳遞無干擾模型[25].Rushby 的研究表明,傳遞無干擾只是非傳遞無干擾的一個(gè)特例.因此,如果沒有特殊說明,“無干擾”一般都特指“非傳遞無干擾”.在Rushby 的模型中,僅僅考慮了觀察者是否能夠區(qū)分狀態(tài)變遷所導(dǎo)致的狀態(tài)差異,而并不關(guān)心觀察者是否能夠同時(shí)觀察到所執(zhí)行的不同動(dòng)作的差異.Meyden 注意到了這個(gè)問題,由此定義了安全約束更強(qiáng)的TA-Security 和TO-Security[30].隨后,Eggert 等人研究了經(jīng)典的傳遞無干擾和非傳遞無干擾以及TA-Security 和TO-Security 這4 種無干擾屬性驗(yàn)證的時(shí)間和空間復(fù)雜度[26].需要指出的是,Eggert 等人僅僅給出了時(shí)空復(fù)雜度推演結(jié)果,但沒有給出具體的屬性驗(yàn)證算法.事實(shí)上,到目前為止,狀態(tài)機(jī)形式的無干擾模型屬性驗(yàn)證仍然是一個(gè)難題[25?27],當(dāng)前最好的工作是Hadj-Alouane 等人給出的驗(yàn)證算法[27],其不僅支持任意多個(gè)安全域,而且支持無干擾屬性的可靠性和完備性條件,然而其時(shí)間復(fù)雜性卻高達(dá)雙指數(shù),無法實(shí)用.

除了狀態(tài)機(jī)以外,進(jìn)程代數(shù)的互模擬特性使得它成為描述無干擾的另一個(gè)有力工具[31,32].特別地,利用進(jìn)程代數(shù)的驗(yàn)證工具,可以很容易地對(duì)基于進(jìn)程代數(shù)描述的無干擾屬性進(jìn)行驗(yàn)證.然而需要指出的是,3 種不同的無干擾模型,即Rushby 建立的無干擾模型[25]、Meyden 和Eggert 等人建立的無干擾模型[26,30]以及Ryan 和Focardi等人建立的無干擾模型[31,32],三者之間兩兩語義不等價(jià).這意味著基于進(jìn)程代數(shù)[31,32]的無干擾屬性驗(yàn)證算法和工具對(duì)于狀態(tài)機(jī)形式[25,26,30]的無干擾屬性驗(yàn)證并無任何幫助.

在國內(nèi),無干擾模型在可信計(jì)算領(lǐng)域受到了廣泛關(guān)注,應(yīng)用在包括可信測(cè)評(píng)[33]、信任鏈可信[22,34]、進(jìn)程可信[23]和終端隔離[24]等在內(nèi)的眾多領(lǐng)域.但是如前所述,由于沒有有效的無干擾屬性驗(yàn)證算法,上述工作中采用狀態(tài)機(jī)作為工具的工作幾乎都只能停留在理論分析層面而難以實(shí)用[22?24].為了解決可實(shí)踐的驗(yàn)證問題,當(dāng)前國際上的主流方法[35,36]是基于Rushby 的展開定理(unwinding theorem)[25],利用公理語義,結(jié)合定理證明器進(jìn)行屬性驗(yàn)證.但定理證明器的證明時(shí)間相對(duì)于實(shí)時(shí)要求而言并不可控,并且有可能無法給出證明,因而這類方法也無法應(yīng)用在實(shí)時(shí)可信防護(hù)領(lǐng)域.

1.3 基于系統(tǒng)調(diào)用的安全防護(hù)

系統(tǒng)調(diào)用在檢測(cè)異常行為方面具有較好的特異性,早期的系統(tǒng)調(diào)用主要應(yīng)用在入侵檢測(cè)領(lǐng)域,研究人員通過考察系統(tǒng)調(diào)用序列切片(不考慮參數(shù))或者系統(tǒng)調(diào)用參數(shù)集合關(guān)系(不考慮系統(tǒng)調(diào)用自身)與預(yù)期標(biāo)準(zhǔn)的差異來判定一個(gè)進(jìn)程是否被入侵,代表性方法如文獻(xiàn)[37]等.這類方法在早期開啟了系統(tǒng)調(diào)用在入侵檢測(cè)領(lǐng)域的新應(yīng)用,但這些方法大多只考慮了系統(tǒng)調(diào)用的語法特征,而并未考慮其語義規(guī)律,因而有較大的局限性.之后,研究人員嘗試綜合考慮系統(tǒng)調(diào)用或者API 的語法和語義,以圖、狀態(tài)機(jī)、馬爾科夫鏈、機(jī)器學(xué)習(xí)等作為工具對(duì)進(jìn)程行為進(jìn)行研究,取得了較為豐碩的成果[38?43].現(xiàn)階段,采用系統(tǒng)調(diào)用方法的研究困難和熱點(diǎn)在于,底層系統(tǒng)調(diào)用與上層應(yīng)用之間存在著語義斷層(semantic gap),僅僅從系統(tǒng)調(diào)用本身無法與上層應(yīng)用行為之間建立映射,從而必須具體問題具體分析,尚沒有一種較為通用的方法或者框架解決這個(gè)問題[38,41].

系統(tǒng)調(diào)用與無干擾模型的結(jié)合很少見,主流工作中相近的是Calvin 等人[44]基于無干擾實(shí)時(shí)檢測(cè)和防御TOCTTOU(time-of-check-to-time-of-use)競(jìng)爭(zhēng)條件攻擊,其核心思想在于構(gòu)建語義等價(jià)、但執(zhí)行順序不同的系統(tǒng)調(diào)用序列以消除競(jìng)爭(zhēng)條件.多數(shù)情況下,這種構(gòu)建是困難的,文獻(xiàn)[44]也未提及構(gòu)建方法(算法),因此,我們認(rèn)為更多的是理論意義[44].不同于文獻(xiàn)[44],由于前期我們找到了無干擾屬性基于狀態(tài)等價(jià)的充要條件[45],因而為系統(tǒng)調(diào)用與無干擾模型相結(jié)合、對(duì)軟件行為進(jìn)行實(shí)時(shí)無干擾屬性驗(yàn)證探索了一條可能的道路.

1.4 攜帶證明的代碼

攜帶證明的代碼PCC(proof carrying code)亦可以對(duì)代碼可信性進(jìn)行驗(yàn)證.PCC 框架[46]由代碼提供者CP(code producer)和代碼使用者CC(code consumer)兩部分構(gòu)成.其中,CP 必須為其提供的代碼提供一個(gè)安全證明(safety proof),該安全證明實(shí)質(zhì)上是CP 對(duì)CC 所規(guī)定的安全策略(safety policy)的形式化描述.CC 在運(yùn)行CP 所提供的代碼之前,會(huì)先用證明驗(yàn)證器對(duì)CP 提供的安全證明進(jìn)行驗(yàn)證:如果驗(yàn)證通過,則說明安全策略得到了遵守,從而CP 所提供的代碼是可信的,可以安全地在CC 上執(zhí)行;否則,代碼不可信,CC 拒絕代碼的執(zhí)行.

PCC 為代碼的可信執(zhí)行建立堅(jiān)實(shí)理論基礎(chǔ),但應(yīng)用到實(shí)時(shí)可信度量領(lǐng)域還存在如下難點(diǎn)需要解決.

(1) PCC 破壞了已部署代碼的兼容性.PCC 框架中,CP 在根據(jù)安全策略編寫了形式化規(guī)范之后,需要將原應(yīng)用和形式化規(guī)范一起重新打包編譯生成新的、包含形式化規(guī)范的二進(jìn)制代碼[47],我們稱其為PCC風(fēng)格的二進(jìn)制代碼.顯然,若采用PCC 架構(gòu)進(jìn)行軟件實(shí)時(shí)可信度量,則度量平臺(tái)上所有的應(yīng)用(即代碼)都必須重新編譯以形成PCC 風(fēng)格的二進(jìn)制代碼,否則,應(yīng)用無法通過平臺(tái)驗(yàn)證,進(jìn)而無法運(yùn)行.這意味著如果采用PCC 架構(gòu),則必然會(huì)破壞已部署應(yīng)用的兼容性.

(2) PCC 安全策略編寫代價(jià)較大.由于不同應(yīng)用所使用的編程語言以及語言的安全特性等存在差異,使得難以構(gòu)造一個(gè)統(tǒng)一、標(biāo)準(zhǔn)的形式化規(guī)范.換句話說,每一個(gè)應(yīng)用的CP 都需要單獨(dú)提供其應(yīng)用所對(duì)應(yīng)的形式化規(guī)范.當(dāng)安全策略發(fā)生變化,例如當(dāng)發(fā)生網(wǎng)絡(luò)安全事件進(jìn)行應(yīng)急響應(yīng)時(shí),每個(gè)應(yīng)用的形式化規(guī)范必須要對(duì)應(yīng)更新,并重新編譯生成新的PCC 代碼.這大大增加了安全策略規(guī)范編寫、維護(hù)和更新的代價(jià).

與PCC 相反,本文的方法不存在上述問題:(1) 從兼容性的角度,由于本文的方法不需要代碼自身攜帶安全證明,因而無需對(duì)應(yīng)用做任何改動(dòng),從而對(duì)已部署應(yīng)用的兼容性沒有任何影響;(2) 從安全策略規(guī)范角度,本文的方法以所有應(yīng)用所共用的系統(tǒng)調(diào)用為對(duì)象來構(gòu)造安全策略.通用情況下,使用者可以基于系統(tǒng)調(diào)用建立適用于所有應(yīng)用的統(tǒng)一、標(biāo)準(zhǔn)的安全策略規(guī)范;在此基礎(chǔ)上,對(duì)于特定應(yīng)用的特定需求,亦可以建立與其一一對(duì)應(yīng)的特殊的安全策略規(guī)范.當(dāng)安全策略發(fā)生變化時(shí)(如前述網(wǎng)絡(luò)安全事件應(yīng)急響應(yīng)時(shí)),只需要更新適用于所有應(yīng)用的統(tǒng)一、標(biāo)準(zhǔn)的安全策略規(guī)范即可.與PCC 相比,本文的方法大大減小了安全策略規(guī)范編寫、維護(hù)和更新的代價(jià).然而,PCC 方法也有其優(yōu)勢(shì),例如PCC 的度量粒度可以更細(xì),且已發(fā)展出堅(jiān)實(shí)的理論基礎(chǔ)和較多的工具,如何嘗試解決PCC 的前述兩大難題,以結(jié)合PCC 和本文的方法進(jìn)一步提升本文方法的理論基礎(chǔ)和可實(shí)踐性,是一個(gè)值得研究的工作,但這超出了本文的研究范圍.

2 理論基礎(chǔ)

2.1 無干擾模型定義

無干擾的思想最早由Goguen 和Meseguer[29]提出,其基本思想是:一組用戶GA,使用一組命令集合C操作之后,如果對(duì)另一組用戶GB所能觀察到的結(jié)果沒有影響,則稱用戶組GA對(duì)用戶組GB是無干擾的.既然GB無法感知GA的操作,那么也就無法從GA的操作中逆推出任何信息,從而也就防止了GA和GB之間的隱通道信息流傳輸.文獻(xiàn)[29]解決了困擾BLP 的隱通道問題,但只能處理傳遞信息流,對(duì)于非傳遞信息流是無法處理的.例如,不失一般性,假設(shè)某個(gè)涉密系統(tǒng)中劃分有文件域uf、加密機(jī)域ue和網(wǎng)絡(luò)域un這3 個(gè)安全域.如果我們用和分別表示允許和不允許信息在安全域之間的流動(dòng),則此涉密系統(tǒng)中機(jī)密文件的傳輸方式可以表示為其含義是:機(jī)密信息不能直接傳輸?shù)骄W(wǎng)絡(luò),而必須首先流經(jīng)加密機(jī)加密、再由加密機(jī)將加密后的密文發(fā)送到網(wǎng)絡(luò)進(jìn)行傳輸.換句話說,uf只能通過加密機(jī)中介ue間接地將信息傳遞到un.直覺地,對(duì)于這種信息流非直接(間接)流動(dòng)的情形,我們稱其為非傳遞信息流,文獻(xiàn)[29]無法對(duì)其進(jìn)行處理

隨后,眾多研究人員對(duì)非傳遞信息流情況下的無干擾模型進(jìn)行了深入研究,但是直到Rushby 才首次提出完全正確的非傳遞無干擾模型[25].由于傳遞無干擾只是非傳遞無干擾的一個(gè)特例[25],因而本文中我們以一般性的非傳遞無干擾模型為基礎(chǔ),研究如何構(gòu)建可實(shí)踐的軟件實(shí)時(shí)度量和防護(hù)方法.以下若沒有特殊說明,則文中的無干擾模型均特指非傳遞無干擾模型,且文中所有的定義均特指在非傳遞安全策略前提下.

定義1.無干擾模型定義.一個(gè)系統(tǒng)M可以用一個(gè)狀態(tài)機(jī)表示,其包含如下元素.

(1) 狀態(tài)機(jī)S,其中包含一個(gè)唯一的初始狀態(tài)s0.

(2) 一個(gè)原子動(dòng)作集A,其中包含了所有的原子動(dòng)作.

(3) 一個(gè)行為集B,其中包含了所有由原子動(dòng)作的連接所構(gòu)成的行為.如果用。表示原子動(dòng)作的連接,則一個(gè)行為的示例是α=a0。a1?！?。an,其中,ai(0≤i≤n)∈A.

(4) 一個(gè)輸出集O,其中包含了所有利用原子動(dòng)作所觀察到的輸出結(jié)果.

(5) 一個(gè)安全域集D,其中包含了系統(tǒng)中所有的安全域.

(6) 干擾關(guān)系?和無干擾關(guān)系/?,分別表示信息授權(quán)/禁止在兩個(gè)安全域之間流動(dòng),兩者互為補(bǔ)集.

(7) 動(dòng)作-安全域映射函數(shù)dom:A→D.返回每一個(gè)原子動(dòng)作a∈A所屬的安全域dom(a).

(8) 單步狀態(tài)變遷函數(shù):step:S×A→S,描述了系統(tǒng)M的單步狀態(tài)變遷.

(9) 多步狀態(tài)變遷函數(shù):multisteps:S×B→S.如果用Λ表示空動(dòng)作,則multisteps可以右遞歸表示為

其描述了系統(tǒng)M從狀態(tài)s∈S執(zhí)行行為(即多個(gè)原子動(dòng)作序列)α=a0?！m∈β之后所到達(dá)的新狀態(tài).

(10) 行為結(jié)果函數(shù)(behavior consequence):behcon:S×A→O,給出了系統(tǒng)M在某個(gè)狀態(tài)s∈S,外界利用動(dòng)作a∈A所能觀察到的結(jié)果o∈O.

約定使用…,s,t,…表示系統(tǒng)狀態(tài),約定使用α,β,…表示行為(原子動(dòng)作序列),使用u,v,…表示安全域.

定義2.結(jié)構(gòu)化機(jī)器M.結(jié)構(gòu)化機(jī)器M包含如下部分.

(1) 存儲(chǔ)單元集N.機(jī)器的每一個(gè)存儲(chǔ)單元都有一個(gè)獨(dú)一無二的名字,所有這些名字的集合構(gòu)成存儲(chǔ)單元集N,又叫名字集N.存儲(chǔ)單元包含寄存器單元、內(nèi)存單元、外存單元、緩存等.

(2) 值集V.當(dāng)狀態(tài)一定的時(shí)候,每一個(gè)存儲(chǔ)單元都有一個(gè)具體的值v.所有存儲(chǔ)單元值的集合構(gòu)成值集V.

(3) 內(nèi)容函數(shù)contents:S×N→V.內(nèi)容函數(shù)返回在狀態(tài)s∈S,名字n∈N的值v∈V.

(4) 觀察函數(shù)observe:D→P(N).觀察函數(shù)給出安全域u∈D所能觀察的名字集合.這里,P是冪集計(jì)算.

(5) 修改函數(shù)alter:D→P(N).修改函數(shù)給出安全域u∈D所能修改的名字集合.這里,P是冪集計(jì)算.

定義1 中的原子動(dòng)作粒度可大可小,可以是輸入(input)、函數(shù)調(diào)用(API 或者syscall)、命令(command)或者機(jī)器指令(instruction)等[25].當(dāng)執(zhí)行原子動(dòng)作之后,機(jī)器從一個(gè)狀態(tài)變遷到里另外一個(gè)狀態(tài).根據(jù)結(jié)構(gòu)化機(jī)器假設(shè),機(jī)器M的狀態(tài)由M中的所有存儲(chǔ)單元取值構(gòu)成.存儲(chǔ)單元包括寄存器(registers)、內(nèi)存單元(memory)或者磁盤扇區(qū)(disk)等.上述存儲(chǔ)單元有一些是不可觀察的(如內(nèi)部存儲(chǔ)單元),有一些是暴露給觀察者的;有一些是只讀的,有一些是可讀可寫的;有一些是遺失性的,有一些是非遺失性的,等等,所有這些存儲(chǔ)單元的取值情況決定了機(jī)器M的當(dāng)前狀態(tài).在實(shí)踐中,用戶可以根據(jù)實(shí)際需要,基于定義1、定義2,將實(shí)際系統(tǒng)與機(jī)器M一一對(duì)應(yīng)起來.

定義3.是等價(jià)關(guān)系,當(dāng)且僅當(dāng)同時(shí)滿足輸出一致性和弱單步一致性.

本文全文遵從文獻(xiàn)[25],約定使用?表示蘊(yùn)含關(guān)系,使用→定義函數(shù).

定義4.引用監(jiān)視器假設(shè)RMA(reference monitor assumption).RMA 由如下3 條假設(shè)構(gòu)成.

(3) 假設(shè)3:contents(step(s,a),n)≠contents(s,n)?n∈alter(dom(a)).其含義是:若動(dòng)作修改了某a個(gè)存儲(chǔ)單元的值,則安全域dom(a)必須擁有對(duì)該存儲(chǔ)單元修改授權(quán).

定義5.干擾源集interfsrcs:B×D→P(D).干擾源集的遞歸定義為interfsrcs(Λ,u)={u},且

干擾源集的含義是:抽取所有對(duì)u有(直接或間接)干擾關(guān)系的安全域形成(干擾源)集合.

定義6.弱預(yù)期函數(shù)wexpected:B×D→B.其遞歸定義為wexpected(Λ,u)=Λ,且

弱預(yù)期函數(shù)的含義是:將所有對(duì)u有(直接或間接)干擾關(guān)系的動(dòng)作保留,并將除此以外的所有動(dòng)作刪除,從而得到在非傳遞無干擾安全策略控制下的預(yù)期行為.

定義7.域集等價(jià)關(guān)系

定義8.局部無干擾屬性:

2.2 基于無干擾的可信性判定

根據(jù)文獻(xiàn)[25],一個(gè)信息系統(tǒng)滿足無干擾,當(dāng)且僅當(dāng)如下判定等式(1)成立.

定義9.無干擾判定等式:

關(guān)于什么是“可信”,國際上可信計(jì)算組織TCG 將其定義為:(1) 完整性;或(2) 行為符合預(yù)期;國內(nèi)有專家指出:(3) 可信≈可靠+安全.形式上,等式(1)對(duì)這些“可信”的定義均可以進(jìn)行解釋.

(1) “完整性”的定義

等式(1)的左邊表示行為α的實(shí)際執(zhí)行結(jié)果,右邊表示在完整性策略控制下,行為wexpected(α,dom(a))的理論執(zhí)行結(jié)果.如果等式成立,則表明真實(shí)執(zhí)行結(jié)果與完整性策略控制下的執(zhí)行結(jié)果一致,換句話說,當(dāng)前的執(zhí)行是符合完整性策略的.因而完整性沒有遭到破壞.

事實(shí)上,利用無干擾研究和解釋完整性是完全可行的.我們?cè)儐栁墨I(xiàn)[31]的作者Ryan 是否可以利用無干擾研究完整性,Ryan 回復(fù)指出:“利用無干擾研究完整性是完全可行的.唯一的細(xì)微差別在于,完整性無干擾模型可能需要一個(gè)更弱一點(diǎn)的形式化:對(duì)于安全性/機(jī)密性必須確保低(low)安全等級(jí)觀察者不能夠推斷出任何高(high)安全等級(jí)的信息;而對(duì)于完整性很可能不需要擔(dān)心高(high)完整性等級(jí)能夠推斷出低(low)完整性等級(jí)的信息,只要低完整性等級(jí)信息不能干擾高完整性等級(jí)信息即可”.

(2) “行為符合預(yù)期”的定義

類似的,等式(1)的左邊表示行為α的實(shí)際執(zhí)行結(jié)果,右邊表示在安全策略控制下,行為wexpected(α,dom(a))的理論執(zhí)行結(jié)果(預(yù)期執(zhí)行結(jié)果).如果等式成立,則表示真實(shí)執(zhí)行結(jié)果與預(yù)期執(zhí)行結(jié)果一致.換句話說,機(jī)器M是以預(yù)期的方式朝著預(yù)期的目標(biāo)在執(zhí)行,因而是可信的.

(3) “安全性(機(jī)密性)”的定義

這是無干擾模型提出的本義,因而自然成立.

綜上所述,對(duì)于“可信”的幾種主流定義,等式(1)均可以給予解釋.我們認(rèn)為,無干擾模型是研究可信的一個(gè)非常合適的數(shù)學(xué)工具.

接下來的困難在于如何將無干擾模型應(yīng)用于實(shí)時(shí)動(dòng)態(tài)系統(tǒng).Rushby 曾明確指出了無干擾模型所面臨的挑戰(zhàn)[25]:一是尋求有效(efficient and effective)的無干擾屬性自動(dòng)化驗(yàn)證算法,二是探索無干擾模型的實(shí)際應(yīng)用.本質(zhì)上,這兩個(gè)問題可以歸結(jié)為第1 個(gè)問題.因此,雖然無干擾模型非常適用于可信研究,但是要真正應(yīng)用于實(shí)時(shí)動(dòng)態(tài)度量和防護(hù),就必須解決無干擾屬性的自動(dòng)化驗(yàn)證問題.幸運(yùn)的是,我們?cè)谖墨I(xiàn)[45]中找到了一種與等式(1)等價(jià)、以狀態(tài)遞歸形式表達(dá)、可靠且完備的無干擾表達(dá)形式(參見如下定理2)解決了這個(gè)問題.詳細(xì)說明如下.

定理1(無干擾屬性驗(yàn)證展開定理[25]).如果機(jī)器M滿足如下屬性,則機(jī)器M是滿足無干擾的,或者說可信的.

證明:參見文獻(xiàn)[25]定理7.□

Rushby 將等式(1)看作一個(gè)狀態(tài)機(jī),利用歸納法證明了定理1 所示的展開定理.在文獻(xiàn)[45]中,我們將等式(1)的左右兩邊看作兩個(gè)狀態(tài)機(jī),分別稱為等價(jià)自動(dòng)機(jī)EMA(equivalent machine’s automaton)和弱預(yù)期等價(jià)自動(dòng)機(jī)WEMA(weakly equivalent machine’s automaton).不失一般性,假設(shè)左右兩個(gè)狀態(tài)機(jī)的狀態(tài)集分別是S和T,則等式(1)中的EMA 和WEMA 將從相同的初始狀態(tài)s0=t0(s0∈S∧t0∈T)出發(fā),分別執(zhí)行行為α以及安全策略控制下的行為β=wexpected(α,dom(a)).利用EMA 和WEMA,可以證明定理1 的3 條屬性的數(shù)學(xué)本質(zhì)是:EMA 和WEMA在同步執(zhí)行的過程中,總是保持狀態(tài)等價(jià)的[45].該數(shù)學(xué)本質(zhì)可以形式地表達(dá)為定理2.

定理2(無干擾(或者說可信)的狀態(tài)遞歸定義[45]).機(jī)器M是滿足無干擾的,或者說可信的,當(dāng)且僅當(dāng):

證明:參見文獻(xiàn)[45]的定理3. □

定理2 中的符號(hào)含義如下.

(1)N:對(duì)于任意行為γ,N是γ中原子動(dòng)作的個(gè)數(shù).例如,不失一般性,設(shè)α=a0。a1?！?。am,則γ中共有m個(gè)原子動(dòng)作,故N=m.

(2)γi(0≤i≤N):對(duì)于任意行為γ,隨著機(jī)器M對(duì)γ中原子動(dòng)作的不斷執(zhí)行,用γi表示剩下的行為,稱為“執(zhí)行子行為串”(參見文獻(xiàn)[45]的定義16),并令γ0=γ,γN=Λ.例如,不失一般性,設(shè)α=a0。a1?！?。am,則有:初始時(shí),γ0=γ=a0。a1?！m;當(dāng)機(jī)器M執(zhí)行原子動(dòng)作a1后,有γ1=a2?！m;...;當(dāng)機(jī)器M執(zhí)行am?1后,有γm?1=am;當(dāng)機(jī)器M執(zhí)行am后,有γm=γN=Λ.

(3)ISiγ:如果用w表示等式(1)中的dom(a),即w=dom(a),則為了書寫簡(jiǎn)單起見,文獻(xiàn)[45]中約定,即的含義是:所有對(duì)w=dom(a)有直接或者間接干擾的安全域構(gòu)成的集合.

(4)si和si+1:si表示EMA 的當(dāng)前狀態(tài),si+1表示EMA 從當(dāng)前狀態(tài)si執(zhí)行γi=ai+1?！?。am中的第1 個(gè)原子動(dòng)作ai+1之后到達(dá)的新狀態(tài),si+1=step(si,ai+1).

(5)ti和ti+1:ti表示W(wǎng)EMA 的當(dāng)前狀態(tài),ti+1表示W(wǎng)EMA 從當(dāng)前狀態(tài)ti執(zhí)行βi=wexpected(γi,w)中的第1 個(gè)原子動(dòng)作之后到達(dá)的新狀態(tài)ti+1.由公式(4)中的γi=ai+1。…。am,根據(jù)定義6,當(dāng)dom(ai+1)∈interfsrcs(γi,w),即dom(ai+1)對(duì)w=dom(a)有直接或者間接干擾時(shí),βi=wexpected(γi,w)的第1 個(gè)原子動(dòng)作為ai+1,此時(shí)ti+1=step(ti,ai+1);否則,若dom(ai+1)?interfsrcs(γi,w),即dom(ai+1)對(duì)w=dom(a)沒有任何干擾時(shí),βi=wexpected(γi,w)的第1 個(gè)原子動(dòng)作為Λ,此時(shí)ti+1=step(ti,Λ)=ti.

綜上,定理2(公式(2))的含義是:機(jī)器M是無干擾的,或者說可信的,當(dāng)且僅當(dāng)EMA 和WEMA 兩個(gè)狀態(tài)機(jī)在同步運(yùn)行的過程中,總是在對(duì)w=dom(a)(參見等式(1))有直接或者間接干擾的安全域上保持狀態(tài)等價(jià)的.

定理2 是無干擾成立的可靠和完備性條件.限于篇幅,其證明思想簡(jiǎn)單說明如下.

(1) 可靠性證明

(2) 完備性證明

完備性證明采用反證法.根據(jù)引用監(jiān)視器假設(shè),機(jī)器M的狀態(tài)具體表現(xiàn)為其名字集的取值.因此,EMA 和WEMA 狀態(tài)等價(jià),本質(zhì)上等價(jià)于EMA 和WEMA 對(duì)應(yīng)名字集的取值相同.再注意到某個(gè)名字的值發(fā)生變化時(shí),是由該名字當(dāng)前本身的值加上當(dāng)前對(duì)其進(jìn)行干擾的名字的值共同決定的.綜合以上兩點(diǎn),要保證 EMA 和WEMA 在w上的狀態(tài)等價(jià)關(guān)系,就必須要保證EMA 和WEMA 在同步運(yùn)行的過程中,在所有那些對(duì)w有直接或者間接干擾的安全域上總是保持狀態(tài)等價(jià)的,亦即當(dāng)EMA 和WEMA 到達(dá)任意狀態(tài)對(duì)(si,ti)時(shí),必須在上是保持狀態(tài)等價(jià)的,此即公式(2).否則,就一定可以構(gòu)造一個(gè)惡意子行為,使得當(dāng)M從狀態(tài)si出發(fā)執(zhí)行iγ′后,EMA 和WEMA 最終在w上不等價(jià),從而導(dǎo)致公式(1)不成立,M不滿足無干擾屬性,矛盾!完備性得證.□

更詳細(xì)的證明請(qǐng)參見[45]的定理3.

接下來以一個(gè)例子說明定理2 的含義及應(yīng)用.假設(shè)某個(gè)涉密系統(tǒng)中劃分有輸入域ui(input)、過濾域uf(filter)、加密機(jī)域ue(encryption)和網(wǎng)絡(luò)域un(network)共4 個(gè)安全域.系統(tǒng)安全策略是:從輸入域ui接收所有的輸入,經(jīng)過濾域uf過濾識(shí)別出敏感信息,再經(jīng)加密域ue的加密機(jī)加密,最后將加密后的密文經(jīng)網(wǎng)絡(luò)域un傳出,輸入域ui和過濾域uf禁止直接向網(wǎng)絡(luò)傳輸信息.安全策略可以表達(dá)為:

再令安全域ui,uf,ue和un中發(fā)出的動(dòng)作分別用ai,af,ae和an表示.不失一般性,假設(shè)有如下動(dòng)作序列(即行為):α=ai1。af1。ai2。ae。af2,則根據(jù)安全策略計(jì)算WEMA 中的對(duì)應(yīng)行為β=wexpected(α,un),由定義6 可得:β=ai1。af1。Λ。ae。Λ.根據(jù)定理2,行為α是否可信的自動(dòng)化驗(yàn)證過程如圖1 所示.圖1 中的圓圈表示狀態(tài),圓圈之間的箭頭表示引發(fā)狀態(tài)變遷的動(dòng)作,圓圈之間的虛線表示EMA 和WEMA 同步執(zhí)行的過程.

Fig.1 Trust verification/measurement of software based on noninterference (Theorem 2)圖1 基于無干擾理論的(定理2)的軟件可信驗(yàn)證/度量

對(duì)α=ai1。af1。ai2。ae。af2的可信性驗(yàn)證過程如下.

(1) 首先,EMA 和WEMA 兩者從相同的初始狀態(tài)s0=t0出發(fā)同步運(yùn)行.

根據(jù)定理2 的符號(hào)解釋:

· 對(duì)EMA:此時(shí),α0=α=ai1。af1。ai2。ae。af2.EMA 執(zhí)行首個(gè)動(dòng)作ai1之后,從狀態(tài)s0變遷到狀態(tài)s1,并將繼續(xù)執(zhí)行子行為α1=af1。ai2。ae。af2.

· 對(duì)WEMA:此時(shí),β0=β=ai1。af1。Λ。ae。Λ.WEMA 執(zhí)行首個(gè)動(dòng)作ai1之后,從狀態(tài)t0=s0變遷到狀態(tài)t1,并將繼續(xù)執(zhí)行子行為β1=af1。Λ。ae。Λ.

(2) 其次,繼續(xù)根據(jù)公式(2)遞歸驗(yàn)證行為是否可信.

· 對(duì)EMA:此時(shí),α1=af1。ai2。ae。af2.EMA 執(zhí)行動(dòng)作af1之后,從狀態(tài)s1變遷到狀態(tài)s2,并將繼續(xù)執(zhí)行子行為α2=ai2。ae。af2.

· 對(duì)WEMA:此時(shí),β1=af1。Λ。ae。Λ.WEMA 執(zhí)行動(dòng)作af1之后,從狀態(tài)t1變遷到狀態(tài)t2,并將繼續(xù)執(zhí)行子行為β2=Λ。ae。Λ.

(3),(4) 然后,繼續(xù)根據(jù)公式(2)驗(yàn)證行為是否可信.

(5) 最后,對(duì)于最后一個(gè)動(dòng)作af2,繼續(xù)根據(jù)公式(2)驗(yàn)證其運(yùn)行之后行為是否可信.

· 對(duì)EMA:此時(shí),α5=af2=af2。Λ.EMA 執(zhí)行動(dòng)作af2之后,從狀態(tài)s4變遷到狀態(tài)s5,并將繼續(xù)執(zhí)行子行為α6=Λ.

· 對(duì)WEMA:此時(shí),β1=Λ=Λ。Λ.WEMA 執(zhí)行空動(dòng)作Λ,狀態(tài)保持不變s4=s5,并將繼續(xù)執(zhí)行子行為β6=Λ.

示例結(jié)束.

由于傳遞無干擾是非傳遞無干擾的特例,對(duì)于傳遞無干擾,定理2 可以簡(jiǎn)化為推論1.

推論1(傳遞無干擾的狀態(tài)遞歸定義).在傳遞無干擾安全策略下,機(jī)器M是滿足無干擾的,或者說可信的,當(dāng)且僅當(dāng):

其中,w=dom(a)是定義9 中觀察動(dòng)作a所屬的安全域.

證明:根據(jù)傳遞無干擾安全策略定義,所有對(duì)w發(fā)生干擾的安全域,無需通過任何中間(intermediate)媒介安全域,即可直接對(duì)w進(jìn)行干擾.這意味著無需保證EMA 和WEMA 在中間安全域(公式(2)中上的狀態(tài)等價(jià)性,只要確保兩者總是在w上等價(jià)即可.故公式(2)可簡(jiǎn)化為,即

注意到,如下公式(5)和公式(6)是公式(4)前后相繼的兩次驗(yàn)證,且公式(6)的前件正好是公式(5)的后件.

再注意到,只有公式(5)驗(yàn)證通過之后,才會(huì)驗(yàn)證公式(6).這意味著當(dāng)驗(yàn)證公式(6)時(shí),其前件必然成立,故而對(duì)公式(6),只需要驗(yàn)證后件即可.

考察公式(4),令j=j+1,其后件下標(biāo)滿足1≤j≤N+1,故只需要驗(yàn)證即可.

此即公式(3),推論1 得證.□

3 方法及實(shí)現(xiàn)

3.1 基本思想

大多數(shù)攻擊都需要兩個(gè)步驟:首先,定位可利用的漏洞;其次,通過漏洞執(zhí)行攻擊代碼(稱為shellcode).只要打斷以上環(huán)環(huán)相扣的兩個(gè)步驟中的任何一步,即可以有效防御攻擊.本文從第2 步入手,建立在如下觀察之上:幾乎所有的shellcode 都必須通過系統(tǒng)調(diào)用達(dá)成攻擊.由此,一旦檢測(cè)到系統(tǒng)調(diào)用序列的語義破壞了定義9 的等式(1),即可以認(rèn)定破壞了系統(tǒng)的可信性.

圖2 給出了基于無干擾理論的軟件實(shí)時(shí)可信防護(hù)方法,包括3 部分.

(1) 預(yù)期行為規(guī)范EBS(expected behavior specification).

預(yù)期行為規(guī)范基于系統(tǒng)調(diào)用編寫,描述了進(jìn)程的預(yù)期行為,即進(jìn)程預(yù)期可以可以做什么,或者預(yù)期不可以做什么.EBS 的說明和示例請(qǐng)分別參見第3.3 節(jié)和附錄.

(2) 每一個(gè)進(jìn)程綁定一個(gè)預(yù)期行為規(guī)范EBS.

所綁定的EBS 描述了該進(jìn)程的預(yù)期行為,并且EBS 放置在內(nèi)核中.注意:在原型實(shí)驗(yàn)中,我們默認(rèn)內(nèi)核是可信的,因而將EBS 放置在內(nèi)核中可以保護(hù)其完整性.

需要指出的是,內(nèi)核完全有可能是不可信的,但如何確保內(nèi)核可信超出了本文的研究范圍.對(duì)于內(nèi)核不可信情況下保證EBS 完整性的可能方法有:采用現(xiàn)有的技術(shù)對(duì)內(nèi)核進(jìn)行加固[7,8,18?21],從而增強(qiáng)內(nèi)核中EBS 的完整性;或者將EBS 放置在TPM 安全協(xié)處理芯片、TrustZone 的安全世界等類似硬軟件安全架構(gòu)中,保證EBS 的完整性.

(3) 安全增強(qiáng)的內(nèi)核實(shí)時(shí)監(jiān)測(cè)軟件行為是否偏離預(yù)期.

Fig.2 Approach for real-time-trusted protection of software based on noninterference圖2 基于無干擾理論的軟件實(shí)時(shí)可信防護(hù)方法

安全增強(qiáng)后的內(nèi)核,對(duì)每個(gè)進(jìn)程實(shí)時(shí)捕獲其系統(tǒng)調(diào)用,并依據(jù)定理2(推論1)實(shí)時(shí)判定進(jìn)程的行為是否偏離了預(yù)期(即EBS),由此發(fā)現(xiàn)各類復(fù)雜攻擊(如新型的ROP 攻擊以及傳統(tǒng)的多態(tài)、混淆、變形和編碼攻擊等),理論上也可以識(shí)別未知攻擊(因?yàn)榧词故俏粗?絕大多數(shù)情況下也需要執(zhí)行shellcode,而只要shellcode 的行為偏離了EBS,即可以被捕獲).

根據(jù)文獻(xiàn)[25],構(gòu)成進(jìn)程行為的原子動(dòng)作可以是輸入(input)、命令(command)、機(jī)器指令(instruction)等任意可以被機(jī)器所執(zhí)行的內(nèi)容.本文選擇系統(tǒng)調(diào)用作為原子動(dòng)作,并以Linux 操作系統(tǒng)作為原型環(huán)境.系統(tǒng)調(diào)用、EBS和機(jī)器M這三者之間的關(guān)系如下:系統(tǒng)調(diào)用作為原子動(dòng)作,其執(zhí)行導(dǎo)致機(jī)器M發(fā)生狀態(tài)變遷;EBS 作為安全策略,描述了系統(tǒng)調(diào)用所屬安全域之間的干擾/無干擾關(guān)系;在此基礎(chǔ)上,軟件動(dòng)態(tài)執(zhí)行是可信的,當(dāng)且僅當(dāng)在EBS的控制下,其系統(tǒng)調(diào)用執(zhí)行滿足推論1 所示的充要條件.

3.2 進(jìn)程系統(tǒng)調(diào)用所屬安全域之間的無干擾關(guān)系

根據(jù)根據(jù)Linux 手冊(cè),基于不同的功能,Linux 系統(tǒng)調(diào)用可以分為如下8 類[48],分別是:(1) 進(jìn)程控制類(u0);(2) 文件系統(tǒng)控制類(u1);(3) 系統(tǒng)控制類(u2);(4) 內(nèi)存管理類(u3);(5) 網(wǎng)絡(luò)管理類(u4);(6) 網(wǎng)絡(luò)Socket 控制類(u5);(7) 用戶管理類(u6);(8) 進(jìn)程間通信類(u7).這8 類系統(tǒng)調(diào)用可以看作8 個(gè)不同的安全域,分別用u0～u7表示.由于系統(tǒng)調(diào)用之間的功能隔離關(guān)系(操作系統(tǒng)內(nèi)核設(shè)計(jì)決定了系統(tǒng)調(diào)用的功能劃分不會(huì)存在耦合關(guān)系,否則會(huì)導(dǎo)致非預(yù)期行為),這8 個(gè)安全域之間是互相無干擾的,形式地:.這意味著安全策略由復(fù)雜的非傳遞安全策略退化為簡(jiǎn)單的傳遞安全策略,因而在判定軟件真實(shí)行為與EBS 之間是否存在偏差時(shí),只需要使用推論1 即可,這大大簡(jiǎn)化了行為可信驗(yàn)證算法的時(shí)間復(fù)雜度(參見第3.5 節(jié)).需要指出的是,這種簡(jiǎn)化具有一般性,因?yàn)槠涫怯上到y(tǒng)調(diào)用所屬安全域之間的無干擾關(guān)系決定的.

3.3 基于系統(tǒng)調(diào)用的EBS編寫

限于篇幅,附錄給出了本文所采用的一種EBS 編寫形式作為示例.事實(shí)上,如何編寫和對(duì)應(yīng)解析EBS,并不限于示例1 所示的方法,可以由使用者自己決定,只要基于系統(tǒng)調(diào)用刻畫軟件預(yù)期行為即可.

EBS 具有如下特點(diǎn).

(1) EBS 可以采用無干擾信息流安全策略/?,也可以采用干擾信息流安全策略?.由無干擾模型定義可知,兩種安全策略本質(zhì)上是等價(jià)的.經(jīng)驗(yàn)表明:一般情況下,推薦使用/?安全策略,因?yàn)檫@可以得到復(fù)雜度更低的EBS.

(2) EBS 描述了軟件預(yù)期的行為,與具體攻擊行為無關(guān).因此,任何攻擊,包括Zero-Day 攻擊在內(nèi),理論上只要導(dǎo)致軟件行為偏離了預(yù)期,仍然可以被本文方法度量到.

(3) EBS 有兩種類型:一是適用于平臺(tái)所有軟件的通用EBS;二是綁定于特定軟件、滿足特定安全需求的特殊EBS.兩種EBS 可以同時(shí)使用.當(dāng)兩種EBS 同時(shí)存在的情況下,特殊EBS 優(yōu)先級(jí)高于通用EBS 優(yōu)先級(jí),增加了靈活性.

3.4 系統(tǒng)調(diào)用實(shí)時(shí)獲取

接下來,需要實(shí)時(shí)捕獲被監(jiān)控進(jìn)程的系統(tǒng)調(diào)用(含參數(shù))行為并與EBS 進(jìn)行對(duì)比,以判定進(jìn)程的運(yùn)行是否偏離了預(yù)期行為.方便起見,本文原型實(shí)驗(yàn)通過ptrace 實(shí)現(xiàn):將PTRACE_PEEKUSER 作為ptrace 的第1 個(gè)參數(shù)進(jìn)行調(diào)用,即可以實(shí)時(shí)取得與待度量進(jìn)程相關(guān)的系統(tǒng)調(diào)用信息.其中,

(1) EAX 當(dāng)中存儲(chǔ)的是系統(tǒng)調(diào)用的索引號(hào),亦即指明了具體的系統(tǒng)調(diào)用.

(2) 在32 位架構(gòu)中,當(dāng)系統(tǒng)調(diào)用參數(shù)的個(gè)數(shù)小于5 個(gè)時(shí),EBX,ECX,EDX,ESI,EDI 當(dāng)中依次存儲(chǔ)著系統(tǒng)調(diào)用所有的參數(shù);當(dāng)系統(tǒng)調(diào)用參數(shù)的個(gè)數(shù)大于5 個(gè)時(shí)(這種情況不多見),EBX 指向一塊內(nèi)存區(qū)域,這個(gè)區(qū)域中就依序存放著系統(tǒng)調(diào)用的所有參數(shù).

(3) 在64 位架構(gòu)當(dāng)中,%rdi,%rsi,%rdx,%r10,%r8,%r9 依次存放著系統(tǒng)調(diào)用參數(shù)信息.

3.5 實(shí)時(shí)可信性驗(yàn)證

第3.2 節(jié)說明,Linux 系統(tǒng)調(diào)用的8 個(gè)安全域之間互相無干擾,即.因此任何兩個(gè)安全域之間都無法利用第三安全域作為中間安全域(intermediate domain)來間接傳遞信息,這本質(zhì)上退化為傳遞無干擾,故使用推論1 來對(duì)進(jìn)程up的實(shí)時(shí)可信性進(jìn)行驗(yàn)證.推論1 可以表述為如下驗(yàn)證算法1.

算法1.進(jìn)程up實(shí)時(shí)可信度量(驗(yàn)證)算法.

1.任意時(shí)刻,實(shí)時(shí)獲取進(jìn)程up的本次系統(tǒng)調(diào)用,不失一般性,假設(shè)為本次執(zhí)行的系統(tǒng)調(diào)用為a.

2.遍歷 EBS,計(jì)算原子動(dòng)作a在 EBS 安全策略控制下的預(yù)期執(zhí)行動(dòng)作β=wexpected(a,w).根據(jù)wexpected(?)的定義,最終有β=a(EBS 安全策略預(yù)期允許執(zhí)行a)或者β=Λ(EBS 安全策略預(yù)期不允許執(zhí)行a).

3.如果β=a,則進(jìn)程真實(shí)執(zhí)行與預(yù)期執(zhí)行一致(真實(shí)執(zhí)行動(dòng)作和預(yù)期執(zhí)行動(dòng)作都是a,兩者執(zhí)行之后狀態(tài)一致,故在EBS 關(guān)注的w上等價(jià)),根據(jù)推論1,up執(zhí)行a后可信,轉(zhuǎn)步驟1;如果β=Λ,則進(jìn)程真實(shí)執(zhí)行與預(yù)期執(zhí)行不一致(真實(shí)執(zhí)行動(dòng)作a,預(yù)期執(zhí)行空動(dòng)作Λ,兩者執(zhí)行之后導(dǎo)致狀態(tài)空間不一致,故在EBS 所關(guān)注的w上不等價(jià)),up執(zhí)行a后不可信,報(bào)警.

算法1 結(jié)束.算法1 只需要在每次系統(tǒng)調(diào)用a執(zhí)行時(shí),判定a是否被EBS 安全策略所允許即可,因而其時(shí)間復(fù)雜度為O(1).

4 實(shí)驗(yàn)評(píng)估

實(shí)驗(yàn)平臺(tái)采用TOSHIBA 筆記本電腦,CPU Intel i5 2.5G,內(nèi)存Samsung 8G.操作系統(tǒng)Linux Fedora,內(nèi)核版本2.6.43.8-1.fc15.i686.PAE.實(shí)驗(yàn)測(cè)試了在ROP 攻擊以及傳統(tǒng)代碼多態(tài)、代碼混淆、代碼變形和代碼編碼等對(duì)抗形式下對(duì)攻擊行為的可信度量功能.表1 給出了實(shí)驗(yàn)結(jié)果.

Table 1 Attacks that can be measured and protected in real time表1 可被實(shí)時(shí)度量和防護(hù)的攻擊方法

表1 顯示,本文的方法可以檢測(cè)到ROP(return-oriented programming)攻擊.ROP 代表了現(xiàn)代攻擊的發(fā)展趨勢(shì),其不尋求注入代碼,而是從已有的“干凈代碼”中尋找合適的“指令片段”(gadget),通過“ret 或者與ret 語義等價(jià)的指令”將前述指令片段鏈接形成完整的攻擊代碼,以達(dá)成攻擊目的.ROP 可以高度自動(dòng)化地構(gòu)造圖靈完全的攻擊,危害巨大.為此,研究人員提出了多種對(duì)抗方法[49?53],取得了長(zhǎng)足的進(jìn)展.早期的ROP 防御側(cè)重于檢測(cè)可疑的ret 指令,但沒有處理與ret 語義等價(jià)的指令(如jmp/pop 等)[49],對(duì)ROP 的防御是不完全的.隨后的工作實(shí)現(xiàn)了對(duì)各類ROP 攻擊的全覆蓋,其基本思想在于消除ROP 指令片段,或者檢測(cè)并阻止(ROP 指令片段所導(dǎo)致)的非法間接跳轉(zhuǎn).但這些方法均需要額外的條件,如,需要被保護(hù)應(yīng)用的非直接跳轉(zhuǎn)指令和地址[50],或者被保護(hù)應(yīng)用的指令片段IG(instruction & gadget)信息[51];需要硬件的特殊功能[52];需要特殊的編譯器[53];需要對(duì)受保護(hù)應(yīng)用進(jìn)行重寫[50,53]等等.不同于這些工作,本文的方法基于如下觀察:ROP 是一種代碼重用方法,其本身并不能達(dá)成攻擊,而仍然要通過調(diào)用敏感系統(tǒng)調(diào)用來實(shí)現(xiàn)惡意功能.因此,通過度量應(yīng)用程序系統(tǒng)調(diào)用與EBS 規(guī)范的偏離可以發(fā)現(xiàn)基于ROP 技術(shù)所發(fā)起的攻擊.嚴(yán)格來說,本文方法并不能檢測(cè)ROP 攻擊本身,這是與文獻(xiàn)[49?53]相比的不足之處.但從另外一個(gè)角度,在面向大量商業(yè)應(yīng)用和通用度量平臺(tái)的一般情況下——此時(shí)可能難以進(jìn)行預(yù)處理(因而難以獲得應(yīng)用本身的信息[50,51]),不一定具備特殊硬件和軟件(因而不一定滿足特定功能的CPU[52]和編譯器[53]要求),且不一定能夠進(jìn)行代碼重寫(如開啟了完整性度量架構(gòu)IMA),本文的方法可以作為上述方法的補(bǔ)充,結(jié)合應(yīng)用.

對(duì)于表1 中余下的4 種經(jīng)典攻擊代碼對(duì)抗方法,實(shí)驗(yàn)結(jié)果表明亦可以有效度量.從實(shí)驗(yàn)結(jié)果還可以發(fā)現(xiàn),通過分析和抽取已有shellcode 的特征,利用較少的EBS 規(guī)范(實(shí)驗(yàn)中采用了7 條主要EBS 規(guī)范),就可以覆蓋主要的攻擊流程和大量的攻擊代碼,實(shí)現(xiàn)對(duì)軟件可信性的實(shí)時(shí)度量,這表明方法是高效的.

表2 對(duì)實(shí)時(shí)度量的時(shí)間負(fù)載進(jìn)行了分析.實(shí)時(shí)度量所引起的時(shí)間負(fù)載由兩部分構(gòu)成:一是捕獲系統(tǒng)調(diào)用及其參數(shù)所花的時(shí)間t1;二是分析系統(tǒng)調(diào)用是否偏離了EBS 安全策略所花的時(shí)間t2.t2主要是字符串比較等指針操作,時(shí)間相對(duì)較快,大致取t2≈t1.再假設(shè)在未進(jìn)行實(shí)時(shí)度量時(shí)(no real-time measurement)軟件的運(yùn)行時(shí)間為TNRM=t0,則進(jìn)行實(shí)時(shí)度量時(shí)(real-time measurement)軟件的運(yùn)行時(shí)間為TRM=t0+t1+t2≈TNRM+2×t1,此時(shí),可求時(shí)間負(fù)載ζ為如下等式(7),故只要得到t1/t0即可.

利用time 命令和strace 命令,可以立即求出T0=t0以及T1=t0+t1,兩者相比有:

將等式(8)代入等式(7),即得ζ.

注意,time 命令會(huì)給出3 種時(shí)間.

(1) 真實(shí)時(shí)間(real):軟件從開始執(zhí)行到結(jié)束執(zhí)行的時(shí)間.

(2) 用戶CPU 時(shí)間(user):軟件在用戶態(tài)花費(fèi)的CPU 時(shí)間.

(3) 系統(tǒng)CPU 時(shí)間(sys):軟件在內(nèi)核態(tài)花費(fèi)的CPU 時(shí)間.那么對(duì)應(yīng)可以定義Tr0,Tr1;Tu0,Tu1;Ts0,Ts1.由于真實(shí)時(shí)間包含了軟件由于等待如I/O 等資源的掛起時(shí)間,其意義不大,一般關(guān)注后兩者(后兩者之和user+sys 給出了軟件運(yùn)行的真實(shí)CPU 時(shí)間),則等式(7)和等式(8)可以對(duì)應(yīng)改寫如下.

表2 給出了Tu1/Tu0和Ts1/Ts0的實(shí)驗(yàn)結(jié)果.

Table 2 Time-load analysis of real-time measurement表2 實(shí)時(shí)度量時(shí)間負(fù)載分析

取平均時(shí)間比,將Tu1/Tu0=5.05 和Ts1/Ts0=5.58 代入等式(9),有tu1/tu0=4.05 以及ts1/ts0=4.58;再代入等式(8),立即可得:ζu=9.1,ζs=10.16,ζ=9.63.因此在實(shí)時(shí)度量時(shí),一般情況下,用戶時(shí)間負(fù)載ζu約為9.10 倍,系統(tǒng)時(shí)間負(fù)載ζs約為10.16 倍,總體時(shí)間負(fù)載ζs約為9.63 倍.

以上各類時(shí)間負(fù)載總體約為10 倍,但這已經(jīng)本方法所能達(dá)到的接近最優(yōu)結(jié)果,且實(shí)際測(cè)試表明,該負(fù)載并不影響用戶的實(shí)際使用體驗(yàn).原因如下.

(1) 實(shí)驗(yàn)所選取的測(cè)試數(shù)據(jù)是接近最壞情況下的測(cè)試數(shù)據(jù).本文方法對(duì)系統(tǒng)調(diào)用進(jìn)行捕獲和度量,對(duì)其他函數(shù)和指令則不做任何處理,顯然,被測(cè)試代碼中系統(tǒng)調(diào)用相關(guān)代碼所占的比例越高,則對(duì)時(shí)間負(fù)載影響越大.注意到shellcode 正好滿足上述特征:考慮到存儲(chǔ)空間,shellcode 會(huì)盡可能短小精干,去除冗余指令以調(diào)用系統(tǒng)調(diào)用完成攻擊功能.換句話說,系統(tǒng)調(diào)用相關(guān)代碼所占比例高.因此,本文直接選擇shellcode 代碼為測(cè)試對(duì)象,所得的10x 時(shí)間負(fù)載約為最壞情況下的結(jié)果.一般情況下,測(cè)試結(jié)果表明,時(shí)間負(fù)載會(huì)介于1.6x～10x 之間.

(2) 前面已說明,時(shí)間負(fù)載由兩部分構(gòu)成:捕獲系統(tǒng)調(diào)用和參數(shù)的t1以及分析系統(tǒng)調(diào)用是否偏離EBS 的t2,且取t2≈t1.實(shí)驗(yàn)中,為方便起見,使用strace 命令獲取系統(tǒng)調(diào)用和參數(shù)信息(strace 仍然基于ptrace 實(shí)現(xiàn)).由于strace 是Linux 標(biāo)準(zhǔn)命令,因此t1可以認(rèn)為是優(yōu)化后的最優(yōu)結(jié)果,從而基于表2 所計(jì)算到的時(shí)間負(fù)載ζu,ζs和ζ也可以認(rèn)為是接近最優(yōu)的結(jié)果.

(3) 以用戶交互性強(qiáng)的應(yīng)用為測(cè)試對(duì)象表明,本文方法所引起的時(shí)間負(fù)載并不影響用戶使用感受.以Firefox 為例,利用“time strace firefox”命令啟動(dòng)火狐瀏覽器并瀏覽文本、圖片和視頻等各類網(wǎng)頁,統(tǒng)計(jì)時(shí)間信息并計(jì)算可得:若將real time 視作1,則user time 約占23%,sys time 約占8%,即陷入內(nèi)核CPU的運(yùn)行時(shí)間(sys time)僅僅約占8%,由于內(nèi)核CPU 時(shí)間(sys time)由系統(tǒng)調(diào)用和非系統(tǒng)調(diào)用時(shí)間兩部分構(gòu)成,因而實(shí)際捕獲系統(tǒng)調(diào)用和參數(shù)信息的時(shí)間不到8%.

根據(jù)測(cè)試結(jié)果,上述時(shí)間占比不影響用戶使用感受.

5 結(jié) 論

運(yùn)行時(shí)可信度量是可信計(jì)算有待解決的一個(gè)關(guān)鍵問題,本文提出了一種基于無干擾的軟件實(shí)時(shí)可信度量方法,嘗試為可信度量的理論構(gòu)建和實(shí)踐應(yīng)用提供一種新的思路.選擇無干擾模型是因?yàn)檠芯勘砻?無干擾模型可以以一種統(tǒng)一的形式描述“行為符合預(yù)期、完整性和機(jī)密性”等不同的主流“可信”定義,從而可以在統(tǒng)一的框架下對(duì)不同內(nèi)涵的可信性進(jìn)行研究.在此基礎(chǔ)上,給出了行為可信性的實(shí)時(shí)判定算法(時(shí)間復(fù)雜度O(1)),解決了無干擾模型難以應(yīng)用于實(shí)時(shí)系統(tǒng)的難題.針對(duì)理論的實(shí)踐應(yīng)用問題,根據(jù)無干擾模型的定義,選擇系統(tǒng)調(diào)用作為基本原子動(dòng)作,將軟件真實(shí)行為定義為原子動(dòng)作的序列,并根據(jù)系統(tǒng)調(diào)用所屬安全域之間的無干擾關(guān)系定義預(yù)期行為規(guī)范EBS.最后,通過判定軟件真實(shí)行為與預(yù)期行為之間是否存在偏差,實(shí)現(xiàn)對(duì)軟件行為的實(shí)時(shí)可信度量.原型實(shí)驗(yàn)證明了本文方法的有效性.

后續(xù)的研究擬從如下幾個(gè)方面入手:一是探索如何結(jié)合人工智能技術(shù)自動(dòng)抽取惡意代碼樣本特征并形成預(yù)期行為規(guī)范庫;二是研究適用于實(shí)時(shí)或者準(zhǔn)實(shí)時(shí)環(huán)境的漏洞定位技術(shù);三是研究移動(dòng)智能終端、物聯(lián)網(wǎng)等環(huán)境下的實(shí)時(shí)可信度量和防護(hù)問題.

附錄.EBS 編寫示例

攻擊者在定位漏洞之后,往往會(huì)執(zhí)行一些通用攻擊操作,以達(dá)成進(jìn)一步攻擊目的,這些通用攻擊操作包括(但不限于)生成shell、開啟反向連接、清空防火墻規(guī)則、關(guān)閉地址空間布局隨機(jī)化ASLR 等等.針對(duì)這些攻擊,這里給出部分EBS 示例如下:

1.EBS 規(guī)范1:預(yù)期不能生成shell.

u[i][j]的下標(biāo)分別是i,j,其表明:i是安全域ui的編號(hào),j是ui中子安全域編號(hào).因此,這里u[i][j]=u[0][0]的含義是u0安全域中的第1 個(gè)子安全域.類似的,如果是u1安全域中的第3 個(gè)子安全域,則表示為u[1][2].

回到u[0][0]={2},查閱[48]可知,u0安全域?yàn)檫M(jìn)程控制類系統(tǒng)調(diào)用,其中,編號(hào)2 對(duì)應(yīng)execve,故u[0][0]={2}={execve}.再結(jié)合FOR INDEX==2:語句的參數(shù)安全策略,由于execve 的第1 個(gè)參數(shù)是字符串類型,指明了要運(yùn)行的二進(jìn)制文件名,因此規(guī)范1 的含義是:進(jìn)程up預(yù)期不能運(yùn)行/bin 目錄下的bash,sh,tcsh,csh 和dash 文件以開啟shell.

解釋:攻擊者突破系統(tǒng)之后,一般需要開啟shell 以進(jìn)一步執(zhí)行命令.規(guī)范1 度量并禁止了這種行為.需要說明的是:Linux 的shell 并不只有上述5 種類型(規(guī)范1 是根據(jù)實(shí)驗(yàn)者機(jī)器的配置情況編寫的),使用者可以根據(jù)實(shí)際安全需求容易地更新規(guī)范1.

2.規(guī)范2:預(yù)期不能開啟非法監(jiān)聽端口連接或者不能進(jìn)行反向連接.

規(guī)范2 的含義是:進(jìn)程up預(yù)期對(duì)子安全域u[5][0]無干擾.查閱文獻(xiàn)[48]可知,u5中2 和3 號(hào)系統(tǒng)調(diào)用分別為bind和connect.進(jìn)一步查閱bind 和connect 參數(shù)信息,兩者的第2 個(gè)參數(shù)均是常量結(jié)構(gòu)體指針const struct sockaddr*,該結(jié)構(gòu)體的內(nèi)部元素sa_familiy 指明了協(xié)議族;sin_port 指明了端口號(hào);sin_addr 指明了遠(yuǎn)程連接的IP 地址.結(jié)合FOR INDEX==2:語句的參數(shù)安全策略可知,進(jìn)程up預(yù)期對(duì)所有不在端口列表PORT_LIST1當(dāng)中的端口都不能開放監(jiān)聽.類似地,結(jié)合FOR INDEX==3:語句的參數(shù)安全策略可知,進(jìn)程up預(yù)期不能對(duì)端口列表PORT_LIST2和地址列表IP_LIST中的機(jī)器發(fā)起遠(yuǎn)程連接.

解釋:攻擊者突破系統(tǒng)之后,往往會(huì)開啟受害機(jī)器監(jiān)聽端口監(jiān)聽外部連接,以方便進(jìn)一步入侵.為此,規(guī)范2的安全策略預(yù)期進(jìn)程up不會(huì)開啟必要端口(即PORT_LIST1中列出的端口)之外的任何端口,從而能夠度量并禁止攻擊者非法開啟監(jiān)聽端口的行為.另一方面,在內(nèi)網(wǎng)中,由于防火墻的存在,外網(wǎng)機(jī)向內(nèi)網(wǎng)機(jī)的連接會(huì)觸發(fā)警報(bào).此時(shí),攻擊者往往會(huì)從受害的內(nèi)網(wǎng)機(jī)向外網(wǎng)特定機(jī)器發(fā)起反向連接.規(guī)范2 度量并禁止了這種反向連接(反彈端口)行為.

3.規(guī)范3:預(yù)期不能清空防火墻規(guī)則.

規(guī)范3 的含義是:進(jìn)程up預(yù)期對(duì)子安全域u[0][1]無干擾.由于規(guī)則1 中u[0][0]和這里u[0][1]均是來自于u0的子安全域,因此兩者賦予不同的編號(hào)j=0 和j=1.類似地,查閱文獻(xiàn)[48]可知:規(guī)范3 表明,進(jìn)程up預(yù)期不能帶參數(shù)“?F”執(zhí)行/sbin/iptables文件以清空所有防火墻規(guī)則.

解釋:規(guī)范3 度量并禁止了清空防火墻規(guī)則行為.

限于篇幅,這里給出3 個(gè)EBS 示例.

根據(jù)我們的分析結(jié)果,大多shellcode 的代碼有很強(qiáng)的功能重合性.換句話說,絕大多數(shù)shellcode 的惡意功能都局限于生成shell、開啟反向連接、清空防火墻規(guī)則、關(guān)閉地址空間布局隨機(jī)化ASLR、修改/etc/passwd 文件、提升權(quán)限和重啟等,只是其機(jī)器碼形式或者對(duì)抗手段(多態(tài)、混淆、變形和編碼)不一致.在我們的實(shí)驗(yàn)中,通過提煉這些重合功能,只需要不到10 條通用EBS,即可檢測(cè)到大多數(shù)shellcode,表明了方法的有效性.