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