Intervenant(s) : Harvey Tuch (Embedded, Real-Time and Operating Systems group at National ICT Australia and the Unive
Over the last decade, the L4 microkernel has demonstrated that the advantages of microkernel based systems, such as decomposed system architecture and a reduced trusted computing base, need not impose excess performance overhead. The seL4 and L4.verified projects at NICTA are concerned with the design, implementation and formal verification of a next generation L4, taking a foundational approach to providing support for the functionality and reliability guarantees required for the use of L4 in secure embedded systems.
In this talk a brief overview of seL4 and L4.verified will be provided, and then details of a challenging aspect of kernel verification, supplying semantics and proof abstractions for low-level pointer-based C code and specifications, will be described.
We present a formal model of memory that both captures the low-level features of C's pointers and memory, and that forms the basis for an expressive implementation of separation logic. At the low level, we do not commit common oversimplifications, but correctly deal with C's model of programming language values and the heap. At the level of separation logic, we are still able to reason abstractly and efficiently. We implement this framework in the theorem prover Isabelle/HOL and demonstrate it on two case studies. We show that the divide between detailed and abstract does not impose undue verification overhead, and that simple programs remain easy to verify. We also show that the framework is applicable to real, security- and safety-critical code by formally verifying the memory allocator of the L4 microkernel.