安全操作系统策略模型的关键问题研究
文献类型：学位论文
| 作者 | 何建波 |
| 学位类别 | 博士 |
| 答辩日期 | 2007-06-04 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 软件研究所 |
| 关键词 | 安全操作系统 安全策略 安全模型 形式化方法 信息流分析 |
| 其他题名 | Study on the Key Issues of Security Policy Models in Secure Operating Systems |
| 中文摘要 | 安全策略模型是开发安全操作系统的基础，它对安全策略的描述准确与否，决定着所开发的系统安全机制是否能正确地实施安全策略。因此，安全模型的研究对于安全操作系统的开发具有重要意义。本文从安全模型动态改进技术，安全模型的形式化分析，完整性模型的实现机制以及SELinux的策略分析四个方面，对安全模型研究领域出现的若干关键问题展开研究，取得了下面四个方面的主要成果： 第一，深入研究了以限制可信主体权限方式改进的BLP模型和以动态调整非可信主体敏感级方式改进的BLP模型，总结了它们的改进思路和理论依据；发现了两个公开发表的BLP改进模型¬——DBLP和SLCF模型——的安全缺陷，并予以修正；给出了第二类模型动态调整非可信主体敏感级的通用模式；这一研究成果为人们避免选用不安全的模型提供了有意义的理论支持，同时也为人们改进BLP模型提供了技术指导。 第二，分析了现有安全模型形式化分析方法的不足，指出除了对模型进行内在一致性验证以外，更重要的是确认模型的不变式与安全策略一致性，即模型外在一致性分析，以确保模型对安全策略的正确建模。并通过实例分析说明了对模型执行外在一致性分析的必要性。这一工作解决了形式化分析安全模型时，“需要证明什么”和“如何进行证明”的问题； 第三，对比了各种Clark-Wilson模型的实现技术，指出了它们在实现Clark-Wilson模型时的不足；深入分析了Clark-Wilson模型难以在系统中完全实现的原因，研究了配置TE来实现Clark-Wilson模型的可行性，并给出了配置规则和约束条件。TE配置与Clark-Wilson模型规则的对应性分析表明，TE细粒度访问控制的优势不仅利于实现Clark-Wilson模型的访问规则，而且有利于系统减少对完整性认证过程（IVP）的依赖。 第四，基于已有的SELinux信息流分析工作，提出了一种SELinux信息流模型SELIF。通过构造有效安全上下文集合和安全上下文的授权关系，根据许可权的信息流语义，SELIF模型用标记转换系统表示的安全上下文关系来刻画信息流。SELIF信息流模型可以直观地表达SELinux策略所描述的安全上下文之间的信息流路径，实现对复杂策略的直观分析和管理。我们还讨论了如何用SELIF模型分析策略的Biba完整性，可信管道和职责隔离等多个安全目标。此外，还展示了SELIF在带权信息流分析和基于域转换攻击检测方面的可能应用。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 180 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/5784]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 何建波. 安全操作系统策略模型的关键问题研究[D]. 软件研究所. 中国科学院软件研究所. 2007. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。