安全系统形式化设计与分析研究
| 致谢 | 第1-6页 |
| 摘要 | 第6-8页 |
| Abstract | 第8-13页 |
| 插图清单 | 第13-14页 |
| 附表清单 | 第14-15页 |
| 1 绪论 | 第15-31页 |
| ·研究背景 | 第15-16页 |
| ·研究现状 | 第16-25页 |
| ·安全策略与安全模型 | 第16-20页 |
| ·访问控制与隐蔽通道 | 第20-23页 |
| ·信息流分析方法概述 | 第23-25页 |
| ·课题来源与研究内容 | 第25-27页 |
| ·课题来源 | 第25页 |
| ·研究内容 | 第25-27页 |
| ·论文组织结构 | 第27-31页 |
| 2 基于多级安全策略的动态二维标识模型 | 第31-53页 |
| ·引言 | 第31-32页 |
| ·相关研究工作 | 第32-33页 |
| ·基于多级安全策略的动态统一模型 | 第33-46页 |
| ·基本模型元素 | 第33-36页 |
| ·模型不变量 | 第36页 |
| ·模型限制性条件 | 第36-39页 |
| ·模型迁移规则 | 第39-46页 |
| ·模型安全性分析 | 第46-48页 |
| ·实例分析与性能测试 | 第48-51页 |
| ·实例分析 | 第48-50页 |
| ·性能测试 | 第50-51页 |
| ·本章小结 | 第51-53页 |
| 3 基于进程代数的时间信息流分析 | 第53-75页 |
| ·引言 | 第53-54页 |
| ·相关研究工作 | 第54-55页 |
| ·时间系统中的信息流安全性质分析 | 第55-63页 |
| ·时间安全进程代数tSPA | 第55-58页 |
| ·时间信息流无干扰安全性质分析 | 第58-63页 |
| ·时间系统中的非传递无干扰安全性质分析 | 第63-74页 |
| ·扩展tSPA | 第63-64页 |
| ·非传递时间互拟强无干扰 | 第64-65页 |
| ·非传递时间互拟复合不可演绎 | 第65-66页 |
| ·非传递时间强互拟强无干扰 | 第66-68页 |
| ·安全属性的组合性 | 第68-71页 |
| ·实例分析 | 第71-74页 |
| ·本章小结 | 第74-75页 |
| 4 面向隐蔽通道构建的多级安全形式定义 | 第75-83页 |
| ·引言 | 第75-76页 |
| ·问题的提出 | 第76-77页 |
| ·多级安全形式定义 | 第77-82页 |
| ·隔离安全与偏序关系 | 第77-80页 |
| ·传递与非传递安全特性 | 第80-82页 |
| ·本章小结 | 第82-83页 |
| 5 基于可信计算平台的安全操作系统设计与实现 | 第83-103页 |
| ·系统设计概述 | 第83-87页 |
| ·设计原则与思想 | 第83-85页 |
| ·功能模块划分 | 第85-87页 |
| ·系统关键技术实现 | 第87-100页 |
| ·强制访问控制机制实现 | 第87-88页 |
| ·恶意代码防护机制实现 | 第88-92页 |
| ·可信恢复机制实现 | 第92-95页 |
| ·隐蔽信道处理机制实现 | 第95-100页 |
| ·系统功能测试与性能测试 | 第100-101页 |
| ·功能测试 | 第100页 |
| ·性能测试 | 第100-101页 |
| ·本章小结 | 第101-103页 |
| 6 结束语 | 第103-107页 |
| ·论文工作总结 | 第103-105页 |
| ·进一步的工作 | 第105-107页 |
| 参考文献 | 第107-119页 |
| 作者简历及在学期间所取得的科研成果 | 第119-120页 |
