軟件實時可信度量:一種無干擾行為可信性分析方法?

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

1(武漢輕工大學 數學與計算機學院,湖北 武漢 430023)

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

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

4(東華大學 電機系,臺灣 花蓮 08 153719)

5(宜蘭大學 資訊工程系,臺灣 宜蘭 02 415271)

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

7(暨南大學 網絡空間安全學院,廣東 廣州 510632)

可信計算經過長期發展,取得了令人矚目的成果[1?24].隨著可信計算成為高價值體系結構(如可信云等)的關鍵安全支撐技術之一,其自身安全性面臨著更高的挑戰.在這些挑戰中,本文關注于如下3 個問題.

(1) 第1 個問題是:當前可信計算缺少理論支撐,且理論研究與實踐應用部分脫節.

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

(2) 第2 個問題是:當前的可信度量屬于“被動發現”機制,缺少“主動防御”能力.

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

(3) 第3 個問題是:可信計算如何在層出不窮的攻擊手段下可靠地實現可信度量.

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

針對上述問題,本文提出了一種基于無干擾理論的軟件實時可信度量與防護方法,主要貢獻如下:

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

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

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

1 相關研究工作

1.1 可信度量相關研究工作

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

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

1.2 無干擾及其應用相關研究工作

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

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

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

1.3 基于系統調用的安全防護

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

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

1.4 攜帶證明的代碼

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

PCC 為代碼的可信執行建立堅實理論基礎,但應用到實時可信度量領域還存在如下難點需要解決.

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

(2) PCC 安全策略編寫代價較大.由于不同應用所使用的編程語言以及語言的安全特性等存在差異,使得難以構造一個統一、標準的形式化規范.換句話說,每一個應用的CP 都需要單獨提供其應用所對應的形式化規范.當安全策略發生變化,例如當發生網絡安全事件進行應急響應時,每個應用的形式化規范必須要對應更新,并重新編譯生成新的PCC 代碼.這大大增加了安全策略規范編寫、維護和更新的代價.

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

2 理論基礎

2.1 無干擾模型定義

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

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

定義1.無干擾模型定義.一個系統M可以用一個狀態機表示,其包含如下元素.

(1) 狀態機S,其中包含一個唯一的初始狀態s0.

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

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

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

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

(6) 干擾關系?和無干擾關系/?,分別表示信息授權/禁止在兩個安全域之間流動,兩者互為補集.

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

(8) 單步狀態變遷函數:step:S×A→S,描述了系統M的單步狀態變遷.

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

其描述了系統M從狀態s∈S執行行為(即多個原子動作序列)α=a0。…。am∈β之后所到達的新狀態.

(10) 行為結果函數(behavior consequence):behcon:S×A→O,給出了系統M在某個狀態s∈S,外界利用動作a∈A所能觀察到的結果o∈O.

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

定義2.結構化機器M.結構化機器M包含如下部分.

(1) 存儲單元集N.機器的每一個存儲單元都有一個獨一無二的名字,所有這些名字的集合構成存儲單元集N,又叫名字集N.存儲單元包含寄存器單元、內存單元、外存單元、緩存等.

(2) 值集V.當狀態一定的時候,每一個存儲單元都有一個具體的值v.所有存儲單元值的集合構成值集V.

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

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

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

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

定義3.是等價關系,當且僅當同時滿足輸出一致性和弱單步一致性.

本文全文遵從文獻[25],約定使用?表示蘊含關系,使用→定義函數.

定義4.引用監視器假設RMA(reference monitor assumption).RMA 由如下3 條假設構成.

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

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

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

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

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

定義7.域集等價關系

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

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

根據文獻[25],一個信息系統滿足無干擾,當且僅當如下判定等式(1)成立.

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

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

(1) “完整性”的定義

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

事實上,利用無干擾研究和解釋完整性是完全可行的.我們曾詢問文獻[31]的作者Ryan 是否可以利用無干擾研究完整性,Ryan 回復指出:“利用無干擾研究完整性是完全可行的.唯一的細微差別在于,完整性無干擾模型可能需要一個更弱一點的形式化:對于安全性/機密性必須確保低(low)安全等級觀察者不能夠推斷出任何高(high)安全等級的信息;而對于完整性很可能不需要擔心高(high)完整性等級能夠推斷出低(low)完整性等級的信息,只要低完整性等級信息不能干擾高完整性等級信息即可”.

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

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

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

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

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

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

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

證明:參見文獻[25]定理7.□

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

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

證明:參見文獻[45]的定理3. □

定理2 中的符號含義如下.

