操作系统的形式化建模与验证技术

1. 成果简介

操作系统是嵌入式系统的重要组成部分，系统能否正确地提供服务不仅仅依赖于软件本身的正确性，还依赖于底层操作系统的正确性。在航空航天领域的应用中，很多安全攸关嵌入式系统既要满足它们的功能要求，又需要满足很多系统级的安全性质。我们提出了基于交互式定理证明的微内核嵌入式操作系统的形式化建模和验证技术，同时涵盖形式模型和代码层次，保证操作系统内核模型和代码实现的一致性，为操作系统设计提供可靠的保证。

对操作系统的验证技术包括以下方面：（1）人工分析待验证的操作系统模块，理解代码结构和功能。（2） 定义系统实现程序语言的形式语义，在此基础上为待验证的模块定义等价于其代码实现的形式模型。（3）定义抽象规范描述语言，为待验证的模块建立上层抽象规范。（4） 基于并发精化程序逻辑，在 Coq或Isabelle 中证明代码实现和抽象规范之间的精化关系。（5）定义模块的功能正确性以及无优先级反转、信息流安全性等系统级性质，并通过逻辑证明抽象规范满足这些需求性质。由于精化关系的成立，系统的代码实现也保证满足这些需求性质。我们设计了自动证明策略，来提高逻辑验证的自动程度。针对实时性质的验证，我们用静态分析方法对操作系统函数进行最坏执行时间分析，开发了一套针对国产DSP芯片的分析工具 Xihe。

2. 技术创新点

该成果首次能够对工业级微内核操作系统的整个实现代码进行形式建模和验证，并能够验证并行、中断等复杂行为存在的多核操作系统。

3. 技术成熟度

该成果当前处于中试阶段（工程化验证）。我们验证了航天嵌入式领域微内核操作系统的正确性，覆盖了微内核操作系统的所有功能模块，保障了操作系统内核的功能正确性、实时性和信息安全性。验证过程中发现20余类错误，均在新版本操作系统代码中得到修改并通过验证。

4. 可应用领域

该成果可应用于航空航天等安全攸关领域对安全性和可靠性具有高需求的操作系统的设计，或者已有操作系统的安全性验证中。

5. 联系人

王淑灵，wangsl@ios.ac.cn，18612791263