Mixed criticality functions integrated on a single computing platform require special attention to safety and security. 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 because of their high cost, a very small footprint is desirable. One promising new development is the open source seL4 microkernel, a formally proven microkernel. The seL4 microkernel is intentionally simple, providing the bare minimum features to isolate software functionality. 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.
The open source, formally-proven seL4 microkernel: Considerations for use in avionics
2016-09-01
573944 byte
Conference paper
Electronic Resource
English
Open systems avionics architectures considerations
IEEE | 2003
|SATWG considerations for space avionics
British Library Conference Proceedings | 1993
|Environmental Considerations for Avionics Installation
SAE Technical Papers | 1977
|Towards Formal Verification of a Separation Microkernel
British Library Conference Proceedings | 2013
|