seL4 in Australia

Abstract

TEN YEARS AGO, the functional correctness proof of the seL4 microkernel marked the first a completed operating system (OS) kernel had been verified to the source-code level.(4) This means there was a machine-checked proof that the implementation in the C language satisfied the kernel's specification, expressed in mathematical logic. Much has happened since then: We have extended the verification to show the kernel enforces desired security and safety properties, we have removed the need to trust the compiler, and we verified implementations for processor architectures other than the original Arm v6. We used experience from deploying seL4 in a number of real-world systems to evolve the kernel and its proofs to support a broader class of use cases, and we have made significant progress toward extending the assurance to systemwide properties. We will provide a brief overview of these developments, as well as ongoing research.