| 摘要 | 第1-6页 |
| Abstract | 第6-8页 |
| 目录 | 第8-15页 |
| 第1章 引言 | 第15-23页 |
| ·选题背景与意义 | 第15-16页 |
| ·安全操作系统形式化验证的发展历史 | 第16-18页 |
| ·论文框架与研究目标 | 第18-20页 |
| ·论文框架 | 第19-20页 |
| ·论文研究目标 | 第20页 |
| ·论文主要研究内容和结构安排 | 第20-23页 |
| 第2章 安全操作系统的形式化验证 | 第23-47页 |
| ·安全模型的形式化描述 | 第23-37页 |
| ·安全策略与安全模型 | 第24-27页 |
| ·BLP模型 | 第27-30页 |
| ·Biba模型 | 第30-32页 |
| ·TE模型和DTE模型 | 第32-34页 |
| ·RBAC模型 | 第34-37页 |
| ·小结 | 第37页 |
| ·形式化安全验证技术及模型检测 | 第37-45页 |
| ·系统建模 | 第38-39页 |
| ·LTL和CTL | 第39-42页 |
| ·模型检测 | 第42-45页 |
| ·本章小结 | 第45-47页 |
| 第3章 基于模型检测的SELinux策略统一信息流验证方法 | 第47-75页 |
| ·SELinux简介 | 第49-57页 |
| ·SELinux框架 | 第50-51页 |
| ·SELinux策略模型与描述语言 | 第51-57页 |
| ·SELinux策略的形式化建模 | 第57-62页 |
| ·策略规则的形式化描述 | 第57-59页 |
| ·策略模型的Kripke结构 | 第59-61页 |
| ·授权关系与信息流 | 第61-62页 |
| ·安全需求描述 | 第62-70页 |
| ·安全需求描述设计原则 | 第63页 |
| ·安全需求分析 | 第63-65页 |
| ·安全需求描述语言的设计 | 第65-67页 |
| ·SELinux的安全需求描述语言实现 | 第67-70页 |
| ·模型检测实例 | 第70-73页 |
| ·web server策略分析 | 第70-72页 |
| ·军队采购系统策略分析 | 第72-73页 |
| ·本章小结 | 第73-75页 |
| 第4章 基于模型检测的安全模型验证方法 | 第75-103页 |
| ·模型验证框架 | 第76-78页 |
| ·安全策略模型的描述 | 第78-82页 |
| ·UML简介 | 第79-81页 |
| ·安全策略模型的UML描述 | 第81-82页 |
| ·模型描述的状态机语义 | 第82-92页 |
| ·UML状态机的抽象语法 | 第82-85页 |
| ·UML的配置和复合迁移 | 第85-86页 |
| ·Run-to-Completion语义 | 第86-87页 |
| ·UML到PROMELA模型的转换 | 第87-92页 |
| ·安全公理的描述 | 第92-93页 |
| ·两个BLP改进模型的验证 | 第93-101页 |
| ·DBLP的UML建模 | 第93-96页 |
| ·SLCF的UML建模 | 第96页 |
| ·安全需求的描述 | 第96-98页 |
| ·实验结果分析 | 第98-101页 |
| ·本章小结 | 第101-103页 |
| 第5章 基于安全状态迁移的简并测试集生成方法 | 第103-123页 |
| ·测试用例化简方法的分析 | 第104-111页 |
| ·基于模型检测的测试用例化简框架 | 第104-106页 |
| ·现有测试集优化技术分析 | 第106-111页 |
| ·基于状态迁移的用例化简 | 第111页 |
| ·简并测试集的形式化定义 | 第111-113页 |
| ·简并测试集生成算法 | 第113-118页 |
| ·DTS生成算法 | 第113-116页 |
| ·DTS生成算法的改进 | 第116-118页 |
| ·算法测试与分析 | 第118-120页 |
| ·算法测试 | 第118-119页 |
| ·算法分析 | 第119-120页 |
| ·本章小结 | 第120-123页 |
| 第6章 结束语 | 第123-127页 |
| ·论文主要成果 | 第123-124页 |
| ·未来工作展望 | 第124-127页 |
| 附录A SELinux权限映射 | 第127-137页 |
| 附录B 军队采购系统的策略配置 | 第137-139页 |
| 参考文献 | 第139-151页 |
| 致谢 | 第151-153页 |
| 在读期间发表的学术论文与取得的研究成果 | 第153页 |