Advanced science.  Applied technology.

Search

seL4 Operating System for Space Platforms Targeting Open-Source RISC-V Processors, 10-R6188

Principal Investigators
Mark Johnson
Gabriel Kanelopoulos
Inclusive Dates 
07/07/21 - Current

Background

Advances in computing capabilities and demands for more fully-functioned flight software applications have sparked an increase in the deployment of mixed-criticality systems (MCS), where multiple applications of various criticality execute sharing processor resources and memory. This presents opportunities to reduce costs as more functionalities can be packed on the same machine. However, this presents significant potential for faults, as application partitions can corrupt one another or starve one another for processor time. The objective of this ongoing research is to utilize and/or extend the novel, high assurance capability-based seL4 microkernel to create a reusable, secure flight software stack in support of deploying MCS, while also protecting against common weaknesses of MCS.

Approach

The approach taken by Southwest Research Institute® involves four primary technical tasks which are:

  1. Analyze and benchmark what is offered in seL4 to support robust application partition isolation by default;

  2. Design a sample MCS application competing for system resources with various failure modes;

  3. Upgrade the kernel to implement a MCS hypervisor;

  4. Validate and benchmark the performance of the hypervisor against the failure modes of the application.

Accomplishments

The initial state of the kernel’s security mechanisms was benchmarked and characterized. A sample MCS application was created with clear failure modes and an MCS hypervisor was created. We have shown that memory and processor time is isolated in this sample MCS application, with faults in partitions being caught and handled.