High Assurance Virtualization forthe HPSC

In this proposed effort, DornerWorks will develop anbsp;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 fornbsp;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 ldquo;end to endrdquo;, 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.nbsp;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 configurationnbsp;files needed to support VM-based systems.