【作者】 程亮；

【导师】 冯登国；

【作者基本信息】 中国科学技术大学 ， 信息安全， 2009， 博士

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

【Abstract】 As an important index of high-level operating system evaluation criterion,and the most effective proof of the security property of the operating system,formal verification of secure operating system has great significance and practical value.In the current stage,formal verification can be divided mainly into two classes:model checking and theory proving.This thesis focuses on some key issues of model checking,in each hierarchy of the formal verification framework of the secure operating system. The main work and innovations are listed as follows:Fist,to the problem that SELinux policy configuration is complicated and hard to analyze,a unified information flow analysis of SELinux policies is proposed,which is based on the techniques of model checking.It can be used to verify the coherence of the security requirement and the policy implementations.A labeled transition system is adopted to merge MLS policies and TE-RBAC policies into a unified description framework.A complete definition of information flow property of the policy configuration is given,including the information flow caused by type access rules, type transition rules and especially MLS constraint rules in SELinux policy configuration. Also,a new security requirement description language is designed to strip off the high-level security requirement description from the low-level policy implementation, which makes the requirement representation independent of the detail of policy language and extends the capability to explore unknown vulnerability.Secondly,a coherence verification of security model and requirement is proposed. In the use of the expression of UML class diagram and state machine diagram in the static and dynamic modeling,a new security model description method of UML is designed.The UMLized model is compiled to model checker’s specification language after given the UML diagram’s state machine semantics.Then the requirement,which is also translated to the model checker’s input,can be checked accordingly against to the security model.This achievement makes it possible to verify the correctness of security model semi-automatically and reduces the high requirement of formal methods and the heavy work in the traditional security model verification.Finally,about optimization of test sets in the security verification,the concept of degenerate test set is proposed,considering not only the redundant state,but also the state transition.The generation algorithm is represented then.A discussion is made to determine the algorithm’s effectiveness when test case fails for the first time. After that,an improved DTS generation algorithm is given,which can show the failure location accurately without affecting the efficiency of the algorithm.更多还原