高安全级操作系统形式设计的研究
文献类型：学位论文
| 作者 | 季庆光 |
| 学位类别 | 博士 |
| 答辩日期 | 2004 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 形式模型 机密性策略 完整性策略 极小特权原理 无干扰理论 信息流 权能 模型层次结构 |
| 其他题名 | Study on Formalization Design for High-Level Secure Operating System |
| 学位专业 | 计算机应用技术 |
| 中文摘要 | 本文主要研究开发高安全等级的操作系统所必需的安全策略形式模型，为此我们从形式设计方法的探讨入手，确定模型设计的基本原则及组织结构，然后根据确定的组织结构逐步展开设计，提出支持多策略的形式框架、实现机密性策略的可动态调节安全级范围的多级安全模型DMLR-MLS（本文把它与DAC模型合在一起形成DBLP模型）、基于DTE技术实现完整性保护的形式模型DTE-IPM及基于权能、角色及DTE的特权控制模型PCM＿RBPC。之后，分析整个模型可能存在的隐通道：提出分析模型的设计。最后，结合Linux内核，初步探讨模型的解释。在这篇学位论文里，提出了八条模型设计的基本原则。构建了三位一体的模型开发模式：形式架构、策略规范语言及分量策略模型。分析了区分实现模与分析模型的必要性。形式框架支持推理多策略的策略等价，策略冲突及策略协作，在多方面优于目前文献中的形式框架。DBLP模型作为可用于系统设计的形式模型，它在多方面改进了现有文献中的工作，使模型更实用。对于DTE-IPM模型，就我们所知，使用DTE技术构筑一个完整的完整性保护形式模型，是本文第一次进行了这样的尝试，该模型在控制恶意信息流方面有自己特殊的不变量。特权控制是在操作系统中实现安全的关键环节，模型PCM-RBPC通过三层结构，即：管理层、功能层及执行层，有效地实现了极小特权原理，从而成功地控制了特权，这个模型在五个方面有创新。提出了一个模型层次结构，并给出了在这个模型层次结构下系统安全的定义，获得安全的分解定理。给出了抽象安全策略的新定义，并用无干扰理论重新进行了解释。提出了多对象管理器与多安全服务器并存的实现体系。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 163 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6552]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 季庆光. 高安全级操作系统形式设计的研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。