Challenges of concurrent Kerne|∨ erification Verifying concurrent programs is difficult Non-deterministic interleaving Verifying concurrent kernel is more challenging OS verification is usually based on refinement verification Concurrent kernel verification requires combination of verifying refinement and concurrency Difficult to do it compositionally Theoretical problems have not been solved until recently [Liang et al. PLDI13, LICS 14][Turon et al. POPL13, ICFP 13 Concurrency caused by preemptions and multi-level interrupts are avoided by previous Os verification projects e.g. seL4 [Klein et al. SOSP 09, CertiKos [Gu et al. POPL' 15]
Challenges of Concurrent Kernel Verification • Verifying concurrent programs is difficult – Non-deterministic interleaving • Verifying concurrent kernel is more challenging – OS verification is usually based on refinement verification – Concurrent kernel verification requires combination of verifying refinement and concurrency • Difficult to do it compositionally • Theoretical problems have not been solved until recently [Liang et al. PLDI’13, LICS’14] [Turon et al. POPL’13, ICFP’13] Concurrency caused by preemptions and multi-level interrupts are avoided by previous OS verification projects e.g. seL4 [Klein et al. SOSP‘09], CertiKOS[Gu et al. POPL’15]
fact Our Contributions Verification framework for preemptive os kernel Refinement of concurrent kernels Multi-Level interrupts Verification of key modules of a commercial OS kernel uc/OS-l in Coq Micrium Embedded Software rHC OS-I The first mechanized verification of a commercial preemptive os kernel
Our Contributions • Verification framework for preemptive OS kernel – Refinement of concurrent kernels – Multi-Level interrupts • Verification of key modules of a commercial OS kernel μC/OS-II in Coq The first mechanized verification of a commercial preemptive OS kernel
Outline OS Correctness Verification framework Program logic for refinement and multi-level interrupts Verifying uC/OS
Outline • OS Correctness • Verification Framework – Program logic for refinement and multi-level interrupts • Verifying μC/OS-II
OS Correctness Os provides abstraction for programmers Hide details of the underlying hardware Provide an abstract programming model OS Correctness: refinement between high-level abstraction and low-level concrete implementation
OS Correctness • OS provides abstraction for programmers – Hide details of the underlying hardware – Provide an abstract programming model • OS Correctness : refinement between high-level abstraction and low-level concrete implementation
OS Correctness Applications High-Level Abstract machine C+ Abstract primitives Low-Level Abstract Machine High-Level Low-Level Concrete C+Assembly Abstract Primitives Implementations
OS Correctness High-Level Abstract Machine High-Level Abstract Primitives Low-Level Concrete Implementations Applications C + Abstract primitives C +Assembly Low-Level Abstract Machine