操作系统内核中线程管理与中断管理的验证研究

Thread management and interrupt management are the essential parts of operating system kernels. Providing the multithreading mechanism at the lowest level of kernels, they are obviously critical to the safety of computer systems. Since the concurrency and the intricate design, these parts of code are extremely hard to verify formally. Although a large amount of research work has been done for verifying OS kernels, the thread management and interrupt management are usually serialized, or over-simplified to verify. As a result, previous work is unable to applied to verify reaslistic thread management and interrupt management of some of modern OS kernels, like Linux, FreeRTOS and so on. In this proposal, we propose a research project for verifying the thread management and interrupt management of some realistic OS kernels with multi-core support, where the kernel code runs concurrently with sophisticated control flows. We plan to work on the theoretical aspect of verifying the thread management and interrupt management with multi-core support, methodolgy of describing the formal semantics of OS kernels, program logics for reasoning about the safety of kernel code. We also plan to verify the thread management and interrupt management of a realitic embedded OS kernel- - FreeRTOS. We hope that the theoretical result of our project will be an important basis for building safe and reliable OS kernels in the future.

操作系统内核的线程管理与中断管理是内核的主要组成部分。它们位于内核的最底层，为上层的内核代码提供多线程机制，其安全性对于整个计算机系统至关重要。这部分代码由于并发性与内在复杂性，为形式化验证内核带来了一些验证难题。而国内外的一些操作系统内核验证工作也对这部分代码研究不足，他们或验证串行执行的线程管理代码，或过度简化这部分功能，因此无法适用于主流内核中的线程管理与中断管理代码，如FreeRTOS与Linux等。本项目拟针对当前研究的不足，深入分析实际的操作系统内核中的并发特性，探索研究支持多核的内核线程管理与中断管理部分的语义描述与验证的一般性方法与理论，并应用这些理论方法来验证一个实际的但规模相对较小的嵌入式操作系统内核FreeRTOS的线程管理与中断管理部分。本项目研究的操作系统内核中的并发代码的验证方法、相关理论与技术对高可信计算机系统的构建有着一定的理论价值与科学意义。

如今计算机系统已在国防、通讯、金融、能源、交通、医疗等关键领域中得到广泛应用，构建高可信系统已成为世界范围的重要课题。其中操作系统内核的安全可靠性是构建高可信计算机系统的关键，因为任何一个微小的内核错误都有可能导致整个计算机系统崩溃。此外随着系统软件内核的并行化、复杂化与追求高性能的发展趋势，内核的可靠性显得更加重要。然而现实情况却不容乐观，全球范围内不断发现和公布的内核漏洞与设计缺陷时刻威胁着众多安全攸关的计算机系统。.操作系统内核的线程管理与中断管理是内核的主要组成部分。它们位于内核的最底层，为上层的内核代码提供多线程机制，其安全性对于整个计算机系统至关重要。这部分代码由于并发性与内在复杂性，为形式化验证内核带来了一些验证难题。而国内外的一些操作系统内核验证工作也对这部分代码研究不足，他们或验证串行执行的线程管理代码，或过度简化这部分功能，因此无法适用于主流内核中的线程管理与中断管理代码。.本项目针对这类问题，主要在以下几个方面做了深入地研究：.(1)深入地分析了实际的操作系统内核中的并发特性，研究支持多核的内核线程管理与中断管理部分的语义描述与验证的一般性方法与理论。.(2)深入地研究了虚拟化系统中中断处理，中断调度，中断注入的形式化语义以及进行形式化验证的方法。.本项目的研究的成果包括：.(1)提出了一种在汇编语言级来验证操作系统内核中中断管理，线程管理，多核支持的统一验证框架和验证方法。.(2)提出了一种验证虚拟化监视器中中断处理，中断管理，中断注入的验证方法。.(3)提出了一种验证方法，来验证操作系统内核中内核抢占，抢占开关控制特性，以及它们与中断控制和线程调度之间的关系。.本项目的研究成果给出了操作系统内核几个重要特性或模块的验证方法和思路。而操作系统内核验证将在不久的将来为我国的航天、核电、医疗设备的高可信软件系统的构建过程中发挥极其重要的作用。