高等级安全操作系统完整性策略模型设计开发及其形式化研究

来源 :中国科学院软件研究所 | 被引量 : 0次 | 上传用户:woshixiaomei110
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
高等级安全操作系统的完整性保护比机密性保护要复杂得多,对它的研究工作远没有机密性保护进展得顺利。本文基于TESEC等国内外计算机信息系统评估标准的要求,从理论和实践两个方面对高等级安全操作系统完整性保护策略模型的设计、实现和分析进行了研究,取得了以下五个方面的主要成果:第一,通过综合地分析比较经典的各种完整性策略模型各自的优点和不足,指出了完整性保护策略模型的发展方向。对当前广泛应用的混合RBAC-DTE策略,首次揭露了当中的多角色管理问题,从角色特权和角色的访问许可权两种层面上结合角色所允许进入的域,提出一种角色粗划分粒度,域细划分粒度的解决方法,进一步地引入域的静态继承关系来提供角色获得访问许可权的另一种方式,不但解决不同域的进程共享访问控制权集,同时又使策略的代码尺寸得以有效控制,特别地,充分支持极小特权原则。第二,利用传统DTE模型的突出特征,即通过域限制进程的活动范围使得授权用户的不当修改行为得以有效控制,以及模型易于实现和应用等特点,结合Biba模型的明确完整性目标,在对Biba完整性两种角度解释的基础上,分别提出以DTE为基本的组成框架,不同Biba完整性解释为安全目标的两种DTE完整性保护形式模型。从策略目标分析和验证来看,这两种DTE完整性保护形式模型差别在于它们的实用性,但它们都为DTE系统的完整性策略配置、完整性策略分析和完整性保护验证提供了理论基础。第三,提供了所设计的DTE完整性保护形式模型内在一致性的非形式化证明过程。进一步地通过选用Isabelle/Isar形式化验证技术,以更为严谨的形式化方法成功地对DTE完整性保护形式模型进行描述并验证其内在一致性。第四,研究SELinux中DTE模型的实现技术,在达到结构化保护级的安胜OSv4.0系统上,结合Flask安全体系结构和LSM访问控制框架,从策略配置、数据结构、系统调用、应用层命令以及访问控制流程等方面真正地实现了DTE完整性保护形式模型。第五,在安全增强L4微内核(SecL4微内核)上实现了DTE完整性保护形式模型的工作基础上,提供SecL4微内核的DTLS,并有效论证了TCB的描述性顶层规范(DTLS)和模型的一致性。  
其他文献
航拍目标检测是利用目标检测算法检测航拍图像中的特定目标的技术,是计算机视觉领域的重要问题之一。航拍目标检测在军事目标智能识别,遥感影像解析以及民用航空等领域具有广阔
当下,网络已经成为很多人工作生活中不可或缺的一部分,而拥有社交网络账号的用户也日益增多,一个人拥有多个网络账号(马甲)的现象普遍存在,并且马甲日渐成为一种危害网络安全与和谐
周总理十分关心知识分子,他常到老学者、老画家……家里走访慰问。关于周总理与我的父亲齐白石交往的故事有许多,但有一件事,几十年来始终深深铭刻在我的心头,总是让我难以忘
项目组合优化是企业项目组合管理中重要的一步,它从满足条件的多个项目组合中选出最可能的最优组合,以便企业做出决策。在IT项目管理中,同样存在软件项目的投资组合优化问题。本
我们通过借鉴硬件系统的成熟经验和技术——故障树分析法,在综合分析比较国内外相关领域最新研究成果的基础之上,就故障树分析法在系统可靠性指标分配,故障树的形式化构造模
  基于移动通信的远程监控系统现阶段已广泛应用于工业控制领域。在这些应用中,监控系统多使用SMS短消息作为数据传输手段。由于SMS短消息本身具有较大的延迟和数据丢失现象
普适计算是继主机计算模式、桌面计算模式之后发展起来的新的计算模式,其本质特征是实现物理空间与信息空间的融合和计算对人透明,普适计算中信息空间和物理空间的融合可以在不
MDA是由OMG提出的一种以模型为主要开发产品的软件开发方法。开发人员首先建立与具体技术平台的实现细节无关的高抽象程度的平台无关模型(Platform Independent Model,PIM)。
随着企业信息化的发展,企业内部已经建立了许多信息系统,如财务系统、客户系统、FRP、CRM等,由于各个应用系统各自独立、相互隔离,导致了大量信息孤岛的出现,应用系统之间无法沟通
随着社会的进步和发展,人们不断涉及和需要解决很多复杂的实际应用问题,图像匹配问题是数字图像处理的一个重要的领域,它广泛应用在卫星与导弹的制导与导航和机器识别等诸多领域