NASA Launches Space Cyber-resilience into a New Era with the seL4 Microkernel

Posted on June 18, 2020 by Matthew Russell

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.

Space technology continues to grow in complexity and processing demands.
Space technology continues to grow in complexity and processing demands.

The Problem: Pushing technology to the limit

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.

DornerWorks helps companies develop technology that can withstand harsh radiation in space.
Source: Wikimedia Commons
DornerWorks helps companies develop technology that can withstand harsh radiation in space.

The Solution: Multiplying capabilities through virtualization

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.

The Plan: Overcoming seL4 microkernel complexity

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:

  1. Create an seL4 SDK to support and expand NASA’s HPSC ecosystem. This SDK will include tools, processes and workflows to simplify the process of configuring and deploying VMs to a multi-core ARMv8 system, like the HPPS on the HPSC or APU on the MPSoC. By the end of this project this development tool will be ready for commercialization supporting various operating systems and hardware, such as Linux, RTEMS, FreeRTOS™, and VxWorks® on HPSC, ZCU102, Ultra96, and Raspberry PI 4 target platforms. We expect to be at TRL 6 for this tool, where the relevant environment is a desktop or cloud-based development environment.
  2. Add additional features to the seL4 VMM, such as SMP support and ARINC-653 scheduling to meet HPSC requirements and NASA’s general needs. We expect these seL4 additions to be at TRL 5 for HPSC, assuming the development board will not be available in this project’s timeframe, and TRL 6 for the Xilinx MPSoC/RFSoC and Raspberry Pi 4.

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:

  • Reduce development cycle time
  • Simplify system configuration
  • Enable focus on your application instead of the platform
  • Minimize premature investment in seL4 expertise
  • Provide solutions to developmental challenges:
    • Repository management
    • Tracking multiple VM configs
    • Identifying components that need to be built for the specified target
    • Configuring seL4 and CAmkES

Ensuring consistency between various software components and configuration files

This SBIR effort will focus on creating an seL4 configuration tool to support and expand NASA’s HPSC ecosystem.
Source: Joint Base Langley-Eustis
This SBIR effort will focus on creating an seL4 configuration tool to support and expand NASA’s HPSC ecosystem.

Building products for space

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.

Matthew Russell
by Matthew Russell