Aerospace and Electronic Systems Magazine February 2018 - 16

Feature Article:

DOI. No. 10.1109/MAES.2018.160217

Is Formal Proof of seL4 Sufficient for Avionics Security?
Steven H. VanderLeest, DornerWorks, Grand Rapids, MI, USA

INTRODUCTION
How do we know that the software on a modern aircraft is reliable
enough to trust our lives with it? The seL4 microkernel is a minimalist operating system that has potential for use in avionics. It has
been formally proven to satisfy its specifications, including classic
security properties of integrity and confidentiality, making it particularly attractive for systems where safety and security are paramount.
Traditional verification methods are good at testing positive requirements-whether the software does something you want, e.g., "when I
push button X, light B turns on." However, those same verification
methods are quite poor at testing negative requirements, when we
want to ensure the software does not do something, e.g., "the software never takes longer than 10 ms to respond." Why is that difficult? The number of circumstances we might need to test could be
astronomical, making it practically infeasible to check exhaustively.
This difficulty with negative requirements is where formal methods
come to the rescue. Formal methods use mathematical proofs to establish high confidence that certain properties hold, such as proving
the software is not vulnerable to a certain class of hacking attacks. Is
formal proof of correctness sufficient for the security needs of safetycritical flight software? No; but it is a good start. One of the most
important properties we might want to test for a large avionics system
is isolation. When multiple software applications are running on the
same computer hardware, we want to be sure that the coffee maker
software cannot interfere with the flight navigation software. That
is, for two applications that have very different levels of safety criticality, we must isolate them from each other. The seL4 microkernel
provides such guarantees of isolation (also called partitioning). This
article introduces a few of the main concepts, provides a compare
and contrast overview of partitioning approaches in modern avionics,
introduces the seL4 microkernel, and finishes with an examination of
what more must be done before seL4 could be legitimately considered for use in flight software. Before tackling those topics, it may
be helpful to review two topics for context: the relationship of safety
and security, and the concept of integrated modular avionics (IMA).

Author's address: DornerWorks, 3445 Lake Eastbrook Blvd
SE, Grand Rapids, MI 49546. E-mail: (Steve.VanderLeest@
dornerworks.com).
An earlier version of this paper appeared in the 35th Digital
Avionics Systems Conference, Sacramento, CA, Sept. 25-29,
2016. The paper was adapted and revised for this article.
Manuscript received October 14, 2016, revised December 30,
2016, March 9, 2017, and ready for publication May 2, 2017.
Review handled by W. Walsh.
0885/8985/18/$26.00 © 2018 IEEE
16

The concept of safety as a paramount goal of avionics is probably
familiar, but security is now becoming equally important. Safety is
focused on reducing the probability of injury or death due to equipment fault or failure. Historical improvements in safety have been
significant, resulting in an excellent safety record for modern aircraft. These improvements are largely due to a focus on reliability:
reducing the number of faults that occur and minimizing their impact
if they do occur. Recently, the aerospace industry has more clearly
recognized the impact that security issues can have on safety-especially as avionics systems become more interconnected-because
exploited security vulnerabilities could lead to faults that impact
safety. Security is focused on reducing the probability of information leakage (inappropriate reading of data) or corruption (inappropriate modification of data). Protection of classified military data
has long implied information assurance measures, but in a highly
connected passenger environment, security concerns now also apply
to protecting confidential information for commercial customers. In
both military and commercial aircraft, security and safety concerns
overlap, affecting the design of the avionics system architecture in
order to prevent unauthorized intrusion to any subsystem that impacts safety of flight. For example, the Future Airborne Capability
Environment (FACE™) consortium has recently defined their FACE
Technical Standard with both a safety profile and a security profile. Formal methods are one means to achieve the highest levels
of safety, such as DO-178C Level A, and they are the only means
to achieve the highest levels of security, such as Common Criteria
Evaluation Assurance Level 7. Formal methods use mathematical
proofs to demonstrate the design is correct. However, the formal
methods approach is costly. Even with the use of some automated
tools, application of formal methods is generally labor intensive, and
thus expensive. One reference estimates the added effort as high as
a 3,125% increase [1] compared with normal software development.
Because of the high cost and extreme effort required to develop formal proofs, a very small software footprint is desirable, with most
authorities suggesting the analyzed software should be less than
10,000 source lines of code. For comparison, Wind River VxWorks
is estimated to be more than 500,000 lines of code, and Microsoft
Windows is estimated to be on the order of 50 million lines of code.
Thus, certification effort proportional to the size of code creates a
tension between the desire for more functionality in the partitioning
environment kernel and the cost to certify that kernel.
The concept of IMA is to reduce the number of line replaceable
units and the number of wires on an aircraft via coalescence of formerly federated units. That is, a more powerful single computing
platform replaces multiple separate (but less computationally powerful) boxes on the aircraft. For example, Honeywell found that for
their work on the A380 avionics, IMA provided "a 50% volume

IEEE A&E SYSTEMS MAGAZINE

FEBRUARY 2018

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