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
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