| 题名 | 高等级安全操作系统完整性策略模型设计开发及其形式化研究 |
| 作者 | 唐柳英 |
| 学位类别 | 博士 |
| 答辩日期 | 2007-06-04 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 软件研究所 |
| 关键词 | 安全操作系统 完整性 完整性策略模型 安全体系结构 形式化 |
| 其他题名 | Development and Formalisation of Integrity Policy Models in High-Level Operating Systems |
| 中文摘要 | 高等级安全操作系统的完整性保护比机密性保护要复杂得多，对它的研究工作远没有机密性保护进展得顺利。本文基于TESEC等国内外计算机信息系统评估标准的要求，从理论和实践两个方面对高等级安全操作系统完整性保护策略模型的设计、实现和分析进行了研究，取得了以下五个方面的主要成果：第一，通过综合地分析比较经典的各种完整性策略模型各自的优点和不足，指出了完整性保护策略模型的发展方向。对当前广泛应用的混合RBAC-DTE策略，首次揭露了当中的多角色管理问题，从角色特权和角色的访问许可权两种层面上结合角色所允许进入的域，提出一种角色粗划分粒度，域细划分粒度的解决方法，进一步地引入域的静态继承关系来提供角色获得访问许可权的另一种方式，不但解决不同域的进程共享访问控制权集，同时又使策略的代码尺寸得以有效控制，特别地，充分支持极小特权原则。第二，利用传统DTE模型的突出特征，即通过域限制进程的活动范围使得授权用户的不当修改行为得以有效控制，以及模型易于实现和应用等特点，结合Biba模型的明确完整性目标，在对Biba完整性两种角度解释的基础上，分别提出以DTE为基本的组成框架，不同Biba完整性解释为安全目标的两种DTE完整性保护形式模型。从策略目标分析和验证来看，这两种DTE完整性保护形式模型差别在于它们的实用性，但它们都为DTE系统的完整性策略配置、完整性策略分析和完整性保护验证提供了理论基础。第三，提供了所设计的DTE完整性保护形式模型内在一致性的非形式化证明过程。进一步地通过选用Isabelle/Isar形式化验证技术，以更为严谨的形式化方法成功地对DTE完整性保护形式模型进行描述并验证其内在一致性。第四，研究SELinux中DTE模型的实现技术，在达到结构化保护级的安胜OS v4.0系统上，结合Flask安全体系结构和LSM访问控制框架，从策略配置、数据结构、系统调用、应用层命令以及访问控制流程等方面真正地实现了DTE完整性保护形式模型。第五，在安全增强L4微内核（SecL4微内核）上实现了DTE完整性保护形式模型的工作基础上，提供SecL4微内核的DTLS，并有效论证了TCB的描述性顶层规范(DTLS)和模型的一致性。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 161 |
| 内容类型 | 学位论文 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7442]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 唐柳英. 高等级安全操作系统完整性策略模型设计开发及其形式化研究[D]. 软件研究所. 中国科学院软件研究所. 2007. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论