Aerospace and Electronic Systems Magazine February 2018 - 18

Is Formal Proof of seL4 Sufficient for Avionics Security?
all the required ARINC 653 functionality to the separation kernel
used at the heart of a MILS hypervisor would push its total size
beyond that which is feasible for security analysis at the highest
levels of assurance.

PARTITIONING APPROACH 3: MICROKERNEL

Figure 1.

Traditional RTOS hosting applications.

Figure 2.

Hypervisor hosting operating systems.

PARTITIONING APPROACH 2: HYPERVISOR
Another architectural approach to provide partitioning is to leverage the virtualization provided by a hypervisor. Also known
as a virtual machine monitor (VMM), a hypervisor manages the
computing hardware on behalf of the rest of the software in the
system. Just like a traditional operating system hosts applications
(Figure 1), a hypervisor can host entire operating systems, each in
turn hosting its own applications (Figure 2). While traditional operating systems provide some limited isolation between applications,
the hypervisor leverages virtualization hardware on the processor
to provide strong isolation that can more easily be verified. Virtualization has a long history stretching back to IBM mainframes in
the 1960s. However, it also forms the modern backbone of cloud
computing. As processors have continued to become more powerful, and particularly with the rise of multicore, hypervisors are now
making the leap from enterprise IT to embedded applications.
Although the hypervisor is a natural means to implement partitioning of mixed-criticality applications as described in DO-297
and ARINC 653, it has not been the solution of choice for most
existing RTOS vendors for avionics. In most cases, the vendor
chose to extend their existing flight-certified product rather than
build a native partitioning environment from the ground up. The
difference between the two approaches is significant enough that
although each vendor also offers a hypervisor, they do so in a
different product line. For example, Wind River describes their
approach [6] to combining safety and security in one system, using a multiple independent levels of security (MILS) hypervisor
that hosts an ARINC 653 RTOS as a virtualized guest. The paper
explains that ARINC 653 partitioning is delegated to a domain
(in essence, a partition) of the hypervisor due to the cost of proving the security attributes: "an ARINC 653 safety critical RTOS
is unlikely to meet the security requirements due to the size of
the kernel and because it may allow device drivers to be implemented in kernel space." Apparently, they concluded that adding
18

A final architectural approach to provide partitioning is use of a
microkernel. Software tends to bloat with features over time. Many
RTOS and hypervisor products that started out slim have grown
over time, resulting in a large source code base. Because the operating system has the highest privilege on the system, that large
code base represents a dauntingly large cost to certify. The microkernel approach attempts to distill the operating system down to
the smallest feature set possible. The resulting kernel can be quite
minimal, thus reducing the cost to provide design assurance for
safety or security purposes.
Only the features absolutely necessary to manage the computing hardware are incorporated in a microkernel. Which features
are those? The microkernel must at least provide the capability to
manage the fundamental computer hardware, including management of memory (space partitioning) and management of threads
of execution on the CPU (temporal partitioning). Beyond CPU
and memory, the third component of computer hardware is input/
output (I/O). Because modern computer architectures map I/O via
the memory address space, I/O is implicitly managed via time and
space partitioning. One final feature is essential: the ability of user
threads to communicate with the kernel. This capability is usually generalized to interprocess communication (IPC), providing
a mechanism not only for kernel communication, but also for one
user process to communicate with another.
Hence, the microkernel is simple, implementing the minimalist approach to partitioning and providing only a bare modicum
of features. This simplicity is a boon to certification, since the
level of effort is proportional to the size and complexity of the
software code. All other functionality is pushed up to userland (an
application space separated from the kernel, with less privilege).
Examples of functionality delegated out of the kernel include file
system, graphical user interface, and the network protocol stack.

THE SEL4 MICROKERNEL
Having reviewed several approaches to partitioning, we can now
examine the seL4 microkernel in more detail. The seL4 microkernel is the "world's first operating-system kernel with an end-to-end
proof of implementation correctness and security enforcement"
[7]. Why is this important? Without a bullet-proof guarantee of isolation of partitions, we cannot rule out the possibility of accidental or malicious cross-interference between partitions with 100%
confidence. As Figure 3 illustrates, the potential attack surface is
large without that guarantee, because information might flow from
anywhere in the system into the domain for which safety and/or
security is critical.
By contrast, seL4 provides guarantees of several properties,
including isolation, via a formal proof of correctness. This proof
gives us assurance that the attack surface is much smaller. Figure 4

IEEE A&E SYSTEMS MAGAZINE

FEBRUARY 2018

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