基于模型检测的安全操作系统验证方法研究

基于模型检测的安全操作系统验证方法研究

论文摘要

安全操作系统的形式化验证,作为高等级安全操作系统评估准则的一项重要指标和操作系统安全性能最有效的证明手段,具有重要意义与实用价值。目前形式化验证主要分为模型检测和定理证明两大类方法。本论文集中探讨了模型检测技术在安全操作系统验证各个层次中的一些关键问题,主要工作和创新成果如下:首先,针对SELinux策略配置复杂难以分析的问题,提出了一种基于模型检测的SELinux策略分析方法,以验证策略实施与安全需求之间的一致性问题。采用扩展的标签迁移系统,将MLS策略和普通TE-RBAC策略的描述融入到统一的描述框架下,并完整定义了策略配置语句的信息流属性,不仅考虑了型访问规则造成的信息流动,也兼顾了型转移以及MLS约束对策略模型信息流的影响。设计了一种新型的安全需求描述语言,将安全需求与和策略配置剥离开,使安全需求的描述不依赖于对实施细节的了解,扩展了模型检测器探索未知漏洞的能力。其次,提出了安全模型与安全需求的一致性验证方法。利用UML类图和状态机图在系统动、静态建模方面的表达能力,设计了一种新的安全模型UML描述方式。并在此基础上给出了UML图的状态机语义,将UML模型编译成模型检测器的规范语言,使用模型检测分析安全模型的性能。这一成果使利用自动化工具辅助安全模型的正确性验证成为可能,减少了传统安全模型验证方法中对验证人员形式化理论的过高要求以及繁重的手工推导过程。最后,探讨了安全验证中测试集的优化问题。提出简并测试集的概念,将测试冗余从状态扩展到状态迁移,将测试集中的冗余归为最小。在此定义的基础上,我们以模型检测作为后端的搜索引擎,给出简并测试集的生成算法。首次讨论了在测试集和系统实现相悖时对测试结果的判定。并据此对算法加以改进,使得在不影响测试集生成的前提下,即使测试失败,测试人员也可以准确地对失败位置进行定位。

