中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
安全操作系统策略模型的关键问题研究
作者: 何建波
答辩日期: 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在带权信息流分析和基于域转换攻击检测方面的可能应用。
英文摘要: Security policy model, or security model, acts as the foundation for secure operating systems development. Whether the resulting system security mechanisms have correctly enforced the security policies depends on the precision of security definition in the models. Therefore, studies on the security models are significant for the research and development of secure operating systems. In this dissertation, research on the key issues of security models is conducted from four perspectives: model dynamic modification, model formal analysis, enforcement mechanism for integrity model, and policy analysis for SELinux (Security-Enhanced Linux). As a result, four principal achievements have been achieved: Firstly, two types of modified BLP models are analyzed. One is characterized by limiting the access rights of trusted subjects, while the other improved the classical BLP model by adding rules for dynamically adjusting the security labels of the untrusted subjects. Their philosophies for modifications are outlined. Moreover, two modified BLP models, namely DBLP and SLCF, are proved to be insecure and the errors are corrected. At last, the general pattern for dynamically adjusting security labels of untrusted subjects is presented. The efforts not only provide the theoretical foundation for model selections, but also propose the technical guideline for further refining BLP model. Secondly, the existing formal analysis techniques for security models is investigated, which comes to a conclusion that besides verifying the internal consistency of formal security models, it is far more essential to validate security models, i.e. external consistency analysis, to ensure the models define the security requirements rightly. To illustrate the necessity for validation, the DBLP model are formalized in a formal language, Z notation, and analyzed in Z/EVES. The efforts answer the questions, such as “what should be proved” and “how to prove”, when formally analyzing security models. Thirdly, the existing implementation techniques for the Clark-Wilson model are reviewed and the reasons that impede the enforcement of the Clark-Wilson model in operating systems are discussed. Then the feasibilities for configuring Type Enforcement to implement Clark-Wilson model are presented and the configuration rules and constraints are given. The corresponding analyses show that the fine-grained access control of Type Enforcement is suited not only to enforce the access rules in Clark-Wilson models, but also to reduce the dependency on the Integrity Verification Procedure, IVP. Finally, based on the existing information flow analysis efforts for SELinux, an information flow model for SELinux, SELIF, is presented. To construct SELIF model, the set for valid security contexts is defined and authorization relationships among valid security contexts are outlined firstly. Then according to the information flow semantic of permissions, the SELIF depicted the information flow relationships between the security contexts in a labeled transition system. SELIF model can be used to analyze and manage the complex policies. The applications of SELIF model are also discussed, such as analyzing the security targets like Biba integrity, assured pipeline and separation of duty. In addition, the potential application of SELIF model on weighted information flow analysis and domain-transition-based attack detection are also presented.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/5784
Appears in Collections:中科院软件所

Files in This Item:

There are no files associated with this item.


Recommended Citation:
何建波. 安全操作系统策略模型的关键问题研究[D]. 软件研究所. 中国科学院软件研究所. 2007-06-04.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[何建波]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[何建波]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace