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

摘要

操作系统是计算机资源的直接管理者，位于整个信息系统的最底层，其安全问题是信息安全的核心问题。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应用场景的一套安全策略配置文件运行该原型系统进行验证分析，初步测试结果比较满意。

目录

声明

致谢

摘要

1 绪论

1．1 课题背景

1．2 国内外研究现状

1．3 论文研究内容与技术路线

1．4 论文组织结构

2 研究基础

2．1 SELinux安全机制

2．1．1 SELinux发展演化

2．1．2 MAC及Flask体系架构

2．1．3 Linux安全访问控制

2．2 SELinux安全策略

2．2．1 SELinux安全模型

2．2．2 SELinux策略配置语言

2．2．3 SELinux策略实施机制

2．3 SELinux安全策略分析方法

2．3．1 访问控制空间分析法

2．3．2 信息流分析法

2．3．3 有色Petri网分析法

2．4 本章小结

3 基于有色Petri网的SELinux安全策略自动化分析方法

3．1 安全策略分析目标

3．2 安全策略要素提取

3．3 安全策略有色Petri网的构建与查询

3．3．1 有色Petri网分析模型

3．3．2 安全策略有色Petri网构建

3．3．3 安全策略有色Petri网查询分析

3．3．4 安全策略有色Petri网的仿真验证

3．4 本文分析方法与现有分析方法的比较

3．5 本章小结

4 原型设计与实现

4．1 总体设计

4．2 关键数据结构设计

4．2．1 安全策略要素描述用数据结构

4．2．2 有色Petri网描述用数据结构

4．3 关键模块详细设计

4．3．1 安全策略要素提取模块

4．3．2 有色Petri网构建模块

4．3．3 有色Petri网查询分析模块

4．4 系统实现

4．5 本章小结

5 原型测试与结果分析

5．1 测试方案

5．2 测试用例

5．3 原型验证

5．3．1 正面验证

5．3．2 反面验证

5．3．3 主客体访问空间的验证

5．4 结果分析

5．5 本章小结

6 结束语

6．1 工作总结

6．2 研究展望

参考文献

作者简历及攻读硕士学位期间取得的研究成果

学位论文数据集