SELinux策略的等級信息分析教材

1、SELinux策略的等級信息分析張謙 2010.4.14Roadmap背景虛擬機(jī)系統(tǒng)策略分析針對SELinux策略的等級信息分析方法新想法討論：實(shí)時(shí)策略分析背景安全互操作與全局訪問控制L. Gong and X.Qian. Computational issues in secure interoperation. IEEE Transactions Software Engineering. Vol. 22, No. 1, pp. 43-52 (1996)背景（續(xù)）安全互操作與全局訪問控制實(shí)現(xiàn)安全協(xié)作關(guān)鍵是訪問控制策略的安全互操作，即融合各成員的本地策略而形成的全局訪問控制策略所支持的成員間

2、數(shù)據(jù)訪問必須與相關(guān)單一成員中的訪問控制策略一致安全互操作的兩個(gè)原則：自治性原則：在單一成員中被允許的訪問必須被安全互操作所允許；安全性原則：某單一成員中不被允許的訪問必須被安全互操作所拒絕。虛擬機(jī)系統(tǒng)策略分析文獻(xiàn)Sandra Rueda, Hayawardh Vijayakumar, Trent Jaeger. Analysis of Virtual Machine System Policies. In Proceedings of the 14th ACM symposium on Access control models and technologies, P227-236, 2009

3、目標(biāo)：VM policies & VMM policy VM-system policy ？安全目標(biāo)困難：特權(quán)VM的存在，導(dǎo)致實(shí)際信息流不完全由VMM policy控制策略的復(fù)雜性，規(guī)則過多，難于確定是否符合安全目標(biāo)各部分策略是獨(dú)立開發(fā)的，缺乏整體規(guī)劃虛擬機(jī)系統(tǒng)策略分析（續(xù)）方法簡單的想法將VMM policy和VM policies構(gòu)建一個(gè)統(tǒng)一的信息流圖，可以解決第一個(gè)困難然而這種方法會受限于第二個(gè)困難VM-system的特點(diǎn)不同層次的策略：VMM policy控制VMM資源，VM policy控制OS資源方法概述只關(guān)心虛擬機(jī)間通信相關(guān)策略（VMM策略和VM中互操作策略）構(gòu)建基于信息

4、流的模型和相應(yīng)的信息流圖使用信息流圖分析策略是否滿足安全目標(biāo)虛擬機(jī)系統(tǒng)策略分析（續(xù)）問題定義在VM-system中，VMM實(shí)施了多級安全策略，每個(gè)VM的MAC策略都可能包含一個(gè)安全級別范圍。建立一個(gè)基于信息流的分析方法來確定是否所有VM間信息流都符合安全需求虛擬機(jī)系統(tǒng)策略分析（續(xù)）VM-system策略模型基礎(chǔ)假設(shè)VM-system中的vmi具有(1)一個(gè)label和(2)一個(gè)局部的MAC策略這個(gè)label是一個(gè)完整性或機(jī)密性區(qū)間定義1 VMs的完整性/機(jī)密性區(qū)間VM-system中的VMs都被分配了完整性/機(jī)密性區(qū)間integrity/confidentiality函數(shù)將VM映射到其完整性/

5、機(jī)密性區(qū)間lint/hint函數(shù)分別返回區(qū)間的最低/最高完整性級別lconf/hconf函數(shù)分別返回區(qū)間的最低/最高機(jī)密性級別定義2 第一類信息流（默認(rèn)信息流）默認(rèn)信息流表現(xiàn)為VM間的只有VMM策略標(biāo)記的通信信道虛擬機(jī)系統(tǒng)策略分析（續(xù)）VM-system策略模型（續(xù)）定義3 VM可見標(biāo)記VM可見標(biāo)記是由兩個(gè)不同VM上的應(yīng)用程序分配給互相通信用的信道的標(biāo)記，表示為vmi.l和vmj.l定義4 第二類信息流（VM可見信息流）VM可見信息流表現(xiàn)為不同虛擬機(jī)上的兩個(gè)應(yīng)用程序間使用相關(guān)VM可見標(biāo)記的通信信道定義5 VM信息流圖G=(V,E)是VM信息流圖，其中V包含(1)VMM策略分配給VMs的標(biāo)記和(

6、2)VM可見標(biāo)記E包含(1)VMM策略中允許的信息流和(2)VM可見標(biāo)記引起的信息流虛擬機(jī)系統(tǒng)策略分析（續(xù)）驗(yàn)證VM-system策略符合安全目標(biāo)的算法示例：一個(gè)VM-system中包含特權(quán)VM(dom0_t)，服務(wù)VM(doms_t)以及兩個(gè)用戶VM(domu_t和domv_t)。dom0_t擁有對所有VMM資源的訪問權(quán)限，同時(shí)監(jiān)控所有VM對VMM資源的訪問；doms_t運(yùn)行了一個(gè)服務(wù)，domu_t和domv_t使用這個(gè)服務(wù)，這個(gè)服務(wù)使用兩個(gè)信道進(jìn)行通信，其中domu_t使用c2_t的標(biāo)記，domv_t使用c1_t的標(biāo)記。虛擬機(jī)系統(tǒng)策略分析（續(xù)）驗(yàn)證VM-system策略符合安全目標(biāo)的算法（

