中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
高等级安全操作系统完整性策略模型设计开发及其形式化研究
作者: 唐柳英
答辩日期: 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)和模型的一致性。
英文摘要: The integrity protection in a high-level secure operating system is more complex than the confidentiality protection, so study on integrity protection is progressing slower than the confidentiality. Based on the requirements of the famous international or domestic computer information system evaluation criteria such as TCSEC, the design, implementation and analysis of high-level secure operation system are conducted both theoretically and practically in this dissertation. As a result, five principal achievements have been obtained. First, after the summary and comparison on various classical integrity policy models, future research directions in integrity protection policy models are pointed out. For the current widely applied hybrid RBAC-DTE policy, the problem of administration of multiple roles in it is revealed at the first time. From the aspects of privilege and access right combined with the domain a role is allowed to enter, an approach to dividing roles and domains that roles are more coarse-grained than domains, is proposed, and a static-inheritance relationship between domains is introduced. This method solves the problem of sharing access right set among processes in different domains while effectively controlling policy code size, especially, supports the principle of least privilege sufficiently. Second, with considerations on the most important advantage of the traditional DTE model, i.e., a domain limits the operations available to a subject such that the inappropriate modification made by authorized users is controlled effectively, and the model’s advantages in convenient implementation and use, together with Biba explicit integrity goals, two types of DTE integrity protection formal models are proposed separately in terms of different expressions on Biba integrity, in which DTE is the underlying composition framework and the Biba integrity is the security goals. From the point of view of the analysis and verification of policy goals, they are different mainly in their values of practical use, but both provide the theoretical basis for integrity policy configuration, policy integrity analysis and verification of the DTE secure systems. Third, the internal consistency of the designed DTE integrity protection models is proved informally. Furthermore, through the decision on the use of the formal verification technology, Isabelle/Isar, the specification and internal consistency verification of one of the DTE integrity formal models are presented well in a stricter way. Fourth, the SELinux implementation of the DTE model is discussed, on AnSheng OS v4.0, a secure operating system in accordance with the requirements of the Structured Protection Level, through the combination of Flask secure architecture and LSM access control framework, DTE integrity formal models are really implemented in many aspects such as policy configuration, data structure, system call, application-level command and access control flow chart. Fifth, building on the work basis of the implementation of DTE integrity formal models on the security-enhanced L4 microkernel, SecL4, the descriptive top-level specification (DTLS) of SecL4 microkernel is given, and correspondence between this DTLS to the models is effectively demonstrated.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7442
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200118015004982唐柳英_paper.pdf(1497KB)----限制开放-- 联系获取全文

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