论文目录

  • 摘要
  • Abstract
  • 目录
  • 第1章 引言
  • 1.1 选题背景与意义
  • 1.2 安全操作系统形式化验证的发展历史
  • 1.3 论文框架与研究目标
  • 1.3.1 论文框架
  • 1.3.2 论文研究目标
  • 1.4 论文主要研究内容和结构安排
  • 第2章 安全操作系统的形式化验证
  • 2.1 安全模型的形式化描述
  • 2.1.1 安全策略与安全模型
  • 2.1.2 BLP模型
  • 2.1.3 Biba模型
  • 2.1.4 TE模型和DTE模型
  • 2.1.5 RBAC模型
  • 2.1.6 小结
  • 2.2 形式化安全验证技术及模型检测
  • 2.2.1 系统建模
  • 2.2.2 LTL和CTL
  • 2.2.3 模型检测
  • 2.3 本章小结
  • 第3章 基于模型检测的SELinux策略统一信息流验证方法
  • 3.1 SELinux简介
  • 3.1.1 SELinux框架
  • 3.1.2 SELinux策略模型与描述语言
  • 3.2 SELinux策略的形式化建模
  • 3.2.1 策略规则的形式化描述
  • 3.2.2 策略模型的Kripke结构
  • 3.2.3 授权关系与信息流
  • 3.3 安全需求描述
  • 3.3.1 安全需求描述设计原则
  • 3.3.2 安全需求分析
  • 3.3.3 安全需求描述语言的设计
  • 3.3.4 SELinux的安全需求描述语言实现
  • 3.4 模型检测实例
  • 3.4.1 web server策略分析
  • 3.4.2 军队采购系统策略分析
  • 3.5 本章小结
  • 第4章 基于模型检测的安全模型验证方法
  • 4.1 模型验证框架
  • 4.2 安全策略模型的描述
  • 4.2.1 UML简介
  • 4.2.2 安全策略模型的UML描述
  • 4.3 模型描述的状态机语义
  • 4.3.1 UML状态机的抽象语法
  • 4.3.2 UML的配置和复合迁移
  • 4.3.3 Run-to-Completion语义
  • 4.3.4 UML到PROMELA模型的转换
  • 4.4 安全公理的描述
  • 4.5 两个BLP改进模型的验证
  • 4.5.1 DBLP的UML建模
  • 4.5.2 SLCF的UML建模
  • 4.5.3 安全需求的描述
  • 4.5.4 实验结果分析
  • 4.6 本章小结
  • 第5章 基于安全状态迁移的简并测试集生成方法
  • 5.1 测试用例化简方法的分析
  • 5.1.1 基于模型检测的测试用例化简框架
  • 5.1.2 现有测试集优化技术分析
  • 5.1.3 基于状态迁移的用例化简
  • 5.2 简并测试集的形式化定义
  • 5.3 简并测试集生成算法
  • 5.3.1 DTS生成算法
  • 5.3.2 DTS生成算法的改进
  • 5.4 算法测试与分析
  • 5.4.1 算法测试
  • 5.4.2 算法分析
  • 5.5 本章小结
  • 第6章 结束语
  • 6.1 论文主要成果
  • 6.2 未来工作展望
  • 附录A SELinux权限映射
  • 附录B 军队采购系统的策略配置
  • 参考文献
  • 致谢
  • 在读期间发表的学术论文与取得的研究成果
  • 相关论文文献

    • [1].主机操作系统安全防护研究与实践[J]. 智能建筑 2017(09)
    • [2].关于高安全操作系统的安全核技术的研究[J]. 福建电脑 2009(03)
    • [3].以安全操作系统为依托为云应用构建“安全云”环境[J]. 信息安全与技术 2012(05)
    • [4].应用嵌入式安全操作系统的框架设计[J]. 电力系统通信 2008(10)
    • [5].基于安全操作系统的继电保护信息管理系统安全防护优化及应用[J]. 水电与抽水蓄能 2018(06)
    • [6].国标四级安全操作系统的内存泄露分析方法研究[J]. 信息网络安全 2011(06)
    • [7].QNX汽车安全操作系统全面上市[J]. 汽车与安全 2014(12)
    • [8].安全操作系统渗透测试方案研究[J]. 电子产品可靠性与环境试验 2013(S1)
    • [9].浅析云平台安全操作系统关键点[J]. 数码世界 2017(10)
    • [10].一个高安全等级操作系统的总体设计[J]. 计算机安全 2014(09)
    • [11].Linux操作系统安全策略的研究[J]. 中国电力教育 2008(S3)
    • [12].基于uC/OS-Ⅱ的嵌入式安全操作系统的框架设计[J]. 广东输电与变电技术 2008(06)
    • [13].基于国产安全操作系统的集中存储管控系统[J]. 计算机系统应用 2016(10)
    • [14].Qubes安全操作系统的研究和改进[J]. 计算机与现代化 2013(04)
    • [15].加强云防护,Palo Alto Networks全面强化安全平台[J]. 中国信息安全 2017(04)
    • [16].Linux安全操作系统的研究与改进[J]. 电子质量 2017(04)
    • [17].QNX汽车安全操作系统满足日益增长的需求[J]. 中国电子商情(基础电子) 2014(12)
    • [18].以安全操作系统为依托 构建可信云计算环境——椒图科技发布JHSE安全云解决方案[J]. 计算机安全 2012(05)
    • [19].安全操作系统中的功能隔离机制[J]. 中国科学院研究生院学报 2008(04)
    • [20].Check Point推出GAiA统一安全操作系统[J]. 通讯世界 2012(05)
    • [21].国产嵌入式安全操作系统技术[J]. 数字技术与应用 2019(04)
    • [22].QNX全新操作系统提高汽车安全性[J]. 现代零部件 2014(10)
    • [23].自主沦为自恋[J]. 商界(评论) 2014(02)
    • [24].QNX推出针对汽车安全性的全新操作系统[J]. 商用汽车 2014(Z1)
    • [25].通用型安全操作系统解决方案浅析[J]. 信息安全与技术 2012(02)
    • [26].安全操作系统的体系结构及其实现模型[J]. 商业故事 2015(19)
    • [27].国产安全操作系统的安全配置实时监测技术研究[J]. 东北电力技术 2018(04)
    • [28].基于TPM的安全嵌入式系统的设计研究[J]. 电脑知识与技术 2010(21)
    • [29].基于可信计算平台的可信动态客体监管系统的设计与实现[J]. 计算机科学 2008(01)
    • [30].基于代码路径的安全操作系统性能优化方法[J]. 计算机系统应用 2015(08)

    标签:;  ;  ;  ;  ;  ;  

    基于模型检测的安全操作系统验证方法研究
    下载Doc文档

    猜你喜欢