otherwise waiting for I/O. This can be used to remove checks in the code paths that deal with the idle thread.

Correct book-keeping: The seL4 kernel has an explicit user-visible concept of keeping track of memory, who has access to it, who access was delegated to, and what needs to be done if a privileged process wants to revoke access from delegates. It is the central mechanism for reusing memory in seL4. The data structure that backs this concept is correspondingly complex and its implications reach into almost all aspects of the kernel. For instance, we proved that if a live object exists anywhere in memory, then there exists an explicit capability node in this data structure that covers the object. And if such a capability exists, then it exists in the proper place in the data structure and has the right relationship towards parents, siblings, and descendants within. If an object is live (may be mentioned in other objects anywhere in the system) then the object itself together with that capability must have recorded enough information to reach all objects that refer to it (directly or indirectly). Together with a whole host of further invariants, these properties allow the kernel code to reduce the complex, system-global test whether a region of memory is mentioned anywhere else in the system to a quick, local pointer comparison.

We have proved about 80 such invariants on the executable specification such that they directly transfer to the data structures used in the C program.

A verification like this is not an absolute guarantee. The key condition in all this is if the assumptions are true. To attack any of these properties, this is where one would have to look. What the proof really does is take 7500 lines of C code out of the equation. It reduces possible attacks and the human analysis necessary to guard against them to the assumptions and specification. It also is the basis for any formal analysis of systems running on top of the kernel or for further high-level analysis of the kernel itself.

3. KeRneL DesiGn foR VeRification

The challenge in designing a verifiable and usable kernel lies in reducing complexity to make verification easier while maintaining high performance.

To achieve these two objectives, we designed and implemented a microkernel from scratch. This kernel, called seL4, is a third-generation microkernel, based on L4 and influenced by EROS. 11 It is designed for practical deployment in embedded systems with high trustworthiness requirements. One of its innovations is completely explicit memory-management subject to policies defined at user level, even for kernel memory. All authority in seL4 is mediated by capabilities, 2 tokens identifying objects and conveying access rights.

We first briefly present the approach we used for a kernel/ proof codesign process. Then we highlight the main design decisions we made to simplify the verification work.

3. 1. Kernel/proof codesign process

One key idea in this project was bridging the gap between
verifiability and performance by using an iterative approach
to kernel design, based around an intermediate target that
is readily accessible to both OS developers and formal meth-
ods practitioners. We used the functional language Haskell
to provide a programming language for OS developers,
while at the same time providing an artifact that can readily
be reasoned about in the theorem proving tool: the design
team wrote increasingly complete prototypes of the kernel
in Haskell, exporting the system call interface via a hard-
ware simulator to user-level binary code. The formal meth-
ods team imported this prototype into the theorem prover
and used it as an intermediate executable specification. The
approach aims at quickly iterating through design, proto-
type implementation, and formal model until convergence.

3. 2. Design decisions

Global Variables and side effects: Use of global variables and functions with side effects is common in operating systems— mirroring properties of contemporary computer hardware and OS abstractions. Our verification techniques can deal routinely with side effects, but implicit state updates and complex use of the same global variable for different purposes make verification more difficult. This is not surprising: the higher the conceptual complexity, the higher the verification effort.

The deeper reason is that global variables usually require stating and proving invariant properties. For example, scheduler queues are global data structures frequently implemented as doubly linked lists. The corresponding invariant might state that all back links in the list point to the appropriate nodes and that all elements point to thread control blocks and that all active threads are in one of the scheduler queues.

Invariants are expensive because they need to be proved not only locally for the functions that directly manipulate the scheduler queue, but for the whole kernel—we have to show that no other pointer manipulation in the kernel destroys the list or its properties. This proof can be easy or hard, depending on how modularly the global variable is used.

Dealing with global variables was simplified by deriving the kernel implementation from Haskell, where side effects are explicit and drawn to the design team’s attention.

Kernel Memory Management: The seL4 kernel uses a model of memory allocation that exports control of the in-kernel allocation to appropriately authorized applications. While this model is mostly motivated by the need for precise guarantees of memory consumption, it also benefits verification. The model pushes the policy for allocation outside the kernel, which means we only need to prove that the mechanism