(1)N:對于任意行為γ,N是γ中原子動作的個數.例如,不失一般性,設α=a0。a1。…。am,則γ中共有m個原子動作,故N=m.

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

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

(4)si和si+1:si表示EMA 的當前狀態,si+1表示EMA 從當前狀態si執行γi=ai+1。…。am中的第1 個原子動作ai+1之后到達的新狀態,si+1=step(si,ai+1).

(5)ti和ti+1:ti表示WEMA 的當前狀態,ti+1表示WEMA 從當前狀態ti執行βi=wexpected(γi,w)中的第1 個原子動作之后到達的新狀態ti+1.由公式(4)中的γi=ai+1。…。am,根據定義6,當dom(ai+1)∈interfsrcs(γi,w),即dom(ai+1)對w=dom(a)有直接或者間接干擾時,βi=wexpected(γi,w)的第1 個原子動作為ai+1,此時ti+1=step(ti,ai+1);否則,若dom(ai+1)?interfsrcs(γi,w),即dom(ai+1)對w=dom(a)沒有任何干擾時,βi=wexpected(γi,w)的第1 個原子動作為Λ,此時ti+1=step(ti,Λ)=ti.

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

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

(1) 可靠性證明

(2) 完備性證明

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

更詳細的證明請參見[45]的定理3.

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

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

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

對α=ai1。af1。ai2。ae。af2的可信性驗證過程如下.

(1) 首先,EMA 和WEMA 兩者從相同的初始狀態s0=t0出發同步運行.

根據定理2 的符號解釋:

· 對EMA:此時,α0=α=ai1。af1。ai2。ae。af2.EMA 執行首個動作ai1之后,從狀態s0變遷到狀態s1,并將繼續執行子行為α1=af1。ai2。ae。af2.

· 對WEMA:此時,β0=β=ai1。af1。Λ。ae。Λ.WEMA 執行首個動作ai1之后,從狀態t0=s0變遷到狀態t1,并將繼續執行子行為β1=af1。Λ。ae。Λ.

(2) 其次,繼續根據公式(2)遞歸驗證行為是否可信.

· 對EMA:此時,α1=af1。ai2。ae。af2.EMA 執行動作af1之后,從狀態s1變遷到狀態s2,并將繼續執行子行為α2=ai2。ae。af2.

· 對WEMA:此時,β1=af1。Λ。ae。Λ.WEMA 執行動作af1之后,從狀態t1變遷到狀態t2,并將繼續執行子行為β2=Λ。ae。Λ.

(3),(4) 然后,繼續根據公式(2)驗證行為是否可信.

(5) 最后,對于最后一個動作af2,繼續根據公式(2)驗證其運行之后行為是否可信.

· 對EMA:此時,α5=af2=af2。Λ.EMA 執行動作af2之后,從狀態s4變遷到狀態s5,并將繼續執行子行為α6=Λ.

· 對WEMA:此時,β1=Λ=Λ。Λ.WEMA 執行空動作Λ,狀態保持不變s4=s5,并將繼續執行子行為β6=Λ.

示例結束.

由于傳遞無干擾是非傳遞無干擾的特例,對于傳遞無干擾,定理2 可以簡化為推論1.

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

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

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

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

再注意到,只有公式(5)驗證通過之后,才會驗證公式(6).這意味著當驗證公式(6)時,其前件必然成立,故而對公式(6),只需要驗證后件即可.

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

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

3 方法及實現

3.1 基本思想

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

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

(1) 預期行為規范EBS(expected behavior specification).

預期行為規范基于系統調用編寫,描述了進程的預期行為,即進程預期可以可以做什么,或者預期不可以做什么.EBS 的說明和示例請分別參見第3.3 節和附錄.

(2) 每一個進程綁定一個預期行為規范EBS.

所綁定的EBS 描述了該進程的預期行為,并且EBS 放置在內核中.注意:在原型實驗中,我們默認內核是可信的,因而將EBS 放置在內核中可以保護其完整性.

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

(3) 安全增強的內核實時監測軟件行為是否偏離預期.

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

安全增強后的內核,對每個進程實時捕獲其系統調用,并依據定理2(推論1)實時判定進程的行為是否偏離了預期(即EBS),由此發現各類復雜攻擊(如新型的ROP 攻擊以及傳統的多態、混淆、變形和編碼攻擊等),理論上也可以識別未知攻擊(因為即使是未知攻擊,絕大多數情況下也需要執行shellcode,而只要shellcode 的行為偏離了EBS,即可以被捕獲).

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

