中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
高安全等级操作系统可信进程安全策略及其关键技术的研究
作者: 沈晴霓
答辩日期: 2006-06-08
授予单位: 中国科学院软件研究所
授予地点: 软件研究所
学位: 博士
关键词: 安全操作系统 ; 可信进程 ; 安全策略 ; 模型 ; 形式化分析 ; 特权 ; 可信路径
摘要: 在安全系统中,惟一重要的接口是能够进入安全周界的外部接口,可信进程明显运行于安全周界之内且是安全内核的扩展。所以,可信进程与内核之间的接口不比内核各部分之间的接口更特别,需要一种安全策略始终实施于安全周界。但可信进程缺乏像BLP模型一样具有通用指导性的形式化模型,基于TCSEC B2级以上安全功能需求,以及CC标准EAL5以上评估保证级的形式化需求,提供一个通用的可信进程安全策略和模型,可为系统开发者和评估者规范和验证可信进程的安全性提供参考。在解决以上问题上,本文取得了六个方面的成果:第一,在系统和深入地分析可信进程的本质及其行为特性的基础上,通过找出通用的四种可信进程行为的共同特点和安全需求,首次提出了一种基于RBAC、DTE、POSIX权能机制和无干扰理论相结合的设计思想,并制定出控制可信进程行为的通用安全策略,为建立通用的可信进程安全模型奠定了基础。第二,通过对现有安全系统中权能遗传算法的分析,提出了一种多策略适应的POSIX权能遗传算法。该算法可以支持安全操作系统对可信进程行为实现不同的特权控制需求,并保证最小特权原则的有效实施。第三,在深入研究建立形式化安全策略模型的目的、要求和方法的基础上,借助数学的形式语言,给出了一个完整的、形式化的可信进程安全策略模型。本模型的提出,对于形式化规范和验证可信进程的行为,为我们今后对TCSEC B2级以上高安全等级操作系统的设计和评估奠定了一定的基础。第四,在深入分析和对比目前可用于高安全等级操作系统中的形式化分析方法和证明工具的基础之上,提出了用Isabelle语言对可信进程模型属性和规则进行形式化规范的方法,总结出基于Isabelle系统证明模型规范内部一致性和正确性的实用方法。第五,基于符合GB17859-1999第四级(TCSEC B2级)、自主开发的结构化保护级安全操作系统(安胜OS v4.0)的特权控制目标,提出了本模型在该系统中进行实现的有效方法。第六,对可信进程实现涉及的其他几个关键技术问题,包括可信路径机制、审计机制和可信功能的设计和实现等都做了有益的研究和探讨,给出了在高安全等级操作系统环境中进行实施的大致方案和原则。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7466
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200218015003333沈晴霓_null.pdf(1523KB)----限制开放-- 联系获取全文

Recommended Citation:
沈晴霓. 高安全等级操作系统可信进程安全策略及其关键技术的研究[D]. 软件研究所. 中国科学院软件研究所. 2006-06-08.
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