Design And Implementation Of A Verification Framework For Preemptive OS Kernels

Computer systems have been widely used in a lot of key areas, like national de-fense, financial industry and communication systems. How to build high confidence systems has become an important research topic. As the core underlying software of computer system, the security and reliability of operating system (OS) kernels are very important.Formal verification is an important way to guarantee that a OS kernel is free of programming errors and has been widely used in a lot of OS kernel verification projects. There are many problems in OS verification, like C inline assembly, large code base, interrupt, preemption and so on. Preemption, on the one hand, is crucial for real-time embedded systems, but on the other hand requires careful implementation of interrupt handlers, synchronization primitives and task scheduling, resulting in highly concurrent and complex kernel code.Most of the OS kernel verification projects are based on refinement verification, while compositional proof technique for concurrent program refinement remained un-proposed until recent years. So concurrency and preemption are avoided in all the projects. Existing compositional proof technique for concurrent program refinement and interrupt verification are based on simplified models, they cannot be used for OS kernel verification directly. This dissertation explores how to apply existing composi-tional refinement verification technique and interrupt verification technique in preemp-tive OS kernel verification and makes several contributions.First, we models the correctness of API implementations in OS kernels as contex-tual refinement of their abstract specifications. In order to verify the refinement relation, we adapt existing theories on interrupt verification and contextual refinement of con-current programs, and integrate them into a framework for real-world preemptive OS kernel verification. The framework consists of three parts:(1) modeling of OS ker-nels; (2) a program logic CSL-R for refinement verification of concurrent kernel code with multi-level hardware interrupts; (3) automated tactics for developing mechanized proofs.Second, we have successfully applied the framework to verify key modules of a commercial preemptive OS μ.C/OS-II [1](around 3450 lines of C code with comments and empty lines), including the scheduler, interrupt handlers, message queues, and mu-texes etc. We also verify the priority-inversion-freedom (PIF) in μC/OS-II. Our work is the first to verify the functional correctness of a practical preemptive OS kernel with machine-checkable proofs. It is worth nothing that, unlike existing works that are all focused on systems newly developed with verification in mind, we take a commercial system developed by an independent third-party and verify the code with minimum modification, which demonstrates the generality and applicability of our framework.Finally, all the proofs are mechanized in Coq [2]. The whole proof package is about 225,000 lines of proof script. This is the first mechanized proof of the core modules for a commercial real time OS kernel.