跨平台的操作系统安全机制形式化验证方法研究

针对现阶段操作系统安全机制分析中出现的困难和现有安全策略分析方法中出现的问题，从操作系统的安全机制实施和安全策略配置方法入手，研究通用的访问控制元数据和安全需求的形式化表述方法，建立用于描述系统安全策略配置的数学模型； 同时利用严格的逻辑和验证工具，分析和验证安全需求与安全策略之间的一致性，在此基础上建立安全策略漏洞报告机制，从而以数学模型和相应的验证工具帮助操作系统设计者、管理者和用户更好地理解和分析安全策略，完善系统安全机制的实现和优化。

本课题针对如何对多种操作系统中的不同安全机制进行统一分析的问题进行了研究，在安全目标的统一化描述，安全机制的抽象，验证结果的分析等方面取得了一系列进展和突破，提出了一套跨平台的操作系统安全机制分析方法。其中，在安全需求的形式化描述方法方面，提出了基于信息流的安全需求形式化描述语言SRDL，通过课题开发的SRDL编译器，可将需求输出为两种逻辑分析引擎的输入语言；在安全机制的形式化建模方面，提出了基于Prolog语言的多操作系统安全机制建模方法，可以对目前流行的两类操作系统（Windows和Linux）中的三种安全机制（MIC、SELinux、AppArmor）进行统一的建模；在前两点的基础上，课题组提出了跨平台操作系统安全机制分析方法，并开发了相应的原型工具，对上述三种安全机制进行了验证，并对验证结果进行了整理与分析。项目实施期间，课题组共计发表论文17 篇，申请专利2 项，实现原型系统1套，培养博士毕业生2名，并为5名研究生提供研究方向。总体而言，本课题实现了预期目标，部分指标超过了预期目标。