【 摘 要 】 selinux是嵌入到linux内核中并得到推广应用的安全增强模块。由于其安全策略配置复杂且工作量较大，故而研究相关的安全策略辅助配置手段及selinux安全策略的自动化分析方法与技术很有必要。本文基于有色petri网建立了selinux安全策略的自动化分析模型，给出了原型实现和测试结果。相关结果表明，有色petri网分析方法和对应原型能较好地完成selinux安全策略的有效性分析，并可实现带有中间过滤类型的信息流查询且更加方便简洁。
　　【 关键词 】 selinux；安全策略；有色petri网；自动化分析
　　1 引言
　　信息技术的发展极大地促进了科技的发展，同时也带来了日益严重的信息安全问题。操作系统作为计算机系统的底层软件，其安全直接影响着整个信息系统的安全。换言之，保障信息安全必须以操作系统的安全为前提条件。linux是主流实用操作系统中的杰出代表，其安全实现机制也一直是人们研究的重点。selinux作为linux内核中的典型安全增强模块，其安全加固效果主要取决于相关安全策略的正确配置。但限于安全策略配置工作的规模复杂性，手工分析和配置太过耗费时间精力。开展selinux安全策略的辅助配置手段及自动化分析方法与技术的研究非常必要且意义重大。本文基于有色petri网建立了selinux安全策略的自动化分析模型，并用c语言编程实现了相应的原型系统，同时还给出了测试验证和分析结果。
　　2 selinux安全策略及有色petri网分析法
　　2.1 selinux安全策略及现有分析方法
　　selinux是美国国家安全局关于强制访问控制的实现机制，其支持te、rbac和mls（可选）等三种安全模型。selinux安全策略的基本元素参表1所示。
　　allow规则是selinux安全策略描述主客体访问控制关系的基本语句类型。其一般形式为：allow {type_set} {type_set} ：{class_set} {permission_name}。其中，allow是关键字，“：”是约定使用的分隔符，第一个type_set和第二个type_set分别代表源类型和目标类型，class_set用于指明客体的类别，permission_set则指明了源类型关于目标类型的操作权限。allow规则的含义是：允许源类型对目标类型的特定类别进行指定操作方式的访问。
　　当前对selinux安全策略的分析方法主要有访问控制空间分析法、信息流分析法和基于有色petri网的分析法。访问控制空间分析法由jaeger在文献[1]中首先提出，该方法基于安全策略配置完成各主体访问控制空间的划分来实现安全策略的自动化分析。j. guttman在文献[2]中，将主客体和信息流定义为不同的集合对象和相互之间的状态的转化，给出了信息流分析法的基本方案。文献[3-5]则综合运用访问控制空间分析法和信息流分析法设计和实现了selinux安全策略的有效性分析和完整性分析。必须指出，访问控制空间分析法的关注焦点在于单个主客体的访问控制规定是否存在冲突或不一致。对于多个相关主客体的复杂访问控制关系（如包含中间类型或过滤类型的访问控制关系）的分析或者从类型级别来检查安全策略配置是否违背安全目标的情形，则需要采用通配符且须经多次单一主客体访问控制关系的分析方可完成。传统的信息流分析法一般需要对信息流进行完整的描述，对于指定较少关键中间类型的访问控制关系的分析而言比较繁琐。基于有色petri网的安全策略分析方法本质上是一种信息流分析法，文献[6][7]采用有色petri网并分别基于xml文档和cpn tools中间文档对selinux安全策略进行了描述和分析。本文试图完成selinux安全策略基本元素的自动提取，并在此基础上实现有色petri网的自动化构造与分析，以改善和提高相关方法的自动化程度。
　　2.2 安全分析目标及其描述
　　安全策略配置关键在于应满足安全需求和安全设计目标，所以selinux安全策略分析应着眼于检查当前安全策略配置是否满足安全设计目标，也即所谓的有效性分析。安全设计目标可通过一组查询语句来具体描述，并提交给安全策略分析系统进行验证和确认。为方便和规范描述，并可基于巴科斯范式来形式化查询语句。如表2所示。
　　2.3 有色petri网分析模型
　　有色petri网区别于其它petri网的最主要区别在于其引入了颜色集的定义[8]，而颜色集把petri网中出现的数据划分成若干不同的类型。为方便selinux安全策略的自动化分析，可将有色petri网定义为一个九元组<∑，p，t，f，nf，cf，gf，fe，ie>，具体组

