SELinux策略的等級信息分析

SELinux戰(zhàn)略的等級信息分析張謙2021.4.14Roadmap背景虛擬機(jī)系統(tǒng)戰(zhàn)略分析針對SELinux戰(zhàn)略的等級信息分析方法新想法討論：實時戰(zhàn)略分析背景平安互操作與全局訪問控制L.GongandX.Qian.Computationalissuesinsecureinteroperation.IEEETransactionsSoftwareEngineering.Vol.22,No.1,pp.43-52(1996)背景〔續(xù)〕平安互操作與全局訪問控制實現(xiàn)平安協(xié)作關(guān)鍵是訪問控制戰(zhàn)略的平安互操作，即交融各成員的本地戰(zhàn)略而構(gòu)成的全局訪問控制戰(zhàn)略所支持的成員間數(shù)據(jù)訪問必需與相關(guān)單一成員中的訪問控制戰(zhàn)略一致平安互操作的兩個原那么：自治性原那么：在單一成員中被允許的訪問必需被平安互操作所允許；平安性原那么：某單一成員中不被允許的訪問必需被平安互操作所回絕。虛擬機(jī)系統(tǒng)戰(zhàn)略分析文獻(xiàn)SandraRueda,HayawardhVijayakumar,TrentJaeger.AnalysisofVirtualMachineSystemPolicies.InProceedingsofthe14thACMsymposiumonAccesscontrolmodelsandtechnologies,P227-236,2021目的：VMpolicies&VMMpolicy→VM-systempolicy？→平安目的困難：特權(quán)VM的存在，導(dǎo)致實踐信息流不完全由VMMpolicy控制戰(zhàn)略的復(fù)雜性，規(guī)那么過多，難于確定能否符合平安目的各部分戰(zhàn)略是獨(dú)立開發(fā)的，缺乏整體規(guī)劃虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕方法簡單的想法將VMMpolicy和VMpolicies構(gòu)建一個一致的信息流圖，可以處理第一個困難然而這種方法會受限于第二個困難VM-system的特點(diǎn)不同層次的戰(zhàn)略：VMMpolicy控制VMM資源，VMpolicy控制OS資源方法概述只關(guān)懷虛擬機(jī)間通訊相關(guān)戰(zhàn)略〔VMM戰(zhàn)略和VM中互操作戰(zhàn)略〕構(gòu)建基于信息流的模型和相應(yīng)的信息流圖運(yùn)用信息流圖分析戰(zhàn)略能否滿足平安目的虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕問題定義在VM-system中，VMM實施了多級平安戰(zhàn)略，每個VM的MAC戰(zhàn)略都能夠包含一個平安級別范圍。建立一個基于信息流的分析方法來確定能否一切VM間信息流都符合平安需求虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕VM-system戰(zhàn)略模型根底假設(shè)VM-system中的vmi具有(1)一個label和(2)一個部分的MAC戰(zhàn)略這個label是一個完好性或性區(qū)間定義1VMs的完好性/性區(qū)間VM-system中的VMs都被分配了完好性/性區(qū)間integrity/confidentiality函數(shù)將VM映射到其完好性/性區(qū)間lint/hint函數(shù)分別前往區(qū)間的最低/最高完好性級別lconf/hconf函數(shù)分別前往區(qū)間的最低/最高性級別定義2第一類信息流〔默許信息流〕默許信息流表現(xiàn)為VM間的只需VMM戰(zhàn)略標(biāo)志的通訊信道虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕VM-system戰(zhàn)略模型〔續(xù)〕定義3VM可見標(biāo)志VM可見標(biāo)志是由兩個不同VM上的運(yùn)用程序分配給相互通訊譽(yù)的信道的標(biāo)志，表示為vmi.l和vmj.l定義4第二類信息流〔VM可見信息流〕VM可見信息流表現(xiàn)為不同虛擬機(jī)上的兩個運(yùn)用程序間運(yùn)用相關(guān)VM可見標(biāo)志的通訊信道定義5VM信息流圖G=(V,E)是VM信息流圖，其中V包含(1)VMM戰(zhàn)略分配給VMs的標(biāo)志和(2)VM可見標(biāo)志E包含(1)VMM戰(zhàn)略中允許的信息流和(2)VM可見標(biāo)志引起的信息流虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕驗證VM-system戰(zhàn)略符合平安目的的算法例如：一個VM-system中包含特權(quán)VM(dom0_t)，效力VM(doms_t)以及兩個用戶VM(domu_t和domv_t)。dom0_t擁有對一切VMM資源的訪問權(quán)限，同時監(jiān)控一切VM對VMM資源的訪問；doms_t運(yùn)轉(zhuǎn)了一個效力，domu_t和domv_t運(yùn)用這個效力，這個效力運(yùn)用兩個信道進(jìn)展通訊，其中domu_t運(yùn)用c2_t的標(biāo)志，domv_t運(yùn)用c1_t的標(biāo)志。虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕驗證VM-system戰(zhàn)略符合平安目的的算法〔步驟1〕構(gòu)建信息流圖V：VMM戰(zhàn)略標(biāo)志+VM可見標(biāo)志E：Type1信息流+Type2信息流虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕驗證VM-system戰(zhàn)略符合平安目的的算法〔步驟2〕定義平安目的定義平安目的信息流圖定義平安目的中的平安級別和戰(zhàn)略中標(biāo)志的映射虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕驗證VM-system戰(zhàn)略符合平安目的的算法〔步驟3〕驗證VM信息流能否符合規(guī)定SAFE、UNSAFE、AMBIGUOUS虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕驗證VM-system戰(zhàn)略符合平安目的的算法〔步驟4〕找出信息流平安的VM只作為SAFE信息流的源或目的節(jié)點(diǎn)存在的VM虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕驗證VM-system戰(zhàn)略符合平安目的的算法〔步驟5〕消除歧義信息流查看VM戰(zhàn)略來確定歧義信息流的實踐等級例如中存在兩類歧義信息流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)戰(zhàn)略分析〔續(xù)〕驗證VM-system戰(zhàn)略符合平安目的的算法〔步驟6〕驗證每個VM本身戰(zhàn)略能否符合規(guī)定定理VM-system符合某個平安需求，當(dāng)一切VM間信息流符合平安需求一切VM內(nèi)信息流符合平安需求例如中domu_t、domv_t都是單一等級，無需驗證dom0_t是可信的，假設(shè)符合平安需求doms_t可以運(yùn)用信息流分析工具分析虛擬機(jī)系統(tǒng)戰(zhàn)略分析〔續(xù)〕總結(jié)該方法首先將VM戰(zhàn)略的等級和VMM戰(zhàn)略的等級映射到平安目的的等級上，然后分析這種映射能否滿足平安目的問題根本假設(shè)VM-visible標(biāo)志VM戰(zhàn)略可驗證針對環(huán)境單一物理平臺的虛擬機(jī)針對SELinux戰(zhàn)略的等級信息分析方法針對環(huán)境虛擬域環(huán)境面對的要挾針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕問題定位背景分析虛擬域環(huán)境中實施整體的多級平安戰(zhàn)略不同物理平臺的VMM無法直接獲得其它VM的戰(zhàn)略信息VM戰(zhàn)略中不包含明顯的等級信息問題定位平安目的？性維護(hù)/MLS戰(zhàn)略VMM戰(zhàn)略等級？MLS戰(zhàn)略VM戰(zhàn)略等級？需求提取VM戰(zhàn)略的等級信息需求驗證等級信息的可信針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕提取VM戰(zhàn)略的等級信息平安戰(zhàn)略分類基于格模型的平安戰(zhàn)略MLS/Biba/LOMAC易于提取等級信息基于訪問控制矩陣的平安戰(zhàn)略TE/RBAC難于提取等級信息，運(yùn)用SELinux戰(zhàn)略為例提出等級信息分析方法驗證等級信息的可信運(yùn)用可信agent提取等級信息構(gòu)建遠(yuǎn)程證明協(xié)議證明agent和等級信息的完好性針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕方法初步設(shè)計提取的等級信息符合BLP模型的簡單平安屬性和*-平安屬性首先提取信息流，分析信息流符合要求的主客體方法步驟：針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕存在的問題及分析問題：實踐提取時無法提取出多等級緣由：實踐系統(tǒng)中信息流不能完全滿足BLP模型平安屬性可信主體與可信進(jìn)程BLP模型中*-屬性限制過嚴(yán)，將導(dǎo)致無法根據(jù)嚴(yán)厲的BLP模型來構(gòu)建可用的平安系統(tǒng)，所以提出可信主體來超越*-屬性可信進(jìn)程作為可信主體的一種實現(xiàn)方式，具有以下性質(zhì)：平安相關(guān)性可信性特權(quán)受控運(yùn)用完好性可用性正確性無干擾性針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕改良的方法設(shè)計針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕基于XSB的實現(xiàn)根本戰(zhàn)略組件如右圖根本規(guī)那么定義一致性consistent(T,R,U)授權(quán)關(guān)系auth(C,P,T1,R1,U1,T2,R2,U2)直接信息流flow_trans(T1,R1,U1,T2,R2,U2)信息流transitive_flow(T1,R1,U1,T2,R2,U2)針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕基于XSB的實現(xiàn)〔續(xù)〕新增規(guī)那么定義不含可信進(jìn)程的信息流infoflow_without_TP(T1,R1,U1,T2,R2,U2)是一個不流經(jīng)可信進(jìn)程的信息流，假設(shè)(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,U1,_,_,T3,R3,U3)，且不存在tp(T2)。針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕基于XSB的實現(xiàn)〔續(xù)〕新增規(guī)那么定義〔續(xù)〕同等級標(biāo)志型T1和T2在同一個等級上，表示為equal(T1,T2)，假設(shè)存在infoflow_without_TP(T1,_,_,T2,_,_)和infoflow_without_TP(T2,_,_,T1,_,_)。偏序等級型T1比型T2的等級高，表示為higher(T1,T2)，假設(shè)存在infoflow_without_TP(T2,_,_,T1,_,_)卻不存在infoflow_without_TP(T1,_,_,T2,_,_)。針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕基于XSB的實現(xiàn)〔續(xù)〕新增規(guī)那么定義〔續(xù)〕同等級標(biāo)志集合T2在等級m的集合內(nèi)，假設(shè)存在equal(T1,T2)或equal(T2,T1)且T1在等級m的集合內(nèi)。針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕基于XSB的實現(xiàn)〔續(xù)〕新增規(guī)那么定義〔續(xù)〕提取一切等級標(biāo)志集合針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕基于XSB的實現(xiàn)〔續(xù)〕新增規(guī)那么定義〔續(xù)〕將等級標(biāo)志集合排序首先定義level_finish(m,S)表示S集合是level(m)等級中一切標(biāo)志的集合。然后將一切的等級標(biāo)志集協(xié)作為元素建立一個新的集合level_set()。最后按照前面改良算法的第4步將等級標(biāo)志集合排序。針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕驗證等級信息的可信構(gòu)建可信agent運(yùn)用改寫過的SELinux戰(zhàn)略載入命令充任提取等級信息的代碼模塊，該命令在載入SELinux戰(zhàn)略的過程中同時進(jìn)展等級信息的提取。構(gòu)建舉證信息針對SELinux戰(zhàn)略的等級信息分析方法〔續(xù)〕驗證等級信息的可信〔續(xù)〕遠(yuǎn)程證明協(xié)議新想法討論：實時戰(zhàn)略分析觸發(fā)動機(jī)之前的戰(zhàn)略分析方法都是針對整體戰(zhàn)略進(jìn)展分析整體戰(zhàn)略包含內(nèi)容過多難以提取戰(zhàn)略的內(nèi)容難以符合某個平安目的類比可執(zhí)行文件平安性分析公用操作系統(tǒng)保證系統(tǒng)中全部的可執(zhí)行程序都是可信的，不通用，難于實現(xiàn)?？尚庞嬎愕亩攘框炞C機(jī)制只關(guān)懷已運(yùn)轉(zhuǎn)的程序能否可信，減少驗證對象，更通用更易于實現(xiàn)新想法討論：實時戰(zhàn)略分析〔續(xù)〕實時戰(zhàn)略分析想法只針對當(dāng)前時辰實踐有效戰(zhàn)略進(jìn)展平安目的