206
15 mars 2018 - 14h00
Extending a verified OS kernel for real-time
par Lionel Rieg de Yale University
Abstract: The CertiKOS operating system is a verified OS kernel, written in C and proven in Coq. Leveraging CompCert, it provides end-to-end correctness proofs all the way down to the generated assembly code. It is designed into many abstraction layers that isolate the various components of the OS and permit to abstract reasoning on the actual code into reasoning on its specification.
My current work aims at extending it into a real-time kernel. In this talk, I will present the modifications we are currently working on and the associated verification challenges: introducing preemptive interrupts to create a timer, switching from a cooperative round-robin scheduler to a preemptive priority-based one, linking the schedulability proof of the task set to the state of the scheduler, updating the information flow non-interference proof. Along the way, I will detail our notion of virtual time, used in the schedulability proof and which we hope will be useful in a broader context.
