Trustworthy Systems


The DARPA HACMS project has been completed. We are now involved in a new DARPA project, the CASE project.

The goal of the DARPA HACMS (High-Assurance Cyber Military Systems) program was to create technology for the construction of high-assurance cyber-physical systems. Such systems are functionally correct and satisfy appropriate safety and security properties. This requires a fundamentally different approach from what the software community has taken to date. HACMS adopted a clean-slate, formal methods-based approach to enable semi-automated code synthesis from executable, formal specifications.

Beyond the defence funding and motivation, the project, and especially TS's contribution, provided core technologies for protecting a wide range of cyber-physical systems from attacks. Examples are civilian aircraft, implanted medical devices, cars and other transport systems, robots and industrial plants.

TS's contribution to HACMS was performed by the Trustworthy Systems group and focussed on the operating-system layer, the lowest and most critical software layer of any high-assurance systems.

The HACMS project consisted of two teams: an Air Team and a Ground Team. The air team developed and applied HACMS technologies to build highly hack-resilient unmanned aerial vehicles (UAVs), while the ground team did this to build highly hack-resilient autonomus ground vehicles.

The Trustworthy Systems group was involved in both air team and ground team.

Air Team: SMACCM


SMACCM was the Air Team funded to build highly hack-resilient unmanned aerial vehicles UAVs under DARPA's HACMS program. SMACCM (which stands for Secure Mathematically-Assured Composition of Control Models) was a joint 18 million USD project running for 4.5 years. The team consisted of formal verification and synthesis groups in Rockwell Collins, TS, Galois Inc, Boeing and the University of Minnesota.

DARPA Boeing Boeing Galois University of Minnesota Rockwell Collins


The SMACCM project investigated the problem space from the angles of formal integration (Rockwell Collins & Univ Minnesota), flight control synthesis (Galois), operating system (TS), and real-life challenge problems (Boeing).

The techniques were demonstrated on unmanned air vehicles, in particular on an open research platform, for which the software was replaced from the ground up, and on a commercial platform, where HACMS software, including the seL4 kernel, ran together with existing systems.

The research vehicle was based on a 3D Robotics Iris+ quad copter, and combines two separate processing platforms: a microcontroller-based flight computer to handle real-time flight control, and a more powerful mission board to handle more complex tasks. The flight controller ran the verified eChronos RTOS together with smaccmpilot, the redesigned flight code. The mission board ran on seL4, with non-critical code running in a virtualised Linux instance and critical code (handling device access, communications with ground control, sensor inputs, etc.) running as native seL4 components.

SMACCMCopter Block diagram of SMACCMCopter

The commercial platform serves for technology transfer. The Unmanned Little Bird (ULB) is an optionally-piloted autonomous helicopter under development at Boeing. Like the research vehicle, it has separate processor boards for low-level flight control and high-level mission operations. Much of the technology developed for the research platform will be ported or repeated on the ULB. In particular, the high-level mission operations ran on seL4.


Ground Transition Team

The Ground Transition Team (GTT) took a slightly different approach from the air team in building highly hack-resilient autonomous vehicles. The GTT approach was to develop a Mixed-Assurance Software Toolchain (MAST) that enabled non-experts to produce mixed-assurance software. MAST systems allow software of different assurance levels to co-exist, with higher assurance components being protected from lower assurance components. Also MAST focusses on synthesis of much of the higher-assurance component code. The GTT was lead by HRL and has contributions from TS, MIT, University of Illinois, CMU, Princeton University, University of Minnesota, Galois Inc, and US Army's TARDEC.

As with the air team the ground team had two demonstration vehicles: a research vehicle and a commercial platform. In both cases, seL4-based software replaced or combined with existing systems to provide improved security using high-assurance software.

The research vehicle was based on a TARDEC GVR-Bot while the commercial platform was a TARDEC AMAS (Autonomous Mobility Applique System) on an autonomous HET (Heavy Equipment Transporter).




Most of the code in this project is open source. Check out seL4 on github and the eChronos RTOS on github. Code for the ArduCopter and IRIS research platforms is available on



