The Open Source, Formally-Proven seL4 Microkernel: Considerations for Use in Avionics

The Open Source, Formally-Proven seL4 Microkernel: Considerations for Use in Avionics

ARINC 653 and DO-248 provide guidelines for partitioning software so that functions of differing levels of criticality are isolated from one another. The partitioning environment operating system isolates each partition, and because it is foundational it must be certified to the highest level of criticality of any supported partition.

Formal methods are one means to achieve high levels of safety and security, but costly. One promising new development is the open source seL4 microkernel, a formally proven microkernel.

In this paper we analyze the suitability of seL4 for use in digital avionics systems that require high levels of safety and/or security. We also provide an overview of our work to leverage the assurance arguments of seL4, to contribute to the ecosystem around it, and to demonstrate use of seL4 for an embedded platform: a Helmet Mounted Display (HMD)

Topics covered in this paper:

  • Partitioning approaches
  • The seL4 microkernel
  • Limitations and future of seL4
  • And more…

This paper is hosted by, the world’s largest technical professional organization dedicated to advancing technology for the benefit of humanity. Click the button below to find the work.
Read The Paper


Steve VanderLeestSteve VanderLeest
Steve is DornerWorks former COO, a multi-talented technical expert and entrepreneur with proven expertise in engineering design and processes. Steve has experience in both industry and academia, having been a professor of engineering at Calvin College for many years. He has published dozens of papers on a variety of technology-related topics.