3.2 進程系統調用所屬安全域之間的無干擾關系

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

3.3 基于系統調用的EBS編寫

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

EBS 具有如下特點.

(1) EBS 可以采用無干擾信息流安全策略/?,也可以采用干擾信息流安全策略?.由無干擾模型定義可知,兩種安全策略本質上是等價的.經驗表明:一般情況下,推薦使用/?安全策略,因為這可以得到復雜度更低的EBS.

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

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

3.4 系統調用實時獲取

接下來,需要實時捕獲被監控進程的系統調用(含參數)行為并與EBS 進行對比,以判定進程的運行是否偏離了預期行為.方便起見,本文原型實驗通過ptrace 實現:將PTRACE_PEEKUSER 作為ptrace 的第1 個參數進行調用,即可以實時取得與待度量進程相關的系統調用信息.其中,

(1) EAX 當中存儲的是系統調用的索引號,亦即指明了具體的系統調用.

(2) 在32 位架構中,當系統調用參數的個數小于5 個時,EBX,ECX,EDX,ESI,EDI 當中依次存儲著系統調用所有的參數;當系統調用參數的個數大于5 個時(這種情況不多見),EBX 指向一塊內存區域,這個區域中就依序存放著系統調用的所有參數.

(3) 在64 位架構當中,%rdi,%rsi,%rdx,%r10,%r8,%r9 依次存放著系統調用參數信息.

3.5 實時可信性驗證

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

算法1.進程up實時可信度量(驗證)算法.

1.任意時刻,實時獲取進程up的本次系統調用,不失一般性,假設為本次執行的系統調用為a.

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

3.如果β=a,則進程真實執行與預期執行一致(真實執行動作和預期執行動作都是a,兩者執行之后狀態一致,故在EBS 關注的w上等價),根據推論1,up執行a后可信,轉步驟1;如果β=Λ,則進程真實執行與預期執行不一致(真實執行動作a,預期執行空動作Λ,兩者執行之后導致狀態空間不一致,故在EBS 所關注的w上不等價),up執行a后不可信,報警.

算法1 結束.算法1 只需要在每次系統調用a執行時,判定a是否被EBS 安全策略所允許即可,因而其時間復雜度為O(1).

4 實驗評估

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

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

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

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

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

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

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

注意,time 命令會給出3 種時間.

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

(2) 用戶CPU 時間(user):軟件在用戶態花費的CPU 時間.

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

表2 給出了Tu1/Tu0和Ts1/Ts0的實驗結果.

Table 2 Time-load analysis of real-time measurement表2 實時度量時間負載分析

取平均時間比,將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.因此在實時度量時,一般情況下,用戶時間負載ζu約為9.10 倍,系統時間負載ζs約為10.16 倍,總體時間負載ζs約為9.63 倍.

以上各類時間負載總體約為10 倍,但這已經本方法所能達到的接近最優結果,且實際測試表明,該負載并不影響用戶的實際使用體驗.原因如下.

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

(2) 前面已說明,時間負載由兩部分構成:捕獲系統調用和參數的t1以及分析系統調用是否偏離EBS 的t2,且取t2≈t1.實驗中,為方便起見,使用strace 命令獲取系統調用和參數信息(strace 仍然基于ptrace 實現).由于strace 是Linux 標準命令,因此t1可以認為是優化后的最優結果,從而基于表2 所計算到的時間負載ζu,ζs和ζ也可以認為是接近最優的結果.

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

根據測試結果,上述時間占比不影響用戶使用感受.

5 結 論

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

后續的研究擬從如下幾個方面入手:一是探索如何結合人工智能技術自動抽取惡意代碼樣本特征并形成預期行為規范庫;二是研究適用于實時或者準實時環境的漏洞定位技術;三是研究移動智能終端、物聯網等環境下的實時可信度量和防護問題.

附錄.EBS 編寫示例

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

1.EBS 規范1:預期不能生成shell.

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

回到u[0][0]={2},查閱[48]可知,u0安全域為進程控制類系統調用,其中,編號2 對應execve,故u[0][0]={2}={execve}.再結合FOR INDEX==2:語句的參數安全策略,由于execve 的第1 個參數是字符串類型,指明了要運行的二進制文件名,因此規范1 的含義是:進程up預期不能運行/bin 目錄下的bash,sh,tcsh,csh 和dash 文件以開啟shell.

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

2.規范2:預期不能開啟非法監聽端口連接或者不能進行反向連接.

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

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

3.規范3:預期不能清空防火墻規則.

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

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

限于篇幅,這里給出3 個EBS 示例.

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