The following activities in our Trustworthy Systems research are part of the SMACCM project:

  • eChronos RTOS: a highly configurable high-assurance real-time OS for resource-constrained micro-controllers without memory protection.
  • Automatic Device Driver Synthesis: generating drivers automatically from formal specifications, resulting in correct-by-construction device drivers and reducing the effort involved in development and testing.
  • Trustworthy Component Framework: developing component-based systems, resulting in formally verified code for the trusted components, including the system initialisation components, guaranteeing that the system is set-up as required by the architecture.
  • Trustworthy File Systems: design, implementation, and synthesis of provably correct file systems.
  • Information Flow: formally proving that seL4 enforces information flow control, guaranteeing isolation between trusted and untrusted components.
  • Real Time: providing sound upper bounds on interrupt latencies for seL4, making it usable in safety-critical systems.
  • Analysis of Protocols for High-Assurance Networks: providing authentication and reliable communication protocols for unmanned aerial vehicles (UAVs).
  • Verification Tools and Automation: further develop and increase the use of automation in formal verification, resulting in efficient and repeatable methodologies.
  • Proving Compiler Correctness: eliminating the compiler correctness assumption of the original seL4 functional correctness proof, using translation validation approach.
  • seL4 Kernel: continuing to develop seL4 to make it the system of choice as a trustworthy foundation for complex software systems. In particular, the SMACCM project is investigating the addition of support for ARM hardware virtualisation techniques.

Related Publications


Abstract PDF Gernot Heiser, Gerwin Klein and June Andronick
seL4 in Australia: From research to real-world trustworthy systems
Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020
Abstract PDF Darren Cofer, Andrew Gacek, John Backes, Michael Whalen, Lee Pike, Adam Foltzer, Michael Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser and Douglas Stuart
A formal approach to constructing secure air vehicle software
IEEE Computer, Volume 51, Issue 11, pp. 14-23, November, 2018
Abstract PDF Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez
Formally verified software in the real world
Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018
Abstract PDF Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson
Secure mathematically-assured composition of control models
Technical Report, Data61, CSIRO, September, 2017
Abstract PDF Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray and Liam O'Connor
Provably trustworthy systems
Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104, pp. 1-23, September, 2017
Abstract PDF Rob van Glabbeek and Peter Hoefner
Split, send, reassemble: A formal specification of a CAN bus protocol stack
2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), pp. 14-52, Uppsala, Sweden, April, 2017
Abstract PDF Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein
Refinement through restraint: Bringing down the cost of verification
International Conference on Functional Programming, Nara, Japan, September, 2016
Abstract PDF Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser
Cogent: verifying high-assurance file system implementations
International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175–188, Atlanta, GA, USA, April, 2016
Abstract PDF Sidney Amani and Toby Murray
Specifying a realistic file system
Workshop on Models for Formal Analysis of Real Systems, pp. 1–9, Suva, Fiji, November, 2015
Abstract PDF Franck Cassez, Takashi Matsuoka, Ed Pierzchalski and Nathan Smyth
Perentie: Modular trace refinement and selective value tracking
SV-COMP-2015, pp. 439–442, London, UK, April, 2015
Abstract PDF Liam O'Connor, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah
CDSL version 1: Simplifying verification with linear types
Technical Report, NICTA, October, 2014
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract PDF Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
PDF Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick
Towards a verified component platform
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
PDF Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser
File systems deserve verification too!
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, Pennsylvania, USA, November, 2013
A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64.
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013
Abstract PDF Toby Murray and Thomas Sewell
Above and beyond: seL4 noninterference and binary verification
Abstract, 2013 High Confidence Software and Systems Conference, Annapolis, MD, May, 2013.
Abstract PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein
Noninterference for operating system kernels
International Conference on Certified Programs and Proofs, pp. 126–142, Kyoto, Japan, December, 2012
Abstract PDF Matthew Fernandez, Ihor Kuz and Gerwin Klein
Formalisation of a component platform
Poster presented at Operating Systems Design and Implementation 2012, October, 2012
Abstract PDF Gernot Heiser, Toby Murray and Gerwin Klein
It's time for trustworthy systems
IEEE Symposium on Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012