安全操作系统是保障信息安全的重要基础设施。由于其自身的复杂性，如何对安全操作系统进行测评以确保其能达到所声称的安全需求一直是科研界和工业界所关注的热点。但从安全操作系统测评的现有研究和相关标准来看，还存在下列一些不足:现有测评标准中使用的方法难以覆盖操作系统中所有的安全状态;对于新型计算环境下安全操作系统安全功能的测评方法研究不足;针对安全操作系统的缺陷检测技术不够成熟。本文以“方德方舟安全操作系统NFSARKV2.0”和“面向访问验证保护级的安全操作系统原型系统”的开发实践中遇到的问题为基础，针对安全操作系统测评的关键技术进行研究，取得了以下五个方面的研究成果:　　 第一，研究将静态分析技术应用于安全操作系统的测评，对CC标准和GB/T20271标准中主要依靠测试方法来实现安全操作系统安全保障的现状进行了补充。提出了适合操作系统的静态分析方法，并在“方德方舟安全操作系统NFSARKV2.0”和“面向访问验证保护级的安全操作系统原型系统”的前期内部测评中进行了实施。　　 第二，研究了安全操作系统的应用场景从传统平台扩展到虚拟化平台以后系统安全功能的验证问题。结合虚拟化环境中两级强制访问控制并存的特点，给出了虚拟机监控器的强制访问控制框架XSM和Linux操作系统的强制访问控制框架LSM中钩子函数放置正确性的验证方法，提出了相应的建模方法和分析算法，并对“方德方舟安全操作系统NFSARKV2.0”和“面向访问验证保护级的安全操作系统原型系统”的具体实现进行了分析，验证了其强制访问控制框架的正确性。　　 第三，研究了虚拟化环境下系统安全策略的验证方法。针对虚拟化平台中两级多个安全策略并存的特点，提出了一种基于信息流的多层次策略分析方法。利用层次式的分析方法，首先分析顶层虚拟机监控器安全策略的正确性，然后分析下层虚拟机安全策略的信息流之间的交叉点，实现跨虚拟机的信息流分析，通过分析其中是否存在非法信息流，验证安全策略是否满足系统的安全目标。　　 第四，提出了一种新型的文件系统中TOCTTOU缺陷的检测方法。针对类Unix操作系统的文件系统中普遍存在的TOCTTOU缺陷，分析了文件系统中TOCTTOU缺陷的成因并完备的列举了所有的TOCTTOU缺陷对，实现了对文件系统中TOCTTOU缺陷的建模，设计了文件系统中TOCTTOU缺陷的检测算法，并且给出了原型实现。实验表明，和现有工作相比，本文提出的方法明显降低了误报。　　 第五，针对操作系统中普通存在的空指针解引用缺陷，提出了一种空指针解引用缺陷的检测方法。用数据流分析的方法，研究空指针在程序中的值流动，并结合控制流图，实现了路径敏感的分析，并在“方德方舟安全操作系统NFSARKV2.0”的源代码中发现了多个相关安全缺陷，经过人工分析，排除误报之后，对确认的安全缺陷在系统提交正式测评之前进行了修复。　　 总之，本论文的研究解决了安全操作系统测评中的一些关键问题，为安全操作系统测评中涉及的安全功能的验证方法和安全缺陷的检测技术进行了探索，取得了一定的成果，为安全操作系统的设计与实现提供了丰富的参考。