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)
system.

 

Read The Paper