Aerospace and Electronic Systems Magazine February 2018 - 17

and 40% weight reduction from previous federated surveillance
equipment" [2]. Cost containment strategies must also address
flight certification. By itself, IMA might actually increase certification costs, because now one must demonstrate that software at
differing levels of criticality that are simultaneously present on one
computing platform do not adversely affect one another. Consider
the hypothetical situation where the coffee maker software and the
flight navigation software that were hosted on separate computers
originally are now both running on a single computer. Our design
must assure that the coffee maker software cannot under any circumstances affect the flight of the aircraft. IMA implements an architectural mechanism to ensure these disparate software modules
are isolated from one another: partitioning.

PARTITIONING APPROACHES
This section reviews the need for partitioning, and briefly examines several approaches to achieving robust partitioning. The subsequent sections then explore the partitioning kernel that is the
main topic of this article: seL4. Partitioning separates software
modules from each other in order to reduce or eliminate unwanted
and unexpected interaction. The ARINC 653 standard specifies
a software execution environment in which isolated applications
can run independently of one another, each in its own container
called a "partition." The partitions provide mutually exclusive
access to all necessary system resources, such as the CPU or
memory, so that (a) the presence of a partition does not affect the
performance of an unrelated partition, and (b) faults within one
partition are isolated from other partitions. Shared resources must
be partitioned spatially and/or temporally. Although the FACE
Technical Standard makes the ARINC 653 Application Program
Interface (API) optional (one can provide POSIX instead, or in
addition), it does require partitioning as part of the operating system segment for the defined system architecture. IMA also requires partitioning, as a means to provide safety, but also because
of its potential to reduce certification costs for reused software.
However, the partitioning environment itself must be certified to
the highest level of any of the hosted software. To illustrate from
our example, consider that less rigorous design assurance may
be needed for the coffee maker software, while highly rigorous
design assurance is necessary for the flight navigation software.
When we assure the underlying partitioning environment software, we must use the higher level of rigor, equal to that used on
the flight navigation software.
The seL4 microkernel is a separation kernel that can provide
the robust partitioning necessary to support information assurance
with multiple levels of security and also support design assurance
FEBRUARY 2018

for airworthiness with mixed levels of safety criticality. While the
seL4 microkernel discussed in this article is the first softwarebased separation kernel to be formally proven correct to specification at the level of executable object code, there has been earlier
work, such as formal verification of the PikeOS microkernel [3]
and the Rockwell Collins proof of their AAMP7G processor [4].
Formal methods have also been used to verify a protection layer
supporting a hypervisor [5].
Consolidation of software functions from multiple federated
computing systems to a single (more powerful) integrated computing system provides savings of size and weight in almost all cases,
and often reduces power and cost. More powerful modern microprocessors not only consolidate legacy functionality, but also frequently
have spare capacity, facilitating the addition of completely new
functionality. However, the tradeoff is increased complexity of interactions. Functions separated by hardware only interact by means
of explicit, well-defined communication pathways. Once integrated
into a single computing system, additional channels of interaction
are introduced. In the absence of any isolating mechanisms, the risk
of potential interference between functions on the same computer
forces us to certify all software on a single computing platform to the
highest level of assurance of any one of them. The high cost of such
certification has led to the definition and standardization of partitioning as an isolation mechanism. With robust partitioning, mixed criticality software can coexist on one system, each assured to its appropriate level (and not necessarily higher). The following subsections
review three historical approaches to partitioning for safety-critical
applications: adaptation of an existing certified operating system,
use of a hypervisor, or use of a microkernel.

PARTITIONING APPROACH 1: ADAPTATION OF A REAL
TIME OPERATING SYSTEM
The most common approach to developing a partitioning environment for safety-critical applications such as avionics has been
incremental extension of an existing flight-certified real time operating system (RTOS). Why? Clean slate development represents
potentially higher cost, higher risk, and may not be capable of offering compatibility to legacy applications developed previously.
By starting with a well-understood existing product, the hope for
the developer is that much can be reused-not only reuse of the
software technology itself, but also reuse of certification artifacts.
Examples of this approach include the Wind River VxWorks 653
Platform which was developed based on the flight-certified VxWorks RTOS, Green Hills Integrity-178B based on its Integrity
RTOS, and LynxOS-178 RTOS.

IEEE A&E SYSTEMS MAGAZINE

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