元素物理含义参表3所示。
　　其间，两个类型库所之间一般经由权限库所及两个变迁相连接，表示前一个类型库所对后一个类型库所拥有对应权限库所所代表的访问权限。显然，这与selinux安全策略配置中的allow语句完全一致。为此，基于有色petri网的selinux安全策略分析模型的构建将主要基于allow语句的分析和处理来完成。
　　令牌是库所中的动态对象，可以从一个库所移动到另一个库所。当且仅当库所中的令牌值和有向弧上的描述一致并通过变迁上的警戒函数测试时，就可以发生一次变迁。在查询分析过程中，令牌将记录从查询语句的源类型所对应的库所到当前库所的信息流路径上（不妨简称为查询信息流路径）的所有类型信息、权限信息以及查询相关的其它信息，故可用一个四元组加以表示。其中，bool是一个布尔值，用于记录当前库所中类型是否为查询语句中类型的判断结果；querytype是一个字符串，用于记录查询分析过程中最近遇到的查询语句中的分类标记（详参3.3）；typelist是一个字符串链表，用于记录查询信息流路径上的所有类型组成的类型列表；permlist也是一个字符串链表，但用来记录查询信息流路径上的所有权限组成的权限列表。 伴随查询分析过程的向前推进，查询分析路径上各库所中的令牌值应及时进行调整。具体而言，首先把当前库所中的令牌值赋值给其所有后继库所的令牌，然后针对不同的后继库所分别对其令牌值做相应的调整。
　　3 原型设计与实现
　　3.1 总体设计
　　根据selinux安全策略配置文件和上述模型，可实现安全设计目标的有效性分析。具体过程如图1所示。
　　3.2 安全策略要素提取
　　安全策略要素提取模块直接针对的处理对象是selinux安全策略配置文件，从中提取包括类型、属性、类别、权限以及访问控制规则（主要是allow语句）等在内的基本元素。其处理步骤有几个。
　　（1）分析安全策略配置文件，并将class、permission、type、attribute、allow、bool、typeattribute的声明语句（行）保存到临时文件。其间，基于接口的声明语句应根据相关接口定义替换为实际对应的策略语句后再进行保存。
　　（2）针对步骤1生成的临时文件，就类型、属性、类别、权限等要素分别提取处理，并保存到相应结构体中。特别地，allow语句需分解和提取出源类型、目标类型及权限类型，而根据typeattribute语句可建立type和attribute之间的双向映射。
　　（3）针对步骤2得到的allow语句处理结果，依次检查相应allow规则的源类型和目标类型，将所有allow规则的源类型和目标类型转换为type，并过滤掉无效的allow语句。进一步讲，若allow规则的源类型（或目标类型）为attribute，则基于attribute和type之间的双向映射关系将对应规则转换为相应type源类型（或目标类型）的allow规则。同时，把拥有既非type也非attribute的源类型或目标类型的allow规则抛弃和删除。
　　3.3 有色petri网构建
　　基于allow规则语句构建selinux安全策略有色petri网模型的基本方法如下：
　　（1）将allow规则的源类型和目标类型转化为有色petri网中的类型库所；
　　（2）将allow规则的权限转化为有色petri网中的权限库所；
　　（3）根据allow规则在类型库所和权限库所之间设立access变迁和将它们连接起来。
　　图2所示为两条allow规则示例及其转化得到的有色petri网结果。
　　allow student_t accessrecord_t process{transition}；
　　allow accessrecord_t courserecord_t：file{ write }；
　　为利用前述有色petri网模型验证selinux安全策略配置关于安全设计目标的有效性，需提示安全管理人员输入一系列查询语句，而每次查询处理也需将对应查询语句转化和插入到基于selinux安全策略配置的allow规则集生成的有色petri网分析模型中。具体而言，首先从查询语句中提取出源类型、目标类型、过滤类型、直接/间接信息流标记、读/写信息流访问方式，然后在有色petri网分析模型中建立源类型、目标类型以及过滤类型所对应的类型库所。为方便后续的查询处理，这里对类型库所的标记进行了更为细致的分类处理。譬如，对于如下的查询语句：teacher_t：（wl，+，！（collegeadmin_t））： courserecord_t
　　在转化和插入分析模型时，可将teacher_t、courserecord_t

