Securing outer space with seL4

Welcome to 2017: we have self-driving cars, mag lev trains, Tesla’s SpaceX and now: seL4-powered mini satellites in space. We at Trustworthy Systems had the opportunity to use one of them as a research machine and we’ve completed a seL4-based system which has been launched into low earth orbit.

Want more info? Well it’s coming at you now.

So what kind of satellite are we talking about?

The mini satellite that seL4 is powering is a CubeSat: a small cuboid satellite that is usually deployed from another orbital vehicle. In our case the particular CubeSat being used is one provided by QB50, a research consortium that attempts to make space research easier by providing accessible, relatively cheap vehicles. Our CubeSat will join 49 other CubeSats in taking readings and measurements of the conditions in the lower thermosphere (approximately 200-380km up).

The precise launch sequence for our own CubeSat box is that it was carried up to the International Space Station on an Atlas-V expendable resupply rocket, and then from there it will be deployed along with 37 other CubeSats into orbit. “Houston, we have lift off!”

What kinds of measurements will the satellite be taking?

The QB50 consortium’s information page is probably going to be able to explain that better than we can – for the specific measurements that will be taken, see the “Scientific Research” section on their “Mission Objectives” page.

Value gained:

It was pretty cool to be able to work on writing a minimal ADC (“Attitude Determination and Control”) system using the algorithm we were provided with. The ADC is the software that will enable the CubeSat device to stabilize and manage its position while in orbit, similar to a flight system for an aeroplane.

We were also able to once again leverage and show our ability to secure information flow between software components with different levels of trustworthiness – our strong isolation guarantees held true.

We’re confident that out seL4-CubeSat system will meet its functional and non-functional requirements – and make seL4’s case for use in similar projects in the future!

Wow: seL4 in outer space, huh?

Yup. It’s as surreal and exciting for us as we hope it is for you: Use the seL4 contact page to stay updated. And always keep an eye out for new blog posts right here. We’ve got other neat stuff ongoing in the pipeline.