NASA SBIR 2019-II Solicitation

Proposal Summary

 19-2- Z6.01-3138
 High Performance Space Computing Technology
 High Assurance Virtualization for the HPSC
SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
DornerWorks, Ltd.
3445 Lake Eastbrook Southeast
Grand Rapids, MI 49546
(616) 245-8369

PRINCIPAL INVESTIGATOR (Name, E-mail, Mail Address, City/State/Zip, Phone)
Jarvis Roach
3445 Lake Eastbrook SE
Grand Rapids, MI 49546 - 5935
(616) 389-8341

BUSINESS OFFICIAL (Name, E-mail, Mail Address, City/State/Zip, Phone)
Lance Hilbelink
3445 Lake Eastbrook SE
Grand Rapids, MI 49546 - 5935
(616) 245-8369

Estimated Technology Readiness Level (TRL) :
Begin: 4
End: 6
Technical Abstract (Limit 2000 characters, approximately 200 words)

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.

Potential NASA Applications (Limit 1500 characters, approximately 150 words)

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.



Potential Non-NASA Applications (Limit 1500 characters, approximately 150 words)

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. 

Duration: 18

Form Generated on 05/04/2020 06:26:30