The seL4 Microkernel – A Robust, Resilient, and Open-Source Foundation for Ground Vehicle Electronics Architecture

There has been a lot of interest in the secure embedded L4 (seL4) microkernel in recent years as the basis of a cyber-security platform because it has been formally proven to be correct and free of common defects. However, while the seL4 microkernel has a formal proof of correctness, it does so at the cost of deferring functionality to the user space that most developers and system integrators would deem necessary for real life products and solutions, and use of formal proofs for user space can be prohibitively expensive. DornerWorks took an approach to bypass the need for native seL4 user space applications to develop a representative real-world system for GVSC VEA based on seL4 by enabling its virtual machine monitor functionality for ARMv8 platforms, allowing feature rich software stacks to be run in isolation guaranteed by the seL4 formal proofs. This paper describes that system and the efforts undertaken to achieve real world functionality.

Citation: R. VanVossen, J. Millwood, C. Guikema, L. Elliott, J. Roach, “The seL4 Microkernel – A Robust, Resilient, and Open-Source Foundation for Ground Vehicle Electronics Architecture”, In Proceedings of the Ground Vehicle Systems Engineering and Technology Symposium (GVSETS), NDIA, Novi, MI, Aug. 13-15, 2019.