SELinux策略的等级信息分析

SELinux策略的等级信息分析张谦2010.4.14Roadmap背景虚拟机系统策略分析针对SELinux策略的等级信息分析方法新想法讨论：实时策略分析背景安全互操作与全局访问控制L.GongandX.Qian.Computationalissuesinsecureinteroperation.IEEETransactionsSoftwareEngineering.Vol.22,No.1,pp.43-52(1996)背景（续）安全互操作与全局访问控制实现安全协作关键是访问控制策略的安全互操作，即融合各成员的本地策略而形成的全局访问控制策略所支持的成员间数据访问必须与相关单一成员中的访问控制策略一致安全互操作的两个原则：自治性原则：在单一成员中被允许的访问必须被安全互操作所允许；安全性原则：某单一成员中不被允许的访问必须被安全互操作所拒绝。虚拟机系统策略分析文献SandraRueda,HayawardhVijayakumar,TrentJaeger.AnalysisofVirtualMachineSystemPolicies.InProceedingsofthe14thACMsymposiumonAccesscontrolmodelsandtechnologies,P227-236,2009目标：VMpolicies&VMMpolicy→VM-systempolicy？→安全目标困难：特权VM的存在，导致实际信息流不完全由VMMpolicy控制策略的复杂性，规则过多，难于确定是否符合安全目标各部分策略是独立开发的，缺乏整体规划虚拟机系统策略分析（续）方法简单的想法将VMMpolicy和VMpolicies构建一个统一的信息流图，可以解决第一个困难然而这种方法会受限于第二个困难VM-system的特点不同层次的策略：VMMpolicy控制VMM资源，VMpolicy控制OS资源方法概述只关心虚拟机间通信相关策略（VMM策略和VM中互操作策略）构建基于信息流的模型和相应的信息流图使用信息流图分析策略是否满足安全目标虚拟机系统策略分析（续）问题定义在VM-system中，VMM实施了多级安全策略，每个VM的MAC策略都可能包含一个安全级别范围。建立一个基于信息流的分析方法来确定是否所有VM间信息流都符合安全需求虚拟机系统策略分析（续）VM-system策略模型基础假设VM-system中的vmi具有(1)一个label和(2)一个局部的MAC策略这个label是一个完整性或机密性区间定义1VMs的完整性/机密性区间VM-system中的VMs都被分配了完整性/机密性区间integrity/confidentiality函数将VM映射到其完整性/机密性区间lint/hint函数分别返回区间的最低/最高完整性级别lconf/hconf函数分别返回区间的最低/最高机密性级别定义2第一类信息流（默认信息流）默认信息流表现为VM间的只有VMM策略标记的通信信道虚拟机系统策略分析（续）VM-system策略模型（续）定义3VM可见标记VM可见标记是由两个不同VM上的应用程序分配给互相通信用的信道的标记，表示为vmi.l和vmj.l定义4第二类信息流（VM可见信息流）VM可见信息流表现为不同虚拟机上的两个应用程序间使用相关VM可见标记的通信信道定义5VM信息流图G=(V,E)是VM信息流图，其中V包含(1)VMM策略分配给VMs的标记和(2)VM可见标记E包含(1)VMM策略中允许的信息流和(2)VM可见标记引起的信息流虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法示例：一个VM-system中包含特权VM(dom0_t)，服务VM(doms_t)以及两个用户VM(domu_t和domv_t)。dom0_t拥有对所有VMM资源的访问权限，同时监控所有VM对VMM资源的访问；doms_t运行了一个服务，domu_t和domv_t使用这个服务，这个服务使用两个信道进行通信，其中domu_t使用c2_t的标记，domv_t使用c1_t的标记。虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法（步骤1）构建信息流图V：VMM策略标记+VM可见标记E：Type1信息流+Type2信息流虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法（步骤2）定义安全目标定义安全目标信息流图定义安全目标中的安全级别和策略中标记的映射虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法（步骤3）验证VM信息流是否符合规定SAFE、UNSAFE、AMBIGUOUS虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法（步骤4）找出信息流安全的VM只作为SAFE信息流的源或目的节点存在的VM虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法（步骤5）消除歧义信息流查看VM策略来确定歧义信息流的实际等级示例中存在两类歧义信息流dom0_t→doms_t：由于dom0可信，相信dom0不会泄密，所以这类信息流是SAFE的doms_t→dom0_t：这类信息流是用于申请VMM资源的，dom0中资源管理的进程标记为priv，高于doms_t的标记，所以这类信息流也是SAFE的虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法（步骤6）验证每个VM本身策略是否符合规定定理VM-system符合某个安全需求，当所有VM间信息流符合安全需求所有VM内信息流符合安全需求示例中domu_t、domv_t都是单一等级，无需验证dom0_t是可信的，假设符合安全需求doms_t可以使用信息流分析工具分析虚拟机系统策略分析（续）总结该方法首先将VM策略的等级和VMM策略的等级映射到安全目标的等级上，然后分析这种映射是否满足安全目标问题基本假设VM-visible标记VM策略可验证针对环境单一物理平台的虚拟机针对SELinux策略的等级信息分析方法针对环境虚拟域环境面对的威胁绝密虚拟机B虚拟机A机密秘密程序A1程序A2程序B1程序B2虚拟域针对SELinux策略的等级信息分析方法（续）问题定位背景分析虚拟域环境中实施整体的多级安全策略不同物理平台的VMM无法直接获得其它VM的策略信息VM策略中不包含明显的等级信息问题定位安全目标？机密性保护/MLS策略VMM策略等级？MLS策略VM策略等级？需要提取VM策略的等级信息需要验证等级信息的可信针对SELinux策略的等级信息分析方法（续）提取VM策略的等级信息安全策略分类基于格模型的安全策略MLS/Biba/LOMAC易于提取等级信息基于访问控制矩阵的安全策略TE/RBAC难于提取等级信息，使用SELinux策略为例提出等级信息分析方法验证等级信息的可信使用可信agent提取等级信息构建远程证明协议证明agent和等级信息的完整性针对SELinux策略的等级信息分析方法（续）方法初步设计提取的等级信息符合BLP模型的简单安全属性和*-安全属性首先提取信息流，分析信息流符合要求的主客体方法步骤：针对SELinux策略的等级信息分析方法（续）存在的问题及分析问题：实际提取时无法提取出多等级原因：实际系统中信息流不能完全满足BLP模型安全属性可信主体与可信进程BLP模型中*-属性限制过严，将导致无法根据严格的BLP模型来构建可用的安全系统，所以提出可信主体来超越*-属性可信进程作为可信主体的一种实现方式，具有以下性质：安全相关性可信性特权受控使用完整性可用性正确性无干扰性针对SELinux策略的等级信息分析方法（续）改进的方法设计针对SELinux策略的等级信息分析方法（续）基于XSB的实现基本策略组件如右图基本规则定义一致性consistent(T,R,U)授权关系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策略的等级信息分析方法（续）基于XSB的实现（续）新增规则定义不含可信进程的信息流infoflow_without_TP(T1,R1,U1,T2,R2,U2)是一个不流经可信进程的信息流，若(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)。tableinfoflow_without_TP/6.infoflow_without_TP(T1,R1,U1,T2,R2,U2):-flow_trans(T1,R1,U1,_,_,T2,R2,U2),not(tp(T1)),not(tp(T2)).infoflow_without_TP(T1,R1,U1,T2,R2,U2):-infoflow_without_TP(T1,R1,U1,T3,R3,U3),flow_trans(T3,R3,U3,_,_,T2,R2,U2),not(tp(T2)).针对SELinux策略的等级信息分析方法（续）基于XSB的实现（续）新增规则定义（续）同等级标记型T1和T2在同一个等级上，表示为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,_,_)。equal(T1,T2):-infoflow_without_TP(T1,_,_,T2,_,_),infoflow_without_TP(T2,_,_,T1,_,_).higher(T1,T2):-not(infoflow_without_TP(T1,_,_,T2,_,_)),infoflow_without_TP(T2,_,_,T1,_,_).针对SELinux策略的等级信息分析方法（续）基于XSB的实现（续）新增规则定义（续）同等级标记集合T2在等级m的集合内，若存在equal(T1,T2)或equal(T2,T1)且T1在等级m的集合内。tablelevel/2.level(m,[T2|S]):-level(m,S),member(T1,S),equal(T1,T2).level(m,[T2|S]):-level(m,S),member(T1,S),equal(T2,T1).针对SELinux策略的等级信息分析方法（续）基于XSB的实现（续）新增规则定义（续）提取所有等级标记集合level(1,usr_t,tset).tablelevel/2.level(m,[T2|S],Tset):-level(m,S,[T2|Tset]),member(T1,S),equal(T1,T2).level(m,[T2|S],Tset):-level(m,S,[T2|Tset]),member(T1,S),equal(T2,T1).level(m+1,[T],Tset):-not(level(m,[T1|S],[T1|[T|Tset]])).针对SELinux策略的等级信息分析方法（续）基于XSB的实现（续）新增规则定义（续）将等级标记集合排序首先定义l