Microkernel Verification Down To Assembly
When constructing systems with high assurance requirements, it is desirable to build on a formally verified trusted computing base, such as the seL4 microkernel. The verification of seL4 guarantees correctness down to the kernel's C implementation and relies on the correctness of the C compiler used. CompCert, a verified C compiler, has the potential to extend these guarantees to the level of assembly. We have made significant modifications to seL4, which has previously only been compiled with variants of GCC, in order to make it compatible with CompCert. The poster proposed will discuss the challenges that have been encountered, some lessons learnt and what we hope to gain from this approach. The contribution of this work is a first step towards our overall aim of the formal verification of a microkernel from a C implementation down to an assembly implementation. To our knowledge, this will be the first proof of functional correctness of a general-purpose operating system kernel down to assembly. The main achievement thus far is applying CompCert to seL4, during which we have already learnt some valuable lessons.
Keywords: seL4, CompCert, microkernel, formal verification