高安全等级操作系统形式化开发技术研究
文献类型：学位论文
| 作者 | 李丽萍 |
| 学位类别 | 博士 |
| 答辩日期 | 2008-01-15 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 软件研究所 |
| 关键词 | 安全操作系统 形式化 形式化安全策略模型 形式化顶层规范 求精 安全体系结构 微内核 |
| 其他题名 | Research on Formal Development of High Security Level Operating System |
| 中文摘要 | 形式化开发安全保证技术是高安全等级操作系统的关键技术难点，国内尚未见相关研究成果。论文围绕高安全等级操作系统开发的整个生命周期，研究了安全策略模型和顶层规范的形式规范和形式验证技术及系统实现。取得以下几个方面的成果：第一，提出一种通用的状态机安全策略模型的形式规范构造方法。该方法基于Isabelle/HOL语言，对多种安全策略模型通用，且充分考虑了与功能规范的对应性分析的可行性。分析了方法的原理，并给出了SBLP模型的规范和验证实例；第二，提出一种形式化顶层规范的构造方法，并给出实施了SBLP模型的SecLinux文件系统的FTLS实例。首次形式化描述了与POSIX1003.1e兼容的ACL机制，并考虑了强制访问控制机制中客体间的信息流控制；第三，提出一种求精证明方法用于FSPM和FTLS之间的对应性分析。该方法包括一套基于Isabelle/HOL的求精规则，和一个引入了中间层的层次化求精方法。该方法大大降低了求精证明的难度。第四，针对支持动态多策略的需求，分析了当前几种典型安全体系结构在策略重用、策略共存方面的问题。提出一个新型的安全体系结构ELSM，引入模型组合器作为主模块实施模块堆栈管理和模块决策管理。策略决策基于访问控制空间形式规范方法，满足通用性。第五，给出了基于ELSM的FTLS的SecLinux文件系统实现实例。该系统基于Linux资源，为主流操作系统实现高安全等级提供了有意义的参考。第六，提出了一种支持多策略的基于微内核的安全体系结构，并基于此开发和验证一个微内核安全操作系统SecL4。该体系结构模块性强、结构清晰，解决了代码实现层难以形式化的难题。体系结构中的TPM保证了系统的引导和安全组件引入系统的可信性。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 140 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7106]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 李丽萍. 高安全等级操作系统形式化开发技术研究[D]. 软件研究所. 中国科学院软件研究所. 2008. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。