In 2009, Gerwin Klein and twelve coauthors reported a machine-checked proof for the seL4 operating-system microkernel, comprising 8,700 lines of C and 600 lines of assembly. The proof showed that the C code matched a specification, but it explicitly assumed that the assembly code was correct. That boundary is part of what they achieved.
The team proved that the kernel’s C implementation followed an abstract specification of its behaviour. This was functional correctness: a precise relationship between what the kernel was specified to do and what its implementation did, under stated assumptions.
The work also found defects. The original paper reports that formal verification uncovered 144 implementation defects, after other activities had already uncovered sixteen. The proof was part of developing and correcting the kernel.
Why focus on the kernel?
An operating-system kernel runs with privileges that ordinary applications do not have. A fault there can undermine the rest of the system. Keeping this privileged foundation small makes it a more manageable target for verification.
seL4 follows the microkernel approach. Its programming model provides mechanisms for threads, address spaces and communication, while most device drivers run as user-mode applications; the kernel described in the paper contains a timer driver. Capabilities—references that carry authority to use kernel objects—control access to resources.
This division gives the proof a defined subject. Proving properties of the microkernel does not automatically prove that every application or driver built around it behaves correctly. The surrounding system still needs its own design and evidence.
The initial verification described in the paper targeted an ARMv6 platform. The authors also reported an x86 port, which at that time had no corresponding proof. Even in the original account, running the kernel and verifying a particular implementation were separate achievements.
Connect the implementation to a simpler description
The team used an intermediate Haskell prototype to connect operating-system development with formal reasoning. Developers could execute the prototype with a hardware simulator, while its restricted Haskell subset could be translated into the theorem prover.
They then manually implemented the kernel in C. This allowed low-level optimisation and avoided making the Haskell runtime part of the production kernel. The prototype served as a detailed design, rather than the final deployed implementation.
The proof connected three layers: an abstract specification describing behaviour, an executable specification containing implementation details, and the C implementation. The technique, called refinement, establishes that a more concrete layer stays within the behaviour permitted by the more abstract layer.
The researchers constructed and guided these proofs using Isabelle/HOL, an interactive theorem prover based on higher-order logic. Human reasoning shaped the argument; the tool checked the proof steps. This was substantially different from running a large collection of example inputs.
A small inconsistency can matter
Much of the work involved invariants: properties that must remain true as the kernel operates. A linked structure might need valid references, correctly connected entries and agreement with information stored elsewhere.
Such properties extend beyond an individual function. Updating one object must preserve assumptions that other operations depend on. The paper reports more than 150 invariants across the specification levels.
One implementation defect offers a concrete example. The ARM interrupt controller used the value 0xFF to indicate that no interrupt was active. Most of the code handled that value correctly, but one location checked against NULL, C’s null-pointer constant, instead.
The authors describe many defects found during C verification as typing mistakes, misread specifications or incomplete updates after specification changes. Their causes could be ordinary human errors even when their consequences included crashes or security vulnerabilities.
The assumptions are part of the result
The 2009 proof stopped at C source code. It assumed a correct compiler, assembly code and hardware. It also omitted about 1,200 lines of boot and initialisation code; the central correspondence concerned behaviour between kernel entry and exit points.
Some low-level hardware interactions remained outside the detailed model. The paper discusses assumptions around cache management and the translation lookaside buffer, the processor’s cache of address translations. These connections between the mathematical model and the machine required additional reasoning and checks.
There was another boundary inside the specification itself. The authors explicitly noted that proving implementation correctness does not guarantee that the specification describes the behaviour a user expects. A precisely implemented requirement can still be the wrong requirement.
The effort was substantial. The paper reports about twenty person-years of proof work, including research, frameworks, tools and libraries. That measures accumulated effort, not twenty years of elapsed project time.
Read today’s claims by configuration
The project has since developed additional proof layers. Its current proof repository separately identifies refinement to C, binary verification, access-control proofs and information-flow proofs. These establish different properties and should not all be attributed to the original 2009 result.
The official configuration documentation makes the distinction operational. It lists which properties apply to particular architectures and configurations. For example, its ARM AArch32 coverage includes binary correctness for C functions with C-level verification; the x64 entry lists C-level functional correctness without the fast path.
The documentation also identifies unverified features, including kernel startup at boot. Its implications page conditions the excluded classes of programming errors on the proof assumptions and verified configurations, and conditions its isolation discussion on correct system setup.
The useful habit is to read a verification claim together with its subject, property, configuration and assumptions. The seL4 paper makes that habit concrete: the 0xFF check, the C implementation and the abstract specification all belong to one argument whose boundaries are written down.
Related stories
Sources
- Klein and coauthors: seL4: Formal Verification of an OS Kernel, SOSP 2009
- The L4.verified Proofs: repository documentation
- seL4 documentation: Verified Configurations
- seL4: What the Proof Implies
- Featured image: Kurt Kaiser; Wikimedia Commons; CC0 (adapted from the original)
SIGNAL TITANS
Leave a Reply