t、collegeadmin_t所在库所的分类标记分别设置为sourcetype、targettype和notlisttype。同时，将分析模型中非上述情况的类型库所的分类标记设置为ordinarytype，而将权限库所的分类标记设置为permissiontype。
　　3.4 有色petri网查询处理
　　在建立和生成selinux安全策略有色petri网模型的基础上，初始化设定sourcetype所在库所的令牌值，就可启动查询处理过程。
　　查询处理的实现过程主要涉及由即将处理的相关库所构成的一个库所队列的维护操作。其基本流程如下所述：
　　其间，库所v的令牌值更新和设置操作尤为关键，详细更新方案参表4所示。
　　针对以上selinux安全策略分析方法，基于c语言对进行了实现，文献[6] [7]分别采用cpn tools和中间xml文档进行了分析。本文采用c语言模拟cpn的执行，自动化地将访问控制关系及查询语句转化成cpn，并自动执行变迁，从而实现了selinux的安全策略自动化分析。
　　4 原型测试及结果分析
　　本文基于一个学生-教师系统selinux应用实例对实验原型进行了测试验证和分析。
　　4.1 测试用例
　　selinux应用实例中主要提供了学生选课及教师评分两种服务操作，系统中的主体类型有三种，学生类型（student_t）、教师类型（teacher_t）和管理员类型（collegeadmin_t），客体类型分为学生作业文件类型（coursework_t）、选课记录文件类型（courserecord_t）、课程资源类型（coursesourse_t）、初始成绩类型（coursepremark_t）和最终成绩类型（coursemark_t），教师提交初始成绩，由管理员根据初始成绩得出最终成绩。学生具有读取课程资源、读取最终成绩、写入选课记录以及写入作业文件的权限；教师的权限有读取选课记录、读取学生作业、写入课程资源、写入初始成绩的权限；管理员有读取选课记录、读取课程资源、读取学生作业的、读取始成绩、写入最终成绩的权限。 4.2 测试验证
　　根据3.2节方法提取出allow语句，选取了两个比较典型的配置语句验证，在配置语句中有allow student_t accessrecord_t：process transition； allow accessrecord_t courserecord_t：file { write }；表示student_t能通过accessrecord_t来最终访问courserecord_t，采用“正”描述表示为必须有一条从student_t到courserecord_t的信息流；在设计用例时，不允许teacher_t直接对courserecord_t进行访问，只能通过collegeadmin_t对courserecord_t进行访问，采用“负”描述查找teacher_t对courserecord_t进行访问且没经过collegeadmin_t的非法信息流。验证结果如表5所示。
　　4.3 结果分析
　　在4.2节的验证中给出了两条比较典型的验证语句，分别从查找合法非法信息流方面对用例中的安全设计目标进行了验证，结果发现符合了“学生能写课程记录”和“教师不能直接写分数记录”的安全设计目标，另外对其他的学生、教师、课程记录、作业记录、分数记录直接的访问控制关系设计目标也进行了验证，由于篇幅关系不再列出，它们之间的访问关系也符合用例的设计目标，以上分析说明分析工具能对安全策略进行有效性分析，同时验证了策略配置的正确性。
　　5 结束语
　　本文基于有色petri网设计和实现了selinux安全策略的自动化分析原型，解决了验证selinux安全策略配置正确性的问题。原型测试结果表明，有色petri网分析模型可有效描述selinux安全策略中的访问控制关系，而对应于安全设计目标描述的方便规范的查询语句通过引入带有中间过滤类型的信息流可支持较为复杂的访问控制关系的分析处理。总体上来讲，相关分析方法和原型可满足安全策略有效性分析基本要求，但相关实现细节需要进一步优化和改进。
　　参考文献
　　[1] t. jaeger， x. zhang， and a. edwards， policy management using access control spaces， acm transations on information and system security. 2003， 6（3）：327-364，
　　[2] j. guttman， a. herzog， and j. ramsdell， “information flow in operating systems： eager formal methods，” in workshop on issues in the theory of security （wits）， 2003.
　　[3] gaoshou zhai， tong wu， jing bai， tao guo and tianyou li， algorithms for automatic analysis of selinux security policy， international journal of security

and its applications， 2013，vol.7， no.1， pp.71-84.
　　[4] jing bai， gaoshou zhai， study on analysis for selinux security policy， proceedings of 2012 international conference on systems and informatics （icsai 2012）， pp.1231-1235.
　　[5] gaoshou zhai， wenlin ma， minli tian， na yang， chengyu liu， hengsheng yang， design and implementation of a tool for analyzing selinux secure policy， icis 2009， november 24-26， 2009 seoul， korea， pp. 446-451.
　　[6] chen yi-ming， kao yung-wei， “information flow query and verification for security policy of security-enhanced linux，” proceedings of the 1st international workshop on security （iwsec 2006） kyoto， japan， oct 23-24， 2006， pp. 389-404.
　　[7] ahn gail-joon， xu wenjuan， zhang xinwen， “systematic policy analysis for high-assurance services in selinux，” proceedings of the ieee international workshop on policies for distributed systems and networks palisades， ny， jun 02-04， 2008， pp. 3-10.
　　[8] 袁崇义. petri网原理与应用.北京电子工业出版社， 2005.3.
　　项目基金：
　　中央高校基本科研业务费专项资金资助（课题编号：2009jbm019）。
　　作者简介：
　　郭涛（1989-），男，河南林州人，硕士研究生；主要研究方向：安全操作系统。
　　翟高寿（1971-），男，山西平定人，副教授；主要研究方向：操作系统与信息安全。