基于有色Petri网的SELinux安全策略分析

发布时间：2018-04-16 11:02

本文选题：安全操作系统 + SELinux　；参考：《北京交通大学》2014年硕士论文

【摘要】：操作系统是计算机资源的直接管理者,位于整个信息系统的最底层,其安全问题是信息安全的核心问题。SELinux是Linux系统的安全增强模块,能够有效实施强制访问机制,保证系统安全。安全策略配置是SELinux安全保护实施的关键所在,但由于安全策略复杂繁多、管理困难,一定程度上制约了SELinux的推广应用。因此,研究构建SELinux安全策略自动化分析工具,进而保证SELinux安全策略配置的正确性是很有必要和颇有意义。论文工作主要包括以下三方面： (1)对SELinux安全策略及其分析方法进行了讨论和研究。简要介绍了SELinux安全机制的发展演化、体系结构及Linux操作系统整体访问控制,讨论了SELinux安全模型、安全策略配置语言及实施机制,并重点就国内外现有SELinux安全策略分析方法进行了归纳分类和分析比较。特别地,针对现有有色Petri网分析法只是尝试性研究、需要借助数学软件工具完成分析并未独立实现的问题,确定了基于有色Petri网开展SELinux安全策略自动化分析方法研究的主题。 (2)系统研究了基于有色Petri网的SELinux安全策略自动化分析方法。围绕安全策略有效性分析目标,详细讨论了从SELinux安全策略配置文件集中提取安全策略要素的步骤和流程以及服务于SELinux安全策略自动化分析的有色Petri网模型的设计、构建和查询分析方案,另外还给出了相关的仿真验证案例。特别地,论文试图通过将安全策略配置中各安全要素和访问控制关系形式化为相关集合及映射,进而将访问控制关系映射及BNF查询语句转化为有色Petri网中的相关库所及变迁,从而通过变迁的发生来实现安全目标有效性的检测。 (3)设计和实现了基于有色Petri网的SELinux安全策略自动化分析工具原型。给出了原型系统的总体设计方案,并重点就描述安全策略要素和有色Petri网的相关数据结构及安全策略要素提取模块、有色Petri网构建模块、有色Petri网查询分析模块等核心模块的详细设计进行了讨论。原型系统由C语言编写,用83个函数实现了相关功能模块。通过采用学生-教师教学管理系统及实际SELinux应用场景的一套安全策略配置文件运行该原型系统进行验证分析,初步测试结果比较满意。
[Abstract]:Ensure system security.Security policy configuration is the key to the implementation of SELinux security protection. However, because of the complexity of security policy and the difficulty of management, it restricts the popularization and application of SELinux to some extent.Therefore, it is necessary and meaningful to study and construct SELinux security policy automatic analysis tool to ensure the correctness of SELinux security policy configuration.The work of the thesis mainly includes the following three aspects:1) the SELinux security policy and its analysis method are discussed and studied.This paper briefly introduces the development and evolution of the SELinux security mechanism, the architecture and the overall access control of the Linux operating system, and discusses the SELinux security model, security policy configuration language and implementation mechanism.The existing SELinux security policy analysis methods at home and abroad are summarized, classified and compared.In particular, aiming at the problem that the existing colored Petri net analysis method is only a tentative study and needs to be implemented independently with the help of mathematical software tools, the research topic of SELinux security policy automation analysis method based on colored Petri net is determined.The automatic analysis method of SELinux security policy based on colored Petri net is studied systematically.Around the goal of security policy effectiveness analysis, this paper discusses in detail the steps and processes of extracting security policy elements from the SELinux security policy configuration file set and the design of a colored Petri net model for SELinux security policy automation analysis.The scheme of query and analysis is constructed, and the relevant simulation cases are given.In particular, this paper attempts to formalize the security elements and access control relationships in security policy configuration into the related set and mapping, and then transform the access control relation mapping and BNF query statements into the relative libraries and transitions in colored Petri nets.In order to achieve the effectiveness of the security target detection through the occurrence of changes.The prototype of SELinux security policy automatic analysis tool based on colored Petri net is designed and implemented.This paper presents the overall design of the prototype system, and focuses on the description of the security policy elements and colored Petri net related data structure and security policy elements extraction module, colored Petri net construction module.The detailed design of the core modules such as the query analysis module of colored Petri net is discussed.The prototype system is written in C language, and 83 functions are used to realize the related function modules.A set of security policy configuration files based on the student-teacher teaching management system and the practical SELinux application scenario are used to run the prototype system for verification and analysis. The preliminary test results are satisfactory.
【学位授予单位】：北京交通大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP393.08

【参考文献】