7.500 lines of C, 1 microkernel, formally proved correct
Speaker(s) : June Andronick - Researcher - NICTA (National ICT Australia)
NICTA's L4.verified project has just successfully achieved the first formal verification of functional correctness of a full microkernel, namely seL4 (secure embedded L4). The seL4 microkernel aims to be a high-performance, secure and verified microkernel. It builds on the strengths of the L4 microkernel architecture, such as small size and high performance, and extends it with a built-in capability-based security model. It has been designed and developed, within NICTA, with formal verification in mind and in parallel to the verification work. The L4.verified project provided a mathematical, machine-checked proof, in Isabelle/HOL, of the functional correctness of seL4, with respect to a high-level, formal description of its expected behaviour. This makes seL4 the world's first formally verified general purpose OS kernel.
I will present the motivation and architecture of the project. I will then detail the formal refinement approach, from the high-level specification down to the high-performance C implementation, and present the verification framework developed for large-scale verification of C programs correctness. I will finally sketch the results and experience of this project and describe our future challenges in the Trustworthy Embedded System Group.