中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
高安全级操作系统形式设计的研究
作者: 季庆光
答辩日期: 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通过三层结构,即:管理层、功能层及执行层,有效地实现了极小特权原理,从而成功地控制了特权,这个模型在五个方面有创新。提出了一个模型层次结构,并给出了在这个模型层次结构下系统安全的定义,获得安全的分解定理。给出了抽象安全策略的新定义,并用无干扰理论重新进行了解释。提出了多对象管理器与多安全服务器并存的实现体系。
英文摘要: This thesis focuses on studying security policy formal model, which is indispensable for developing high level secure operating system. For this, based on analyzing formalized design method, principles and architecture for designing formal model are proposed, then according to them, the model is designed hierarchically. First, a formal framework for supporting multipolicy is presented. Second, some component models are constructed, including dynamically mediated security level rang multilevel security model DMLR-MLS, which is used to implement confidentiality policy, and renamed as DBLP model after it is combined with DAC model, based-DTE integrity protection security model DTE^IPM, and privilege control model PCM-RBPC based on capability mechanism, role mechanism and DTE privilege mechanism. Third, an analysis model aiming at finding out potential covert channel existing in implementation model is proposed. At last, model interpretation is discussed elementarily based on Linux kernel. In this work, eight principles are set out to direct model design. The model development mode with three components: formal framework, model specification language and component models, is figured out. The detailed analysis shows that it is necessary to distinguish implementation model from analysis model. The resulted formal framework reasoning about policy equivalence, policy conflict and policy cooperation has more advantages over ones described in literature. As a model that can be used to develop practical system, DBLP model has been designed based on some researches improving those works described in literature relevant to confidentiality policy models. To our knowledge, DTE-IPM is the first trying to build a whole integrity policy model based on DTE. It presents some new invariants, used to prevent malicious information flow from jeopardizing system, different from ones in some literatures. As key ingredient implementing secure operating system, effective privilege control is needed, and captured successfully by our model PCM^RBPC by means of the implementation of the least privilege principle with three layers structure, i.e., administration layer, functionality layer and execution layer; five original findings have been used to design this model. A model hierarchy is proposed, and system security under this model hierarchy is defined, and the unwinding theorem of system security is proved. The security policy is abstractly redefined, and made a new interpretation in noninterference theory. An implementation architecture consisted of multiple object managers and multiple security servers is described.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6552
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW013930.pdf(2317KB)----限制开放-- 联系获取全文

Recommended Citation:
季庆光. 高安全级操作系统形式设计的研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004-01-01.
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