| 目录 | 第1-7页 |
| 摘要 | 第7-8页 |
| Abstract | 第8-9页 |
| 第一章 绪论 | 第9-17页 |
| ·论文研究背景 | 第9-14页 |
| ·安全操作系统的发展历程 | 第9-10页 |
| ·安全操作系统相关标准 | 第10-11页 |
| ·安全模型在安全操作系统中的地位及发展趋势 | 第11-14页 |
| ·论文研究意义 | 第14页 |
| ·论文主要工作 | 第14-15页 |
| ·论文组织结构 | 第15-17页 |
| 第二章 操作系统经典安全模型研究 | 第17-28页 |
| ·经典单策略安全模型研究 | 第17-23页 |
| ·BLP模型 | 第17-18页 |
| ·Biba模型 | 第18-20页 |
| ·RBAC模型 | 第20-22页 |
| ·DTE模型 | 第22-23页 |
| ·混合多策略模型的国内外研究现状 | 第23-26页 |
| ·混合 BLP和 Biba | 第24页 |
| ·混合 MLS和 RBAC | 第24-25页 |
| ·混合 MLS和 TE | 第25页 |
| ·混合 RBAC和 DTE | 第25-26页 |
| ·相关研究 | 第26页 |
| ·本章小结 | 第26-28页 |
| 第三章 安全操作系统混合多策略模型SOS_HMPM的设计 | 第28-54页 |
| ·安全需求分析 | 第28-31页 |
| ·需求分析 | 第28-29页 |
| ·设计目标及基本设计思想 | 第29-31页 |
| ·SOS_HMPM的设计步骤 | 第31-32页 |
| ·SOS_HMPM的抽象计算模型 | 第32-33页 |
| ·SOS_HMPM的详细设计 | 第33-49页 |
| ·SOS_HMPM的安全策略定义 | 第33-34页 |
| ·SOS_HMPM的非形式化描述 | 第34-39页 |
| ·SOS_HMPM的形式定义 | 第39-49页 |
| ·SOS_HMPM的特点及其与 SELinux混合多策略模型的比较 | 第49-52页 |
| ·SOS_HMPM的特点 | 第49-51页 |
| ·SOS_HMPM与 SELinux混合多策略模型的比较 | 第51-52页 |
| ·本章小结 | 第52-54页 |
| 第四章 基于Isabelle/HOL的SOS_HMPM形式规范与验证方法 | 第54-68页 |
| ·安全策略模型形式化规范与验证的必要性 | 第54-55页 |
| ·Isabelle/HOL证明方法简介 | 第55-57页 |
| ·Isabelle/HOL简介 | 第55-56页 |
| ·Isabelle/HOL证明方法 | 第56-57页 |
| ·基于 Isabelle/HOL的SOS_HMPM形式化规范方法 | 第57-62页 |
| ·状态变量及状态规范 | 第58-59页 |
| ·不变量规范 | 第59-60页 |
| ·安全状态规范 | 第60页 |
| ·操作规则规范 | 第60-61页 |
| ·初始状态规范 | 第61-62页 |
| ·基于 Isabelle/ HOL的SOS_HMPM形式化验证方法 | 第62-66页 |
| ·证明工作总结 | 第66-67页 |
| ·本章小结 | 第67-68页 |
| 第五章 SOS_HMPM在SELinux中的应用研究 | 第68-86页 |
| ·SELinux内核体系结构 | 第68-69页 |
| ·基于 SELinux的SOS_HMPM实施架构 | 第69-79页 |
| ·系统访问控制处理流程 | 第70-71页 |
| ·安全服务器核心功能组件的设计及实现 | 第71-77页 |
| ·对象管理器及钩子函数调用层相关改进 | 第77页 |
| ·AVC改进 | 第77-78页 |
| ·策略管理服务器 | 第78-79页 |
| ·基于 SELinux的SOS_HMPM核心配置实例分析 | 第79-84页 |
| ·SELinux策略语言简介 | 第79-80页 |
| ·基于SELinux的SOS_HMPM核心配置实例 | 第80-84页 |
| ·安全性分析 | 第84页 |
| ·本章小结 | 第84-86页 |
| 第六章 总结与展望 | 第86-88页 |
| ·论文工作总结 | 第86-87页 |
| ·下一步工作展望 | 第87-88页 |
| 参考文献 | 第88-92页 |
| 附录A SOS_HMPM机密性模型安全操作规则的证明(部分) | 第92-94页 |
| 附录B SELinux的文件类许可权集到 MLS基许可权集的映射 | 第94-95页 |
| 作者简历 攻读硕士学位期间完成的主要工作 | 第95-96页 |
| 致谢 | 第96页 |
