A Practical Verification Framework for Preemptive OS Kernels

CertiuCOS2 · CAV 2016 · Rocq 9.2 port
Source code and project README on GitCode

Research overview from CAV 2016

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]

Source code and Rocq build

The current CertiuCOS2 repository on GitCode contains the research framework, uC/OS-II specifications and proofs, and the Rocq 9.2 port. All 224 proof source files are included in the build and independent kernel-checking targets.

• Project README: project overview, supported toolchain, build and verification commands, and a guide to the source tree.
• Verification scope and trust boundary: the port preserves the original theorem statements and assumptions. The README documents inherited axioms and known model limitations; successful kernel checking does not establish the consistency of those assumptions.

Original CAV 2016 artifact

These materials document the original Coq development. Use the GitCode README above for the current Rocq build.

• Original README: historical code structure and compilation instructions.
• Original VirtualBox image (archival links; unavailable when checked in October 2026): CAV_CertiOS.ova (zipped).
• Browse the original Coq development online. Proofs are hidden in this historical rendering. The current expanded proof development is maintained in the GitCode repository.

Paper authors (affiliations in 2016)

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