seL4: Formal Verification of an

Doi: 10.1145/1743546.1743574

Operating-System Kernel

By Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood

abstract

We report on the formal, machine-checked verification of
the seL4 microkernel from an abstract specification down to
its C implementation. We assume correctness of compiler,
assembly code, hardware, and boot code.
seL4 is a third-generation microkernel of L4 provenance,
comprising 8700 lines of C and 600 lines of assembler. Its
performance is comparable to other high-performance L4
kernels.

We prove that the implementation always strictly follows our high-level abstract specification of kernel behavior. This encompasses traditional design and implementation safety properties such as that the kernel will never crash, and it will never perform an unsafe operation. It also implies much more: we can predict precisely how the kernel will behave in every possible situation.

1. intRoDuction

Almost every paper on formal verification starts with the observation that software complexity is increasing, that this leads to errors, and that this is a problem for mission and safety critical software. We agree, as do most.

Here, we report on the full formal verification of a critical system from a high-level model down to very low-level C code. We do not pretend that this solves all of the software complexity or error problems. We do think that our approach will work for similar systems. The main message we wish to convey is that a formally verified commercial-grade, general-purpose microkernel now exists, and that formal verification is possible and feasible on code sizes of about 10,000 lines of C. It is not cheap; we spent significant effort on the verification, but it appears cost-effective and more affordable than other methods that achieve lower degrees of trustworthiness.

To build a truly trustworthy system, one needs to start at the operating system (OS) and the most critical part of the OS is its kernel. The kernel is defined as the software that executes in the privileged mode of the hardware, meaning that there can be no protection from faults occurring in the kernel, and every single bug can potentially cause arbitrary damage. The kernel is a mandatory part of a system’s trusted computing base (TCB)—the part of the system that can bypass security. 10 Minimizing this TCB is the core concept behind microkernels, an idea that goes back 40 years.

A microkernel, as opposed to the more traditional mono-
lithic design of contemporary mainstream OS kernels,
is reduced to just the bare minimum of code wrapping
hardware mechanisms and needing to run in privileged
mode. All OS services are then implemented as normal pro-
grams, running entirely in (unprivileged) user mode, and
therefore can potentially be excluded from the TCB. Previous
implementations of microkernels resulted in communica-
tion overheads that made them unattractive compared to
monolithic kernels. Modern design and implementation
techniques have managed to reduced this overhead to very
competitive limits.

figure 1. call graph of the seL4 microkernel. Vertices represent functions, and edges invocations.

The original version of this paper was published in the Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles, Oct. 2009.