Starting 2017 off strong

April 6th, 2017

Starting 2017 off strong.

At Trustworthy Systems, we’ve achieved major cyber-security milestones funded by the US Department of Defense over the last few years. Delve with us into the results of the DARPA High Assurance Cyber-Military Systems project, where we take an autonomous helicopter, and demonstrate that seL4 can deliver on military-grade promises of security and reliability using formal methods and a small trusted computing base.

It’s a celebration for all of us: as an industry we’ve made greater strides toward a secure, connected world, which makes us all winners.

Before we celebrate – what exactly have we achieved?

After much intense work and challenging engineering (and a lot of fun, too) we have managed to deliver a seL4-based system to DARPA as part of a project to enhance the security of critical systems, whether military or civilian, across the industry.

Our work on the HACMS was done in 3 stages, across a total of four hardware platforms. Two of the platforms are air-vehicles: a small quacopter research drone which was used as the demo platform which gave us the opportunity to redo the whole system from the ground up in collaboration with our partners; and a fully functional autonomous research helicopter, the Boeing ULB (“Unmanned Little Bird”). We’re pleased to announce that these two machines now run on seL4.

The other two platforms are two ground-vehicles: a small US Army Robotics reference platform called the GVR-BOT; and the full featured target platform, the HET (“Heavy Equipment Transporter”). Both of these machines now also run on seL4.

The ULB and the two land vehicles have also been made cyber-hard through a “seismic security retrofit” strategy which is essentially one of several ways to enhance the security of existing systems by leveraging the seL4-enforced isolation guarantees, and it was a great fit for our partners in using seL4.

We are proud to announce our success in delivering, in collaboration with our partners, full seL4-based systems for the air-vehicles. We’ve also got some goodies for our readers: check out the exciting footage below!

You can also read the full description of our work on the DARPA SMACCM project to get a better picture of what the project is about.

Significance – our progress:

Even as we celebrate our steps forward, we must keep a keen focus on making sure that both our present and future work has real world impact. What we and our partners have done in this milestone is:

Evaluated seL4 as a real-world embedded platform.
Assessed seL4’s performance in a real-world environment.
Convincingly demonstrated that seL4 delivers on its promise of providing solid isolation of components in a mixed-trustworthiness system.
Along with our partners, encountered and overcome issues in deploying both our bespoke CAmkES architecture, as well as their high-assurance development frameworks which has matured both our tools and approach to integrating and constructing secure systems.
Integrated our CAmkES framework with the industry-standard AADL tools that support a model-driven design methodology. The automation resulting from this integration massively increases the assurance of our systems.

Contributions – our impact:

While marching toward this milestone, we’ve also shown the importance of formal methods. At Trustworthy Systems, we have a strong belief in and commitment to the improvement of the discipline of formal verification of software. We want to drive the costs of formal verification down, and pioneer the development lifecycles and methodologies that will enable verification to be deployed at scale throughout the software industry.

We are committed to making an impact and continually pushing the state of the art until it sees wide adoption.

Let’s not forget our heroes.

This project has been especially challenging for our Formal Methods team. Our proof engineers came together to deliver a stellar result under tight time constraints, showing true grit.

Our partners:

We’ve had the blessing and opportunity to work with very keen minds and it’s been a humbling experience to observe the very best at work from all across the security community.