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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    The open source, formally-proven seL4 microkernel: Considerations for use in avionics


    Contributors:


    Publication date :

    2016-09-01


    Size :

    573944 byte





    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English





    SATWG considerations for space avionics

    Cox, K. J. / Brown, D. C. | British Library Conference Proceedings | 1993


    Environmental Considerations for Avionics Installation

    Hauter, A. J. | SAE Technical Papers | 1977


    Towards Formal Verification of a Separation Microkernel

    Butterfield, A. / Sanan, D. / Hinchey, M. et al. | British Library Conference Proceedings | 2013