A Practical Verification Framework for Preemptive OS Kernels

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 uC/OS-II, including the scheduler, interrupt handlers, message queues, and mutexes, etc. We also verify the priority-inversion-freedom (PIF) in uC/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.

Paper

• A Practical Verification Framework for Preemptive OS Kernels.
  Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li.
  In CAV 2016 (July 2016)
  [Paper][TR][Slides]

Implementation

• README.txt : this file describes the code structure and compilation instructions for the entire Coq package. Please read it first and download the Coq package from the links given as below. "README.txt" can also be found in the Coq package.


• Download our Coq implementation (packaged as a VirtualBox virtual machine) from : CAV_CertiOS.ova (zipped)


• Browse the Coq development online
  (Here proofs are hidden for readability, and the complete proofs can be found in the Coq package.)

People

• Fengwei Xu, USTC
• Ming Fu, USTC
• Xinyu Feng, USTC
• Xiaoran Zhang, USTC
• Hui Zhang, USTC
• Zhaohui Li, USTC