基于模型检测的安全操作系统验证方法研究

摘要

安全操作系统的形式化验证，作为高等级安全操作系统评估准则的一项重要指标和操作系统安全性能最有效的证明手段，具有重要意义与实用价值。目前形式化验证主要分为模型检测和定理证明两大类方法。本论文集中探讨了模型检测技术在安全操作系统验证各个层次中的一些关键问题，主要工作和创新成果如下： 首先，针对SELinux策略配置复杂难以分析的问题，提出了一种基于模型检测的SELinux策略分析方法，以验证策略实施与安全需求之间的一致性问题。采用扩展的标签迁移系统，将MLS策略和普通TE-RBAC策略的描述融入到统一的描述框架下，并完整定义了策略配置语句的信息流属性，不仅考虑了型访问规则造成的信息流动，也兼顾了型转移以及MLS约束对策略模型信息流的影响。设计了一种新型的安全需求描述语言，将安全需求与和策略配置剥离开，使安全需求的描述不依赖于对实施细节的了解，扩展了模型检测器探索未知漏洞的能力。 其次，提出了安全模型与安全需求的一致性验证方法。利用UML类图和状态机图在系统动、静态建模方面的表达能力，设计了一种新的安全模型UML描述方式。并在此基础上给出了UML图的状态机语义，将UML模型编译成模型检测器的规范语言，使用模型检测分析安全模型的性能。这一成果使利用自动化工具辅助安全模型的正确性验证成为可能，减少了传统安全模型验证方法中对验证人员形式化理论的过高要求以及繁重的手工推导过程。 最后，探讨了安全验证中测试集的优化问题。提出简并测试集的概念，将测试冗余从状态扩展到状态迁移，将测试集中的冗余归为最小。在此定义的基础上，我们以模型检测作为后端的搜索引擎，给出简并测试集的生成算法。首次讨论了在测试集和系统实现相悖时对测试结果的判定。并据此对算法加以改进，使得在不影响测试集生成的前提下，即使测试失败，测试人员也可以准确地对失败位置进行定位。

目录

文摘

英文文摘

论文说明：图表目录

声明

第1章引言

1.1 选题背景与意义

1.2安全操作系统形式化验证的发展历史

1.3论文框架与研究目标

1.3.1 论文框架

1.3.2论文研究目标

1.4论文主要研究内容和结构安排

第2章安全操作系统的形式化验证

2.1 安全模型的形式化描述

2.1.1 安全策略与安全模型

2.1.2 BLP模型

2.1.3 Biba模型

2.1.4 TE模型和DTE模型

2.1.5 RBAC模型

2.1.6 小结

2.2形式化安全验证技术及模型检测

2.2.1 系统建模

2.2.2 LTL和CTL

2.2.3 模型检测

2.3本章小结

第3章基于模型检测的SELinux策略统一信息流验证方法

3.1 SELinux简介

3.1.1 SELinux框架

3.1.2 SELinux策略模型与描述语言

3.2 SELinux策略的形式化建模

3.2.1 策略规则的形式化描述

3.2.2 策略模型的Kripke结构

3.2.3 授权关系与信息流

3.3安全需求描述

3.3.1 安全需求描述设计原则

3.3.2 安全需求分析

3.3.3 安全需求描述语言的设计

3.3.4 SELinux的安全需求描述语言实现

3.4模型检测实例

3.4.1 web server策略分析

3.4.2 军队采购系统策略分析

3.5本章小结

第4章基于模型检测的安全模型验证方法

4.1模型验证框架

4.2安全策略模型的描述

4.2.1 UML简介

4.2.2 安全策略模型的UML描述

4.3模型描述的状态机语义

4.3.1 UML状态机的抽象语法

4.3.2 UML的配置和复合迁移

4.3.3 Run-to-Completion语义

4.3.4 UML到PROMELA模型的转换

4.4安全公理的描述

4.5两个BLP改进模型的验证

4.5.1 DBLP的UML建模

4.5.2 SLCF的UML建模

4.5.3 安全需求的描述

4.5.4.实验结果分析

4.6本章小结

第5章基于安全状态迁移的简并测试集生成方法

5.1 测试用例化简方法的分析

5.1.1 基于模型检测的测试用例化简框架

5.1.2 现有测试集优化技术分析

5.1.3 基于状态迁移的用例化简

5.2简并测试集的形式化定义

5.3简并测试集生成算法

5.3.1 DTS生成算法

5.3.2 DTS生成算法的改进

5.4算法测试与分析

5.4.1 算法测试

5.4.2 算法分析

5.5本章小结

第6章结束语

6.1论文主要成果

6.2未来工作展望

附录

参考文献

致谢

在读期间发表的学术论文与取得的研究成果