基于有色Petri网SELinux安全策略自动化分析.doc

基于有色Petri网SELinux安全策略自动化分析 　　【 摘 要 】 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网定义为一个九元组，具体组成元素物理含义参表3所示。 　　其间，两个类型库所之间一般经由权限库所及两