Mechanized Verification Of Preemptive Os Kernels (Invited Talk)

We propose a practical verification framework for preemptive OS kernels. The framework models the correctness of API implementations in OS kernels as contextual refinement of their abstract specifications. It provides a specification language for defining the high-level abstract model of OS kernels, a program logic for refinement verification of concurrent kernel code with multi-level hardware interrupts, and automated tactics for developing mechanized proofs. The whole framework is developed for a practical subset of the C language. We have successfully applied it to verify key modules of a commercial preemptive OS C/OS-II, including the scheduler, interrupt handlers, message queues, and mutexes, etc. We also verify the priorityinversion- freedom (PIF) in ae C/OS-II. All the proofs are mechanized in Coq. To our knowledge, our work is the first to verify the functional correctness of a practical preemptive OS kernel with machine-checkable proofs. More details about the project is available at http://staff. ustc. edu. cn/similar to fuming/research/certiucos/