Figure 1. Isolation and controlled communication with seL4.
Figure 2. Kernel objects for an example seL4-based system with two threads communicating via an endpoint.
seL4
Untrusted VM
Guest apps
Guest OS
Native apps Native apps
TrustedUntrusted
Hardware
Thread ObjectA
CNodeA1 EP
Thread Object B
CNodeB1
CNodeA2
VSpace
VSpace
CSpace CSpace
Se
n
d
Re
cei
ve
PDA
PTA1
FRAME
FRAME
...
...
...
...
...
. . . CON
T
EX
T
CO
N T
EX
T
AB
other publicly available software in hu-
man history in terms not only of lines
of proof but strength of properties
proved. At the heart of this verification
story sits the proof of “functional cor-
rectness” of the kernel’s C implemen-
tation, 23 guaranteeing every behavior
of the kernel is predicted by its formal
abstract specification; see the online
appendix ( dl.acm.org/citation.cfm?
doid=3230627&picked=formats) for an
idea of how these proofs look. Following
this guarantee, we added further proofs
we explain after first introducing the
main kernel mechanisms.
seL4 API. The seL4 kernel provides a
minimal set of mechanisms for imple-
menting secure systems: threads, ca-
pability management, virtual address
spaces, inter-process communication
(IPC), signaling, and interrupt delivery.
The kernel maintains its state in
“kernel objects.” For example, for each
thread in a system there is a “thread
object” that stores information about
scheduling, execution, and access con-
trol. User-space programs can refer to
kernel objects only indirectly through
“capabilities” 10 that combine a refer-
ence to an object with a set of access
rights to this object. For example, a
thread cannot start or stop another
thread unless it has a capability to the
corresponding thread object.
Threads communicate and syn-
chronize by sending messages through
IPC “endpoint” objects. One thread
with a send capability to an appropri-
ate endpoint can message another
thread that has a receive capability to
that endpoint. “Notification” objects
provide synchronization through sets
of binary semaphores. Virtual address
translation is managed by kernel ob-
jects that represent page directories,
are toy systems. For instance, Comp-
Cert is a commercial product, the seL4
microkernel is used in aerospace, au-
tonomous aviation, and as an Internet
of Things platform, and the CoCon
system has been used in multiple full-
scale scientific conferences.
These verification projects required
significant effort, and for verification
to be practical for widespread use, the
effort needs to decrease. Here, we demonstrate how strategically combining
formal and informal techniques, partially automating the formal ones, and
carefully architecting the software to
maximize the benefits of isolated components, allowed us to dramatically increase the assurance of systems whose
overall size and complexity is orders-of-magnitude greater than that of the
systems mentioned earlier.
Note we primarily use formal veri-
fication to provide proofs about cor-
rectness of code that a system’s safety
or security relies on. But it has other
benefits as well. For example, code
correctness proofs make assumptions
about the context in which the code is
run (such as behavior of hardware and
configuration of software). Since for-
mal verification makes these assump-
tions explicit, developer effort can
focus on ensuring the assumptions
hold—through other means of verifi-
cation like testing. Moreover, in many
cases systems consist of a combina-
tion of verified and non-verified code,
and in them, formal verification acts
as a lens, focusing review, testing, and
debugging on the system’s critical non-
verified code.
seL4
We begin with the foundation for building provably trustworthy systems—the
operating system (OS) kernel, the system’s most critical part and enabler
of cost-effective trustworthiness of the
entire system.
The seL4 microkernel provides a
formally verified minimal set of mechanisms for implementing secure systems. Unlike standard separation kernels31 they are purposefully general and
so can be combined for implementing a
range of security policies for a range of
system requirements.
One of the main design goals of
seL4 (see the sidebar “Proof Effort”)
is to enforce strong isolation between
mutually distrusting components that
may run on top of it. The mechanisms
support its use as a hypervisor to, say,
host entire Linux operating systems
while keeping them isolated from se-curity-critical components that might
run alongside, as outlined in Figure 1.
In particular, this functionality allows
system designers to deploy legacy
components that may have latent vulnerabilities alongside highly trustworthy components.
The seL4 kernel is unique among
general-purpose microkernels. Not
only does it deliver the best performance in its class, 20 its 10,000 lines
of C code have been subjected to
more formal verification than any
