航天器嵌入式安全攸关微内核操作系统形式化验证技术研究

Micro-kernel operating systems have been widely adopted in many safety-critical applications, including aerospace systems. OS being one of the most fundamental layers of software systems, a single bug or loopholes may cause the crash of all the applications running above it. Therefore its safety and security is the prerequisite to fulfill the “zero-defect” requirement of safety-critical systems. Formal verification has been viewed as a promising technique to ensure the safety and security of OS kernels, and has been a hot research topic in recent years...In this project we plan to study the general methodology, theories and tools to formally verify safety-critical embedded micro-kernel operating systems. We would build models for all the stages of the system development, including models for requirements, design and implementation. Then we formally specify system requirements and key properties in the models of different abstraction levels. We use the contextual refinement theory as a general verification framework to establish the refinement between the high-level system requirements and the low-level executable code of the OS kernel. The full formalization and verification will be done in the proof assistant Coq, which can be used as a unified foundational logical framework. Based on this foundational logic, we can on the one hand reuse or develop various domain-specific theories and tools, and on the other hand to support their interaction and integration to provide rigorous safety and security guarantees for the whole system. Given the methodologies, theories and tools, we will verify SpaceOS, an embedded micro-kernel real-time OS that has been widely deployed in spacecrafts.

在众多安全攸关领域，包括航天领域，微内核操作系统被广泛部署在各类设备和应用中。由于其基础地位，操作系统的缺陷和漏洞将会导致运行于其上的应用崩溃，因此其可靠性和安全性是实现安全攸关系统“零缺陷”的前提。形式化验证则被认为是严格保证操作系统内核高度可靠和安全的有效手段，是当前研究的热点。本项目拟以国家航天科技重大专项需求为背景，研究安全攸关微内核嵌入式操作系统形式化验证的一般性方法、理论和工具。在需求、设计和代码等不同抽象层次构造内核模型，形式化定义系统规范和关键性质。开发基于上下文精化验证的开放式统一理论框架，建立涵盖最高层需求到可执行代码之间的一致性关系；以定理辅助证明工具Coq作为统一的基础逻辑平台，复用和开发多种领域专用验证理论和工具，并支持不同理论和工具之间的交互和集成。基于上述方法、理论和工具，开展实用的嵌入式航天操作系统SpaceOS内核的验证，给出航天领域的示范性应用。

本项目以国家航天科技重大专项需求为背景，围绕操作系统从需求到代码实现各阶段进行建模并验证、提出统一精化理论框架贯穿各抽象层次的一致性验证、开发操作系统底层模块验证理论及工具，将各种验证理论和工具统一在基础逻辑框架中，实现完整系统的验证。具体研究内容包括：.1)分阶段、分层次的操作系统内核的形式化建模，以及关键性质的形式化规范和验证； .2)基于上下文精化验证的统一理论框架；.3)针对操作系统特定底层模块的专用验证理论和工具；.4)轻量级的程序分析和验证工具的开发，以提高验证效率；.5)多种验证理论和工具在统一逻辑框架Coq上的交互和融合。.本项目通过深入研究，在理论与方法、工具和操作系统验证上取得了突出进展。.1）在理论方法方面，提出了分阶段、分层次的操作系统形式化验证方法，降低了大规模操作系统软件形式化验证的复杂度，便于在实际工程广泛应用；提出了上下文精化统一理论框架，实现贯穿需求、设计和实现三个阶段的一致性验证；提出了C语言和汇编混合代码验证方法，建立了汇编语言的操作语义，实现对操作系统底层硬件抽象层的验证；.2）在工具方面，基于领域知识设计轻量化工具及策略，并在统一逻辑框架下集成；使得用不同理论和工具建立的可信结论可以在共同的语义模型下组合，推导出完整系统的可信结论。.3）在操作系统验证方面，实现了首个支持抢占式多任务调度及多级中断的航天器实际部署的SpaceOS（天卓）操作系统的全面形式化验证。.发表了相应的高水平论文53篇，申请专利14项，软件著作权8项，撰写技术报告12份。其中，获得2019年度PLDI杰出论文奖，为40年来中国大陆科研院所第一作者单位首次获奖，在国内外产生了重要学术影响。.本项目提出的理论方法，为解决复杂大规模软件形式化验证提供了一种验证途径，具有重要的科学意义。验证的操作系统在我国载人航天、探月工程、火星探测、北斗导航等为代表的重大航天工程中应用，为航天任务的成功作出了重大贡献，具有重要的政治、经济和社会效益。