Formal verification of software refers to the application
of mathematical proof techniques to establish properties about programs. Formal verification can cover not just
all lines of code or all decisions in a program, but all possible behaviors for all possible inputs. For example, the very
simple fragment of C code if (x < y)z = x/y else z =y/x
for x, y, and z being int tested with x = 4, y = 2 and x = 8,
y = 16, results in full code coverage: every line is executed at
least once, and every branch of every condition is taken at
least once. Yet, there are still two potential bugs remaining.
Of course, any human tester will find inputs such as x =0,
y = − 1 and x = − 1, y = 0 that expose the bugs, but for bigger
programs it is infeasible to be sure of completeness. This is
what formal verification can achieve.
The approach we use is interactive, machine-assisted,
and machine-checked proof. Specifically, we use the theorem prover Isabelle/HOL. 8 Interactive theorem proving
requires human intervention and creativity to construct
and guide the proof. It has the advantage that it is not
constrained to specific properties or finite, feasible state
spaces. We have proved the functional correctness of the
seL4 microkernel, a secure embedded microkernel of the
L46 family. This means, we have proved mathematically
that the implementation of seL4 always strictly follows our
high-level abstract specification of kernel behavior. This
property is stronger and more precise than what automated
techniques like model checking, static analysis, or kernel
implementations in type-safe languages can achieve. We
not only analyze specific aspects of the kernel, such as safe
execution, but also provide a full specification and proof
for the kernel’s precise behavior.
In the following, we describe what the implications of the
proof are, how the kernel was designed for verification, what
the verification itself entailed and what its assumptions are,
and finally what effort it cost us.
In a sense, functional correctness is one of the strongest
properties to prove about a system. Once we have proved
functional correctness with respect to a model, we can use
this model to establish further properties instead of having
to reason directly about the code. For instance, we prove that
every system call terminates by looking at the model instead
of the code. However, there are some security-relevant properties, such as transmission of information via covert channels, for which the model may not be precise enough.
So our proof does not mean that seL4 is secure for all purposes. We proved that seL4 is functionally correct. Secure
would first need a formal definition and depends on the
application. Taken seriously, security is a whole-system
question, including the system’s human components.
Even without proving specific security properties on top,
a functional correctness proof already has interesting implications for security. If the assumptions listed in Section 4. 5
are true, then in seL4 there will be:
no code injection attacks: If we always know precisely what
the system does and if the spec does not explicitly allow it,
then we can never have any foreign code executing as part
no buffer overflows: This is mainly a classic vector for code
injection, but buffer overflows may also inject unwanted
data and influence kernel behavior that way. We prove that
all array accesses are within bounds and we prove that all
pointer accesses are well typed, even if they go via casts to
void or address arithmetic.
no nULL pointer access: NULL pointer bugs can allow local
privilege escalation and execution of arbitrary code in kernel mode. 9 Absence of NULL pointer dereference is a direct
proof obligation for us for every pointer access.
no ill-typed pointer access: Even though the kernel code
deliberately breaks C type safety for efficiency at some
points, in order to predict that the system behaves according to specification, we prove that circumventing the type
system is safe at all these points.
no memory leaks and no memory freed that is still in use.
This is not purely a consequence of the proof itself. Much of
the design of seL4 was focused on explicit memory management. Users may run out of memory, but the kernel never will.
no nontermination: We have proved that all kernel calls
terminate. This means the kernel will never suddenly freeze
and not return from a system call. This does not mean that
the whole system will never freeze. It is still possible to write
bad device drivers and bad applications, but set up correctly,
a supervisor process can always stay in control of the rest of
no arithmetic or other exceptions: The C standard defines
a long list of things that can go wrong and that should be
avoided: shifting machine words by a too-large amount,
dividing by zero, etc. We proved explicitly that none of these
occur, including the absence of errors due to overflows in
no unchecked user arguments: All user input is checked and
validated. If the kernel receives garbage or malicious arguments it will respond with the specified error messages, not
with crashes. Of course, the kernel will allow a thread to kill
itself if that thread has sufficient capabilities. It will never
allow anything to crash the kernel, though.
Many of these are general security traits that are good to
have for any kind of system. We have also proved a large number of properties that are specific to seL4. We have proved
them about the kernel design and specification. With functional correctness, we know they are true about the code as
well. Some examples are:
Aligned objects: Two simple low-level invariants of the
kernel are: all objects are aligned to their size, and no two
objects overlap in memory. This makes comparing memory
regions for objects very simple and efficient.
Well-formed data structures: Lists, doubly linked, singly
linked, with and without additional information, are a pet
topic of formal verification. These data structures also occur
in seL4 and we proved the usual properties: lists are not circular when they should not be, back pointers point to the
right nodes, insertion, deletion etc., work as expected.
Algorithmic invariants: Many optimizations rely on certain
properties being always true, so specific checks can be left
out or can be replaced by other, more efficient checks. A simple example is that the distinguished idle thread is always
in thread state idle and therefore can never be blocked or