Have you ever seen the cargo manifest of a NASA rocket? It’s the definition of exact measures. The crews’ clothing, the vehicle hardware, even the CD case is weighed and accounted for. Rocket scientists need precise data or they’ll get an imprecise result.
In 1969, NASA sent astronauts into space with the Apollo Guidance Computer. It had 64 Kb of memory, a top speed of 0.043 MHz and ran all the essential calculations the crew needed to leave orbit and return home. Today, most NASA space craft are operated by computers based on PowerPC based processors for space applications. They’re faster and much more capable than the original Apollo technology but just as rapidly moving toward obsolescence.
A major problem facing space-qualified technology is the time it takes to design and fabricate a radiation hardened version of a commercial chip. NASA’s PowerPC solution is able to shield critical data and processes from radiation but unable to take advantage of more recent software innovations.
The High-Performance Spaceflight Computing (HPSC) platform will move NASA technology into the next era, enabling a greater processing load without burdening spacecraft with added size, weight, and power (SWaP). The new heterogeneous multi-processor ARM®-based platform will mark an estimated two-orders of magnitude increase in computing power, which will support more of the existing and emerging applications being incorporated into space travel.
This advantage also poses a challenge for the space-based system integrators who must consolidate those applications on a single integrated system.
One solution to this challenge is the virtualized platform DornerWorks began developing for NASA during a Phase I Small Business Innovation Research (SBIR) contract. The initial stages of that development focused on expanding the Xen Hypervisor ecosystem to support NASA requirements. For Phase II of the SBIR, DornerWorks is using the seL4 microkernel, which also enables virtualized systems.
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 distributed under the open source GPLv2 license. This microkernel has been proven correct via a formal mathematical proof when used on verified hardware platforms in specific configurations. 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.
The architecture of seL4 is also designed to provide important security properties while retaining good performance. seL4 follows microkernel design principles by delegating typical Operating System (OS) features up to user applications via Capability objects that determine specific feature and access privileges. The result is that seL4 is one of the fastest and most secure microkernels on the supported platforms.
DornerWorks seL4 virtual machine (VM) Composer will put these advantages in the hands of system integrators, providing a trusted foundation for high-assurance systems. A CAmkES (component architecture for microkernel-based embedded systems)-based virtual machine monitor (VMM), originally developed by CSIRO’s Data61, can be used to host VMs supporting AMP, SMP, or a mix of both on a multi-core processor, enabling richer software architectures using different operating systems.
Developers face a steep learning curve when working with the seL4 microkernel. This difficulty is compounded by an ecosystem that lacks the number and quality of development tools enjoyed by other open source hypervisor ecosystems.
Up until now, processing limitations have gotten in the way of running VMs with multiple cores. DornerWorks will be concentrating on solving this problem and making seL4 development easier for space system integrators as part of the Phase II effort by achieving two technical objectives:
The completed Phase II SBIR will leave NASA with a more secure platform for running mission-critical applications in space. Other companies will also be able to use the open sourced portion of the seL4 VMM, a free version of it supporting Linux and Raspberry Pi, for their own development. This will help teams:
Ensuring consistency between various software components and configuration files
You won’t reach low-earth orbit without a tested flight plan. Just as rocket launches require meticulous planning and foresight, preparing products for space is no trivial matter.
Using virtual machines can help in the harsh space environment by improving fault containment. In an architecture with only a single OS or kernel, an event anywhere in memory has the potential of cascading and taking down the whole system. In a system partitioned into virtual machines, events occurring in the virtual machines are contained to that virtual machine, giving the system a chance to detect and react to, or recover from, the event.
Running the virtualized systems enabled by the seL4 microkernel on radiation-hardened hardware that can leverage its advance security features opens a unique path to dominance in the space-qualified product market.
