微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑，操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障，造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生，对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误，因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中，互斥量可协调多任务对资源的访问，是一种常用的任务同步方式，其功能正确性对于保障多任务应用的正确性十分关键.本文基于定理证明方法，在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模，给出其接口函数的形式化规范，并实现这些接口函数的功能正确性验证.

Formal Verification of Functional Correctness for Mutexes in a Microkernel

Operating systems are the key foundational components of the software stacks used in many safety-critical scenarios. The tinest error or loophole in the operating system may cause major failures of the overall software system, resulting in huge economic losses or endangering human lives. To reduce the number of such accidents, it is necessary to verify the correctness of the operating system. Traditional validation methods such as testing cannot guarantee the exhaustive detection of the potential errors in the target system. Hence, it is necessary to use formal methods based on strict mathematical theories for the verification of operating systems. In an operating system, mutexes are used to coordinate the access of shared resources by tasks --- they are a typical means of task synchronization. The functional correctness of mutexes is key to the correct functioning of multi-task applications. Based on the theorem proving method and in the Coq proof assistant, this paper formalizes the code of the mutex module of a preemptive microkernel, gives the formal specifications of the interface functions of this module, and formally proves the functional correctness of these interface functions.