SELinux策略的等级信息分析

1、SELinux策略的等级信息分析张谦 2010.4.14Roadmap背景虚拟机系统策略分析针对SELinux策略的等级信息分析方法新想法讨论：实时策略分析背景安全互操作与全局访问控制L. Gong and X.Qian. Computational issues in secure interoperation. IEEE Transactions Software Engineering. Vol. 22, No. 1, pp. 43-52 (1996)背景（续）安全互操作与全局访问控制实现安全协作关键是访问控制策略的安全互操作，即融合各成员的本地策略而形成的全局访问控制策略所支持的成员间

2、数据访问必须与相关单一成员中的访问控制策略一致安全互操作的两个原则：自治性原则：在单一成员中被允许的访问必须被安全互操作所允许；安全性原则：某单一成员中不被允许的访问必须被安全互操作所拒绝。虚拟机系统策略分析文献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、目标：VM policies & VMM policy VM-system policy ？安全目标困难：特权VM的存在，导致实际信息流不完全由VMM policy控制策略的复杂性，规则过多，难于确定是否符合安全目标各部分策略是独立开发的，缺乏整体规划虚拟机系统策略分析（续）方法简单的想法将VMM policy和VM policies构建一个统一的信息流图，可以解决第一个困难然而这种方法会受限于第二个困难VM-system的特点不同层次的策略：VMM policy控制VMM资源，VM policy控制OS资源方法概述只关心虚拟机间通信相关策略（VMM策略和VM中互操作策略）构建基于信息

4、流的模型和相应的信息流图使用信息流图分析策略是否满足安全目标虚拟机系统策略分析（续）问题定义在VM-system中，VMM实施了多级安全策略，每个VM的MAC策略都可能包含一个安全级别范围。建立一个基于信息流的分析方法来确定是否所有VM间信息流都符合安全需求虚拟机系统策略分析（续）VM-system策略模型基础假设VM-system中的vmi具有(1)一个label和(2)一个局部的MAC策略这个label是一个完整性或机密性区间定义1 VMs的完整性/机密性区间VM-system中的VMs都被分配了完整性/机密性区间integrity/confidentiality函数将VM映射到其完整性/

5、机密性区间lint/hint函数分别返回区间的最低/最高完整性级别lconf/hconf函数分别返回区间的最低/最高机密性级别定义2 第一类信息流（默认信息流）默认信息流表现为VM间的只有VMM策略标记的通信信道虚拟机系统策略分析（续）VM-system策略模型（续）定义3 VM可见标记VM可见标记是由两个不同VM上的应用程序分配给互相通信用的信道的标记，表示为vmi.l和vmj.l定义4 第二类信息流（VM可见信息流）VM可见信息流表现为不同虚拟机上的两个应用程序间使用相关VM可见标记的通信信道定义5 VM信息流图G=(V,E)是VM信息流图，其中V包含(1)VMM策略分配给VMs的标记和(

6、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策略符合安全目标的算法（

7、步骤1）构建信息流图V：VMM策略标记+VM可见标记E：Type 1信息流+Type 2信息流虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法（步骤2）定义安全目标定义安全目标信息流图定义安全目标中的安全级别和策略中标记的映射虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法（步骤3）验证VM信息流是否符合规定SAFE、UNSAFE、AMBIGUOUS虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算法（步骤4）找出信息流安全的VM只作为SAFE信息流的源或目的节点存在的VM虚拟机系统策略分析（续）验证VM-system策略符合安全目标的算

8、法（步骤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都是单一等级，无需验证

9、dom0_t是可信的，假设符合安全需求doms_t可以使用信息流分析工具分析虚拟机系统策略分析（续）总结该方法首先将VM策略的等级和VMM策略的等级映射到安全目标的等级上，然后分析这种映射是否满足安全目标问题基本假设VM-visible标记VM策略可验证针对环境单一物理平台的虚拟机针对SELinux策略的等级信息分析方法针对环境虚拟域环境面对的威胁针对SELinux策略的等级信息分析方法（续）问题定位背景分析虚拟域环境中实施整体的多级安全策略不同物理平台的VMM无法直接获得其它VM的策略信息VM策略中不包含明显的等级信息问题定位安全目标？机密性保护/MLS策略VMM策略等级？MLS策略VM策略

10、等级？需要提取VM策略的等级信息需要验证等级信息的可信针对SELinux策略的等级信息分析方法（续）提取VM策略的等级信息安全策略分类基于格模型的安全策略MLS/Biba/LOMAC易于提取等级信息基于访问控制矩阵的安全策略TE/RBAC难于提取等级信息，使用SELinux策略为例提出等级信息分析方法验证等级信息的可信使用可信agent提取等级信息构建远程证明协议证明agent和等级信息的完整性针对SELinux策略的等级信息分析方法（续）方法初步设计提取的等级信息符合BLP模型的简单安全属性和*-安全属性首先提取信息流，分析信息流符合要求的主客体方法步骤：针对SELinux策略的等级信息分析

11、方法（续）存在的问题及分析问题：实际提取时无法提取出多等级原因：实际系统中信息流不能完全满足BLP模型安全属性可信主体与可信进程BLP模型中*-属性限制过严，将导致无法根据严格的BLP模型来构建可用的安全系统，所以提出可信主体来超越*-属性可信进程作为可信主体的一种实现方式，具有以下性质：安全相关性可信性特权受控使用完整性可用性正确性无干扰性针对SELinux策略的等级信息分析方法（续）改进的方法设计针对SELinux策略的等级信息分析方法（续）基于XSB的实现基本策略组件如右图基本规则定义一致性consistent(T,R,U) 授权关系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策略的等级信息分析方法（续）基于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,U

13、1,_,_,T3,R3,U3)，且不存在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,_,_)。针对SELinux策略的等

14、级信息分析方法（续）基于XSB的实现（续）新增规则定义（续）同等级标记集合T2在等级m的集合内，若存在equal(T1,T2)或equal(T2,T1)且T1在等级m的集合内。针对SELinux策略的等级信息分析方法（续）基于XSB的实现（续）新增规则定义（续）提取所有等级标记集合针对SELinux策略的等级信息分析方法（续）基于XSB的实现（续）新增规则定义（续）将等级标记集合排序首先定义level_finish(m,S)表示S集合是level(m)等级中所有标记的集合。然后将所有的等级标记集合作为元素建立一个新的集合level_set()。最后按照前面改进算法的第4步将等级标记集合排序。针

15、对SELinux策略的等级信息分析方法（续）验证等级信息的可信构建可信agent使用改写过的SELinux策略载入命令充当提取等级信息的代码模块，该命令在载入SELinux策略的过程中同时进行等级信息的提取。构建举证信息针对SELinux策略的等级信息分析方法（续）验证等级信息的可信（续）远程证明协议新想法讨论：实时策略分析触发动机之前的策略分析方法都是针对整体策略进行分析整体策略包含内容过多难以提取策略的内容难以符合某个安全目标类比可执行文件安全性分析专用操作系统保证系统中全部的可执行程序都是可信的，不通用，难于实现。可信计算的度量验证机制只关心已运行的程序是否可信，减少验证对象，更通用更易于实现新想法讨论：实时策略分析（续）实时策略分析想法只针对当前时刻实际有效策