Aerospace and Electronic Systems Magazine February 2018 - 19

VanderLeest
shows that information flow can penetrate the partitions only via
defined interfaces. Our attention can thus be focused solely on the
interfaces, reducing the overall effort.
The seL4 microkernel uses IPC to configure privileges, using
a mechanism called "capabilities." When the first (root) user process is created, it is given the full capabilities of the hardware,
e.g., full schedule of the CPU and entire memory address space.
These capabilities can then be delegated (in whole or in part) to
spawned threads. A thread can never obtain more capability than
was originally delegated, enforced by the microkernel. Thus, we
can manage and guarantee the isolation property required for robust partitioning.

HISTORY OF SEL4
The seL4 microkernel is a variant of the L4 microkernel family,
which has a long history dating back to the early 1990s [8]. Jochen
Liedtke developed the first L4 microkernel (based on his earlier L3
microkernel) in 1993. The work was motivated by a desire to significantly improve the performance of the kernel, and in particular,
to speed up IPC, the mechanism by which user threads gain access
to system services. Microkernels in the L4 family have appeared
on x86, Alpha, MIPS, and ARM architectures. Variations on the
original L4 with a standard application binary interface (ABI) appeared over time, such as the commercial PikeOS around 1999,
OKL4 microkernel around 2007, and the subject of this article,
seL4, around 2009.
The idea of creating a provably secure microkernel based on
L4 was first proposed by Elphinstone in 2004 [9]. The name seL4
was first published in 2005, in an honors thesis by Philip Derrin at
the University of New South Wales (UNSW) [10], working under
professors Elphinstone and Heiser; and next in a technical magazine article by Heiser [11]. The seminal work, however, appears
in a 2009 conference paper [12] outlining the formal verification
of seL4, written by a large cast of contributors from UNSW and
also NICTA, an Australian research institute, now merged into an
organization named Data61.
The intellectual property of seL4 must have been present at
least as far back as 2006, when NICTA created a spin-off company
called Open Kernel Labs. Later, in 2012 when Open Kernel Labs
was acquired by General Dynamics, the seL4 microkernel was part
of the acquisition and thus transferred to new ownership. However, in 2014, General Dynamics released seL4 as an open source
product.

LIMITATIONS AND FUTURE OF SEL4
The seL4 microkernel runs on multiple hardware platforms: x86
and ARM architectures. However, the proof of correctness was
performed on one specific target: the i.MX31 platform, using the
arm1136jf-s CPU, which uses the ARMv6 architecture: "Initial
development of seL4, and all verification work, was done for an
ARMv6-based platform, with a subsequent port of the kernel (so
far without proof) to x86" [12]. Subsequent work on the proof
was then extended to the next generation of the ARM instruction set, the ARMv7 architecture on the SABRE Lite i.MX6 platFEBRUARY 2018

Figure 3.

Unsecure kernel results in large attack surface.

Figure 4.

seL4 secure microkernel reduces attack surface.

form, which uses the ARM Cortex A9 CPU. Among other things,
Data61 has plans to expand seL4 functionality to provide multicore scheduling, ARMv8 instruction set, and real-time scheduling. Regarding real-time scheduling, at least one group has
implemented an approach in user space [13], but with significant
limitations: (a) time partitioning cannot be rigorously assured
without implementing it in the kernel and reworking the formal
proof, (b) performance is poor, which is not surprising when
implemented at the user level, (c) they implemented an earliest
deadline first algorithm, which is useful for real-time applications (were it not for the performance issues), but not the industry
standard for time partitioning, which is the two-level hierarchical
scheduling dictated by the ARINC 653 standard. As of this writing, researchers at Data61 were continuing to work on time partitioning, including elimination of covert timing channels, where
they have met some potentially insurmountable challenges with
common processor architectures [14].
The proof of correctness for seL4 is limited by the set of assumptions on which it rests. For example, it assumes that no direct
memory access (DMA) devices are present. Most modern embedded systems use DMA to improve performance, so this is not a

IEEE A&E SYSTEMS MAGAZINE

Table of Contents for the Digital Edition of Aerospace and Electronic Systems Magazine February 2018