In this proposed effort, DornerWorks will develop a software development kit (SDK) to help developers defeat the steep learning curve of using the formally proved seL4 microkernel as a high assurance bare metal hypervisor for the HPSC. Doing so supports the SBIR topic interest in having a fault tolerant, bare metal hypervisor for the HPSC, supporting asymmetric and symmetric multi-processing for operating systems, such as Linux and RTEMS.
seL4 is a member of the L4 family of high-performance microkernels developed, maintained, and formally verified by the Trustworthy Systems Group at Data61. seL4 is owned by General Dynamics, which released it under the open source GPLv2 license in 2014. This microkernel has been proven correct via a formal mathematical proof using Isabelle/HOL, an interactive Higher Order Logic theorem prover. The proof guarantees that seL4 correctly implements its specifications, e.g., is free from buffer overflows, has no null pointer exceptions, never hangs, etc. A second proof guarantees that the binary executable is a correct translation of the source code. Thus, the kernel is proven correct “end to end”, from specification to executable. Furthermore, the architecture of seL4 is cleverly designed to provide important security properties while retaining good performance. The seL4 follows microkernel design principles by delegating typical operating system (OS) features up to user applications via Capability objects that determine specifics feature and access privileges. The result is that seL4 is one of the fastest microkernels on the supported platforms.
However, there is a steep learning curve with seL4, which is further complicated when using the hypervisor functionality to host multiple virtual machines running different operating systems, an HPSC system requirement. The proposed SDK will handle the complexity of configuring and building the various OS kernels, files systems, and configuration files needed to support VM-based systems.
This effort will simplify use of virtual machine-based architectures on the HPSC, Xilinx MPSoC/RFSoC-based, and Raspberry Pi 4 platforms. The HPSC is targeted for Rover, Landers, High Bandwidth Instrument, and SmallSat/Constellation missions, with immediate possible projects including Mars Fetch Rover, WFIRST/Chronograph, Gateway, and SPLICE/Lunar Lander. Innoflight’s CFC-400 and NASA’s SpaceCube 3.0 use the MPSoC. The Raspberry Pi 4 can be used for low cost prototyping or creation of a low cost distributed mission test bed.
An easy-to-use, provably correct micro-hypervisor is valuable for applications and products requiring high assurance software design for safety and/or security. Traditionally these kinds of products have been found in aerospace, defense, and industrial markets, but cyber-security is becoming increasingly critical for medical, IoT, and automotive markets.