Aerospace and Electronic Systems Magazine February 2018 - 21

VanderLeest
but here the intrinsic IPC service that seL4 already provides might
serve as a sufficient basis. The ARINC 653 Part 2 extended services such as filesystems and logging services could likely be built
using IPC along with seL4 capabilities to configure specific access permissions. Perhaps the most challenging would be the fault
management and health monitoring required by ARINC 653, as
this might require changes to the kernel itself, which would in turn
require reworking elements of the proof of correctness.
The certification story for seL4 starts with the strong basis of
the mathematical proof of correctness to specifications. However,
this is not sufficient. The Federal Aviation Administration (FAA)
uses DO-333 to guide the use of formal methods as a means to
assuring safety. Before using seL4 in a commercial flight environment, the objectives of this standard must be met. Furthermore,
because the proof used Isabelle, a mechanical theorem prover, Isabelle itself must be qualified as a tool according to DO-330. Of
course the applications leveraging seL4 must also be certified to
the appropriate level of assurance, but here the hidden extra effort is that seL4 pushes several features up to the application level,
including drivers and libraries. On the other hand, because of this
shift, it may be possible to certify that code to a lower level of
criticality than if it were in the kernel, which must be certified to a
level of assurance equivalent to the highest necessary for any application it supports. For example, an RS-232 serial driver used by
the coffee maker could be certified with a rather low level of rigor
if it were isolated to the coffee maker partition, but if it were in the
kernel, it would need to be certified with much more rigor. Another
certification challenge may be that seL4 is open source. Some have
worried that frequent changes and improvements to open source
code under a loose system of distributed management would make
it difficult to meet the dictates of DO-178, such as strict configuration management and problem report tracking. However, these
concerns can be addressed by a support vendor that captures a
snapshot of the open source code, which is then used as the baseline for certification. This is the approach DornerWorks takes. Future improvements to the open source code "in the wild" could
then be considered for incorporation into the certified branch, just
like a proprietary vendor would do when considering the addition
of new features, balancing these capability improvements with the
cost of recertifying part of the code.

ACKNOWLEDGMENT
This research was developed in part with funding from the Defense
Advanced Research Projects Agency (DARPA). The views, opinions, and/or findings expressed are those of the author and should
not be interpreted as representing the official views or policies of
the Department of Defense or the U.S. Government.

REFERENCES
[1]

[2]

[3]

[4]

[5]

[6]
[7]
[8]

[9]

[10]
[11]

CONCLUSION

[12]

The seL4 microkernel is a promising new technology that has
strong potential to form the basis for secure and safe avionics systems in the future. Data61 will continue development of some of
the core functionality, while companies like DornerWorks continue
development of the ecosystem around seL4 and perhaps also fleshing out the design assurance story with hopes of identifying a pilot
program that can provide the first instance of flight certification
using the seL4 microkernel.

FEBRUARY 2018

[13]

[14]

IEEE A&E SYSTEMS MAGAZINE

Colbert, E., and Boehm, B. Cost estimation for secure software &
systems. In Proceedings of the ISPA/SCEA 2008 Joint International
Conference, May 12-14, 2008.
Ramsey, J. W. Integrated modular avionics: Less is more. Avionics
Today, Feb. 1, 2007, http://www.aviationtoday.com/av/commercial/
Integrated-Modular-Avionics-Less-is-More_8420.html.
Baumann, C. Beckert, B., Blasum, H., and Bormer, T. Formal verification of a microkernel used in dependable software systems. In Computer Safety, Reliability, and Security. Berlin Heidelberg: Springer,
2009, pp. 187-200.
Wilding, M. M., Greve, D. A., Richards, R. J., and Hardin, D. S.
Formal verification of partition management for the AAMP7G microprocessor. In Design and Verification of Microprocessor Systems
for High-Assurance Applications. New York: Springer, 2010, pp.
175-191.
McCoyd, M., Krug, R. B., Goel, D., Dahlin, M., and Young, W. Building a hypervisor on a formally verifiable protection layer. In Proceedings of the 46th Hawaii International Conference on System Sciences
(HICSS), 2013.
Parkinson, P. Safety, security and multicore. In Advances in Systems
Safety. London: Springer, 2011, pp. 215-232.
The seL4 Microkernel, https://sel4.systems, accessed 14 Oct. 2016.
Elphinstone, K., and Heiser, G. From L3 to seL4 what have we learnt
in 20 years of L4 microkernels? In Proceedings of the Twenty-Fourth
ACM Symposium on Operating Systems Principles, 2013.
Elphinstone, K. Future directions in the evolution of the L4 microkernel. NICTA Formal Methods Program Workshop on Operating Systems Verification, 2004.
Derrin, P. G. A secure microkernel. Dissertation, University of New
South Wales, 2005.
Heiser, G. Secure embedded systems need microkernels. USENIX,
login 30.6, 2005, 9-13.
Klein, G. Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin,
P. et al. seL4: Formal verification of an OS kernel. In Proceedings of
the ACM SIGOPS 22nd Symposium on Operating Systems Principles,
2009.
Åsberg, M., and Nolte, T. Towards a user-mode approach to partitioned scheduling in the sel4 microkernel. ACM SIGBED Review, 10.3
(2013), 15-22.
Ge, Q., Yarom, Y., and and Heiser, G. Do hardware cache flushing
operations actually meet our expectations? arXiv:1612.04474, 2016.

http://www.aviationtoday.com/av/commercial/Integrated-Modular-Avionics-Less-is-More_8420.htm http://www.aviationtoday.com/av/commercial/Integrated-Modular-Avionics-Less-is-More_8420.htm https://www.sel4.systems

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