小型操作系统内核的轻量级形式化设计和验证方法研究

The consistency among functonality requirements, design and implementation of the operating system, and the correctness and security of the system functionality and implementation, are the two important issues for the security operating system. Due to the complexity of the oprating system framework and formal logic system, the verification for design and implementation of the operating system becomes very difficult. Before, we studied the security structure and functionality of the operating system, and developed a small-scale microkernel operating system prototype - VTOS. This applied project aims to propose an easy-modeling, strong-expressiveness, and convenient reasoning formal method for the design, implementation and verification of the operating system. We plan to build the kernel-hardware model of the operating system for the Intel processor, and based on this model to describe the semantics of the system kernel codes. And we plan to construct the kernel state automaton model, analyse the kernel functionality and security features, and accurately define the kernel state domain. Through establishing the mapping between the kernel domain and the model in the logic system, we describe and define the logic assertions of the kernel functionality correctness and the system integrity. With Isabelle/HOL theorem prover, we can verify whether the implementation of microkernel of VTOS meets the expected logic assertions of functionality correctness and integrity. Meanwhile, we plan to study the feedback mechanism in the process of formal verification, i.e., through the feedback to the system design to ensure the system correctness.

操作系统功能体系需求、设计和实现的一致性，以及功能体系与实现的正确性和安全性是安全操作系统重要的两个问题，由于操作系统框架和形式化逻辑系统的复杂性，对其设计和实现的形式化验证变得非常困难。此前我们对操作系统的安全结构和功能体系进行了研究，开发了一个小型微内核操作系统原型VTOS。本课题旨在针对操作系统设计实现和验证方面提出一种易于建模、描述能力强、推理方便的形式化方法。本申请课题计划针对Intel处理器建立操作系统内核硬件模型，描述系统内核代码的语义；设计内核状态自动机模型，分析内核的功能与安全特性，准确定义系统内核的状态空间，建立内核论域以及与逻辑系统中模型的映射关系，定义内核功能正确性和系统完整性的逻辑断言；借助Isabelle/HOL定理证明器验证VTOS微内核的实现是否满足预期功能正确性和完整性的逻辑断言；研究形式化验证过程中的反馈机制，通过对系统设计的反馈来保证系统的正确性。

本研究在前期对OS形式化设计和验证的研究的基础上，借助Isabelle/HOL定理证明器对微内核从系统功能的正确性和完整性两个方面进行形式化验证。本研究针对Intel处理器建立了OS内核硬件模型，在该模型的基础上描述了OS内核代码的语义；设计和描述了OS内核状态自动机模型，用于分析OS内核的功能与安全特性。准确定义了OS内核的状态空间，并建立了OS内核论域以及与逻辑系统中模型的映射关系，在此基础上研究了OS内核功能正确性的逻辑断言（命题）以及系统完整性的条件，并建立了相应的逻辑断言（命题）；在逻辑系统中验证了微内核的实现是否满足预期的功能正确性和完整性的逻辑断言（命题）；同时，研究了形式化验证过程中的反馈机制，通过对系统设计的反馈来保证系统的正确性，如果在验证过程中发现问题，及时地修改系统设计，最大程度地保证系统的健壮性。研究结果表明，本研究提出的形式化设计和验证的方法是可行的和高效的，可为国产安全可信操作系统提供理论支持。