中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
可信进程机制及相关问题研究
作者: 梁彬
答辩日期: 2004
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 可信进程 ; 安全操作系统 ; 可信主体 ; 特权 ; 形式化安全策略模型
其他题名: Research on Trusted Process Mechanism and Related Problems
摘要: 本文以一个实际的安全操作系统SECIMOS开发实践为基础,对安全操作系统可信进程机制及一些相关问题进行了研究,取得了以下四个方面的研究成果。第一,在对可信进程基本性质进行了深入研究基础上,从可信进程可信性出发给出了一个一般化的可信进程定义,消除了原有定义中存在的片面性,为实现一个较为完善的可信进程机制提供坚实的理论指导。以此定义为指导,在SECIMOS中实现了一个可信进程机制的原型系统,从多个方面保障了可信进程的可信性,提供了一个较为完善的可信进程解决方案。第二,为有效地支持最小特权原则,针对传统特权机制存在的局限性,提出了一种新的特权控制模型—基于状态的特权控制(State-based Privilege colltrol,SBPc),并在sEcIMos中实现了一个Linux平台上的SBPC原型系统—受控特权框(Controlled Privilege Fromework,CPF)。CBPC该机制以程序逻辑为中心,引入了特权状态的概念来进行特权控制;构建了特权与特权参数之间的显式关系;完善了特权进程的特权计算机制。通过CPF的实现,系统能进行细粒度的、自动的特权控制,且对应用软件完全透明,恶意入侵的危害性被大大降低,系统能有效地支持最小特权原则。第三,对轻量级形式化方法的核心思想进行了发展,将其应用到安全系统的FSPM规格说明和验证中,提出了一种轻量级的基于Z语言的安全操作系统FSPM规格说明及验证方法-LFSV(Lightweight FormalSpeeification and Verifieation)。LFSV使用简洁单一的形式化技术完成了FSPM的规格说明和验证,降低了模型复杂度和形式化建模的难度。使用LFSV方法为SECIMOS系统所实施的访问控制策略提供了精确易懂的FSPM,发现了一些与模型要求不一致的错误实现,特别是在一致性证明过程中发现了最新版的Linux内核特权机制中存在的一个致命错误,保障了SECIMOS系统安全控制的正确实施,提高了基础平台(Linux)的安全性。实践表明LFSV是一种有效的、容易掌握的FSPM规格说明和验证方法。第四,对一种公认的经典的由Sondhu等人提出的以RBAC实施BLP模型的方法进行了研究分析,指出并证明存在的错误,并揭示了其存在的不足,尤其是未能容纳BLP模型所不可缺少的可信主体概念。为此,提出了一种改进的方法-ISandhu方法,修正了原有方法的错误,提供了对可信主体概念的支持,面向实际应用扩展了其实施范围,保证了强制访问控制策略在RBAC中的正确实施,为在大量商业系统中以较小的代价引入强制访问控制提供了理论基础。总而言之,本文的研究成果将有助于研究开发完善的可信进程机制及构建高可信级别的安全操作系统。
英文摘要: With an experiment of implementing a practical secure operating system SECIMOS, research on the trusted process mechanism and some relative problems in secure operating system is discussed in this dissertation. As results, four principal archivements have been obtained. First, based on the thorough research on the fundamental properties of trusted processes, a new generic definition of trusted process is proposed from the aspect of trustworthiness. The definition overcomes the one-sidedness of some old definitions; provide a firm theoretical foundation for implementing a comparative complete trusted process mechanism. Under the guidance of this definition, a prototype of trusted process mechanism is implemented in SECIMOS; the trustworthiness of trusted process is assured in many ways. As a result, a comparative perfect solution is offered. Second, In order to provide effective support to the principle of least privilege, considering the limitation of traditional privilege mechanisms, a new privilege control model called State-Based Privilege Control (SBPC) is proposed and a prototype system for SBPC called Controlled Privilege Framework (CPF) is implemented in SECIMOS. SBPC concentrates on program logic, introduces the notation of privilege state for privilege control; constructs the explicit relationship between privileges and their parameters; and improves the privilege computing mechanism of privileged process. With the implementation of CPF, fine-grain and automatic privilege control can be transparently exercised to traditional applications, threats of malicious intrusion to a system can be reduced greatly, and support to the principle of least privilege can therefore be achieved effectively. Third, the ideas of lightweight formal methods are extended and applied to modeling the formal security policy model (FSPM) of secure operating system. A lightweight Z-based specification and verification method for FSPM called LFSV (Lightweight Formal Specification and Verification) is proposed. In this method, the formal specification and verification are performed with succinct and unitary formal techniques. As a result, the complexity of FSPM and difficulties of modeling are reduced greatly. LFSV has been employed in modeling FSPM of SECIMOS. Using it, a pricise and easy-understand formal policy model is provided for the access control mechanisms enforced by SECIMOS; and some inconsistent implementation that violate the requirements of model are found, especially, a serious error of orginal Linux privilege mechanism in the newest release is detected by consistence proving. Consequently, the correct enforcement of security control is ensured, and the security of basic platform (Linux) is improved. The experiment results show that this method is an effective and easy-master FSPM specifying and verifying method. Fourth, an existing classic and generally accepted method of enforcing BLP model in Role-based Access Control (RBAC) model presented by Sandhu et al. is researched and analyzed. Some errors of it are revealed and proved; and some shortages are pointed out, especially it can't accommodate the notation of trusted subject necessary for BLP model. An improved method called ISandhu method is presented. Based on this method, the mistakes of the original method are revised; the support to the notation of trusted subject is provided and the scope of enforcement objects is extended to meet the practical requirements. As results, the exact enforcement of mandatory access control in RBAC is guaranteed and the theoretical foundation for adopting MAC in a large amount of commercial systems with small cost is offered. In summary, the principal achievements of this dissertation are helpful to the research and development of a consummate trusted process mechanism, and to the construction of high-trust secure operating system.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6596
Appears in Collections:中科院软件所

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

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