7、步驟1）構(gòu)建信息流圖V：VMM策略標(biāo)記+VM可見標(biāo)記E：Type 1信息流+Type 2信息流虛擬機(jī)系統(tǒng)策略分析（續(xù)）驗(yàn)證VM-system策略符合安全目標(biāo)的算法（步驟2）定義安全目標(biāo)定義安全目標(biāo)信息流圖定義安全目標(biāo)中的安全級別和策略中標(biāo)記的映射虛擬機(jī)系統(tǒng)策略分析（續(xù)）驗(yàn)證VM-system策略符合安全目標(biāo)的算法（步驟3）驗(yàn)證VM信息流是否符合規(guī)定SAFE、UNSAFE、AMBIGUOUS虛擬機(jī)系統(tǒng)策略分析（續(xù)）驗(yàn)證VM-system策略符合安全目標(biāo)的算法（步驟4）找出信息流安全的VM只作為SAFE信息流的源或目的節(jié)點(diǎn)存在的VM虛擬機(jī)系統(tǒng)策略分析（續(xù)）驗(yàn)證VM-system策略符合安全目標(biāo)的算

8、法（步驟5）消除歧義信息流查看VM策略來確定歧義信息流的實(shí)際等級示例中存在兩類歧義信息流dom0_t doms_t：由于dom0可信，相信dom0不會泄密，所以這類信息流是SAFE的doms_t dom0_t：這類信息流是用于申請VMM資源的，dom0中資源管理的進(jìn)程標(biāo)記為priv，高于doms_t的標(biāo)記，所以這類信息流也是SAFE的虛擬機(jī)系統(tǒng)策略分析（續(xù)）驗(yàn)證VM-system策略符合安全目標(biāo)的算法（步驟6）驗(yàn)證每個(gè)VM本身策略是否符合規(guī)定定理 VM-system符合某個(gè)安全需求，當(dāng)所有VM間信息流符合安全需求所有VM內(nèi)信息流符合安全需求示例中domu_t、domv_t都是單一等級，無需驗(yàn)證

9、dom0_t是可信的，假設(shè)符合安全需求doms_t可以使用信息流分析工具分析虛擬機(jī)系統(tǒng)策略分析（續(xù)）總結(jié)該方法首先將VM策略的等級和VMM策略的等級映射到安全目標(biāo)的等級上，然后分析這種映射是否滿足安全目標(biāo)問題基本假設(shè)VM-visible標(biāo)記VM策略可驗(yàn)證針對環(huán)境單一物理平臺的虛擬機(jī)針對SELinux策略的等級信息分析方法針對環(huán)境虛擬域環(huán)境面對的威脅針對SELinux策略的等級信息分析方法（續(xù)）問題定位背景分析虛擬域環(huán)境中實(shí)施整體的多級安全策略不同物理平臺的VMM無法直接獲得其它VM的策略信息VM策略中不包含明顯的等級信息問題定位安全目標(biāo)？機(jī)密性保護(hù)/MLS策略VMM策略等級？MLS策略VM策略

10、等級？需要提取VM策略的等級信息需要驗(yàn)證等級信息的可信針對SELinux策略的等級信息分析方法（續(xù)）提取VM策略的等級信息安全策略分類基于格模型的安全策略MLS/Biba/LOMAC易于提取等級信息基于訪問控制矩陣的安全策略TE/RBAC難于提取等級信息，使用SELinux策略為例提出等級信息分析方法驗(yàn)證等級信息的可信使用可信agent提取等級信息構(gòu)建遠(yuǎn)程證明協(xié)議證明agent和等級信息的完整性針對SELinux策略的等級信息分析方法（續(xù)）方法初步設(shè)計(jì)提取的等級信息符合BLP模型的簡單安全屬性和*-安全屬性首先提取信息流，分析信息流符合要求的主客體方法步驟：針對SELinux策略的等級信息分析

