A Practical Verification Framework for Preemptive OS Kernels

The Verification Framework

Modeling Preemptive OS Kernels

• memory.v : the C memory model
• language.v: the low-level language for a practical subset of C, and the high-level specification language
• opsem.v: the operational semantics for the low-level and high-level languages

Refinement-based Program Logic

• assertion.v: the assertion language
• inferules.v: the inference rules
• soundness.v: the soundness proofs of the inference rules
• toprule.v: the top rule and the soundness theorem of the verification framework
• simulation.v: definitions of compositional simulation relations, which are employed as the underlying semantics for proving the soundness of the program logic
• toptheorem.v : OS correctness definition and auxiliary compositionality lemmas

Automated Tactics Support

• derivedrules.v : derived inference rules based on "inferules.v" for developing automated tactics
• aux_for_hoare_lemmas.v & hoare_assign.v & hoare_conseq.v & hoare_lemmas.v & hoare_tactics.v & symbolic_execution.v : the coq files for the tactic "hoare forward", which is used to automatically generate verification conditions
• lemmasforseplog.v& seplog_lemmas.v & seplog_tactics.v & tacticsforseplog.v : the coq files for the tactic "sep auto" and its variations, which are used to prove entailments of relational assertions
• IntLib.v & mathsolver.v: the coq files for tactics "int auto" and "mauto", which are used to automatically prove the mathematical properties of machine integers involved with bit operations

Verifying uC/OS-II

• kernel code: notations, macros, Coq definitions for the C code of key modules of uC/OS-II
  • os_q.v : Message Queue
  • os_sem.v : Semaphore
  • os_mbox.v : Mailbox
  • os_mutex.v : Mutex
  • os_time.v : Time Management
  • os_cpu_a.v : Timer Interrupt （Id : 0) & Pseudo Interrupt (Id : 1)
  • os_core.v : Internal Functions
• specifications: the specifications for uC/OS-II and PIF proofs
  • OSQInvDef.v & OSTCBInvDef.v : global invariants for specifying the shared resources between interrupt handlers and non-handler code
  • absop.v : the specification code written with our specification language for specifying kernel APIs and interrupt handlers of uC/OS-II
  • InternalFunSpec.v : specifications of internal functions
  • absop_rules.v : abstract implication rules of abstract operations
  • PIF_def.v : the definition of priority-inversion-freedom (PIF)
• refinement proofs: refinement proofs for internal functions, APIs and interrupts (e.g. OSTimeDlyProof.v )
• ucos_correct.v: two final theorems, which are for the functional correctness of APIs (as contextual refinement) and PIF of mutexes (no nested use) in uC/OS-II, respectively