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.
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.
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:
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.
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.
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.
We’re ramping up our efforts to reach out to our community. We want your input and we want to know what you think you can do with seL4.
From us at Trustworthy Systems to you, our customers, our well-wishers, and our peers: thank you for your support.