QQ客服 官方微博 反馈留言

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

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。