A Practical verification Framework for Preemptive os Kernels Fengwei Xu Ming Fu Xinyu Feng Xiaoran Zhang Hui zhang Zhaohui Li University of Science and Technology of China Jy22,2016CAV2016 http://staff.ustcedu.cn/-fuming/research/certiucos/
A Practical Verification Framework for Preemptive OS Kernels Fengwei Xu Ming Fu Xinyu Feng Xiaoran Zhang Hui Zhang Zhaohui Li University of Science and Technology of China July 22, 2016 CAV2016 http://staff.ustc.edu.cn/~fuming/research/certiucos/
Motivation of os verification Computer System
Motivation of OS Verification Computer System
Motivation of os verification Applications Operating System Hardware Correctness of OS is crucial for safety and security of the whole system
Motivation of OS Verification Hardware Operating System Applications Correctness of OS is crucial for safety and security of the whole system
Challenges of os Verification Many challenges AsSembly code Concurrency Preemption Interrupts Large code base Device&v/o Concurrency caused by preemptions is particularly challenging
Challenges of OS Verification Many challenges: Preemption … Concurrency C/Assembly code Interrupts Large code base Device & I/O Concurrency caused by preemptions is particularly challenging
Preemption Preemption is the act of temporarily inter nested multi-level t requiring its cooperation interrupts Hand ler 1 Handler 0) Task A Kernel-Level iret preemption cli switch preempt Task B Handler 1 Handler 1 cli switch iret iret s switch iret Preemptions and multi-level interrupts are indispensable to achieve real-time guarantees in rtos Preemptive os kernel is highly concurrent and complex
Preemption Preemptions and multi-level interrupts are indispensable to achieve real-time guarantees in RTOS. Preemptive OS kernel is highly concurrent and complex. . . . . . . cli . . . switch . . . sti . . . Task A . . . sti Handler 1 iret. . . Handler 0 . . . . . . cli . . . switch . . . sti . . . Task B . . . cli . . . switch . . . iret . . . sti . . . eoi Handler 1 . . . iret iret. . . Handler 1 Kernel-Level preemption Preemption is the act of temporarily interrupting a task without requiring its cooperation. nested multi-level interrupts
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