11、方法（續(xù)）存在的問題及分析問題：實(shí)際提取時(shí)無法提取出多等級原因：實(shí)際系統(tǒng)中信息流不能完全滿足BLP模型安全屬性可信主體與可信進(jìn)程BLP模型中*-屬性限制過嚴(yán)，將導(dǎo)致無法根據(jù)嚴(yán)格的BLP模型來構(gòu)建可用的安全系統(tǒng)，所以提出可信主體來超越*-屬性可信進(jìn)程作為可信主體的一種實(shí)現(xiàn)方式，具有以下性質(zhì)：安全相關(guān)性可信性特權(quán)受控使用完整性可用性正確性無干擾性針對SELinux策略的等級信息分析方法（續(xù)）改進(jìn)的方法設(shè)計(jì)針對SELinux策略的等級信息分析方法（續(xù)）基于XSB的實(shí)現(xiàn)基本策略組件如右圖基本規(guī)則定義一致性consistent(T,R,U) 授權(quán)關(guān)系auth(C,P,T1,R1,U1,T2,R2,U2)

12、直接信息流flow_trans(T1,R1,U1,T2,R2,U2)信息流transitive_flow(T1,R1,U1,T2,R2,U2)針對SELinux策略的等級信息分析方法（續(xù)）基于XSB的實(shí)現(xiàn)（續(xù)）新增規(guī)則定義不含可信進(jìn)程的信息流infoflow_without_TP(T1,R1,U1,T2,R2,U2)是一個(gè)不流經(jīng)可信進(jìn)程的信息流，若(1)存在flow_trans(T1,R1,U1,_,_,T2,R2,U2)，且不存在tp(T1)和tp(T2)；或者(2)存在flow_trans(T3,R3,U3,_,_,T2,R2,U2)和infoflow_without_TP(T1,R1,U

13、1,_,_,T3,R3,U3)，且不存在tp(T2)。針對SELinux策略的等級信息分析方法（續(xù)）基于XSB的實(shí)現(xiàn)（續(xù)）新增規(guī)則定義（續(xù)）同等級標(biāo)記型T1和T2在同一個(gè)等級上，表示為equal(T1,T2)，若存在infoflow_without_TP(T1,_,_,T2,_,_)和infoflow_without_TP(T2,_,_,T1,_,_)。偏序等級型T1比型T2的等級高，表示為higher(T1,T2)，若存在infoflow_without_TP(T2,_,_,T1,_,_)卻不存在infoflow_without_TP(T1,_,_,T2,_,_)。針對SELinux策略的等

14、級信息分析方法（續(xù)）基于XSB的實(shí)現(xiàn)（續(xù)）新增規(guī)則定義（續(xù)）同等級標(biāo)記集合T2在等級m的集合內(nèi)，若存在equal(T1,T2)或equal(T2,T1)且T1在等級m的集合內(nèi)。針對SELinux策略的等級信息分析方法（續(xù)）基于XSB的實(shí)現(xiàn)（續(xù)）新增規(guī)則定義（續(xù)）提取所有等級標(biāo)記集合針對SELinux策略的等級信息分析方法（續(xù)）基于XSB的實(shí)現(xiàn)（續(xù)）新增規(guī)則定義（續(xù)）將等級標(biāo)記集合排序首先定義level_finish(m,S)表示S集合是level(m)等級中所有標(biāo)記的集合。然后將所有的等級標(biāo)記集合作為元素建立一個(gè)新的集合level_set()。最后按照前面改進(jìn)算法的第4步將等級標(biāo)記集合排序。針

15、對SELinux策略的等級信息分析方法（續(xù)）驗(yàn)證等級信息的可信構(gòu)建可信agent使用改寫過的SELinux策略載入命令充當(dāng)提取等級信息的代碼模塊，該命令在載入SELinux策略的過程中同時(shí)進(jìn)行等級信息的提取。構(gòu)建舉證信息針對SELinux策略的等級信息分析方法（續(xù)）驗(yàn)證等級信息的可信（續(xù)）遠(yuǎn)程證明協(xié)議新想法討論：實(shí)時(shí)策略分析觸發(fā)動機(jī)之前的策略分析方法都是針對整體策略進(jìn)行分析整體策略包含內(nèi)容過多難以提取策略的內(nèi)容難以符合某個(gè)安全目標(biāo)類比可執(zhí)行文件安全性分析專用操作系統(tǒng)保證系統(tǒng)中全部的可執(zhí)行程序都是可信的，不通用，難于實(shí)現(xiàn)。可信計(jì)算的度量驗(yàn)證機(jī)制只關(guān)心已運(yùn)行的程序是否可信，減少驗(yàn)證對象，更通用更易于實(shí)現(xiàn)新想法討論：實(shí)時(shí)策略分析（續(xù)）實(shí)時(shí)策略分析想法只針對當(dāng)前時(shí)刻實(shí)際有效策