Aerospace and Electronic Systems Magazine February 2018 - 20

Is Formal Proof of seL4 Sufficient for Avionics Security?
domains: (a) a highly secure domain to contain classified information, such as secure video or "friend" positions, and (b) a lower security domain to contain nonclassified information, such as public
map or weather data. In the envisioned system of Figure 6, we follow the Bell-Lapadula multilevel security model, i.e., no read-up
and no write-down. This ensures that no information can leak from
the higher to the lower security domain.

IMPLICATIONS TO AVIONICS SECURITY AND SAFETY
Use of the seL4 microkernel in a flight-certified system must address two issues: expanding its functionality to provide a full partitioning environment, and building its certification story. Both these
challenges are discussed in this section.
The separation provided by seL4 is a fundamental technology that could support isolation of mixed-criticality applications
in partitions as described in DO-297. However, the common implementation of partitioning for avionics is the ARINC 653 API,
which requires more than simply a separation kernel. Following
the design philosophy for a microkernel, a system architecture that
implemented ARINC 653 on seL4 would push as much functionality into user space as possible. This is relatively straightforward for
intrapartition services such as blackboards and semaphores. Somewhat more challenging would be shared services. This would include interpartition services such as sampling and queueing ports,

Figure 5.

GDB for seL4.

small omission. Data61 has plans to address some of
these proof assumptions in the future.
The seL4 microkernel is relatively young and
thus the software development ecosystem around it
is rather immature. When the US Defense Advanced
Research Projects Agency (DARPA) took interest in
the seL4 microkernel, the lack of a broad ecosystem
was a weakness they sought to address by funding a
variety of initiatives, including the Small Business
Innovation Research (SBIR) contract that funded a
project at DornerWorks. Part of the work was to define an ecosystem roadmap for seL4 and begin fleshing out that roadmap, starting with the porting of the
GDB debugger for use with seL4. Figure 5 illustrates
our first version using the gdb-stub method, which
embeds some extra code alongside the application on
the target. The GDB monitor running on a host development system then communicates with this remote
target gdb stub (via serial) to provide the standard debugging functionality such as breakpoints, memory
examination, etc. We next plan to add Ethernet as a
communication protocol and expand to gdb server on
the target to allow debugging of multiple application
processes.
The DornerWorks project with DARPA also
examined whether the assurance of the seL4 microkernel could be leveraged in a real, embedded environment. We collaborated with Rockwell Collins to
consider the use of seL4 in their helmet mounted display (HMD) as a means to provide separate security
20

Figure 6.

seL4 security for HMD.

IEEE A&E SYSTEMS MAGAZINE

FEBRUARY 2018

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