The HACMS project @ Data61
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 is 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 adopts a clean-slate, formal methods-based approach to enable semi-automated code synthesis from executable, formal specifications.
Aim: The aim of the DARPA HACMS program is to fundamentally raise the bar and lower the development cost for high-assurance cyber-physical systems.
Approach : The approach to building high-assurance systems in HACMS is to use formal design, synthesis, and verification from the ground up. Recent projects like our microkernel verification have shown that formal verification can scale to real-life systems. Synthesis will reduce the effort that needs to be expended for the verification of new systems, and formal design from the start will help to integrate different formal analyses into a coherent whole.
Beyond the defence funding and motivation, the project, and especially Data61's contribution, provides 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.
Data61's contribution to HACMS is performed by the Trustworthy Systems group and focusses on the operating-system layer, the lowest and most critical software layer of any high-assurance systems.
The HACMS project consists of two teams: an Air Team and a Ground Team. The air team develops and applies HACMS technologies to build highly hack-resilient unmanned aerial vehicles (UAVs), while the ground team does this to build highly hack-resilient autonomus ground vehicles.
The Trustworthy Systems group is involved in both the air team and the ground team.
Air Team: SMACCM
SMACCM is 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) is a joint 18 million USD project running for 4.5 years. The team consists of formal verification and synthesis groups in Rockwell Collins, Data61 (formerly NICTA), Galois Inc, Boeing and the University of Minnesota.
The SMACCM project investigates the problem space from the angles of formal integration (Rockwell Collins & Univ Minnesota), flight control synthesis (Galois), operating system (Data61), and real-life challenge problems (Boeing).
The techniques will be demonstrated on unmanned air vehicles, in particular on an open research platform, for which the software is being replaced from the ground up, and on a commercial platform, where HACMS software, including the seL4 kernel, will run together with existing systems.
The research vehicle is 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 is running the verified eChronos RTOS together with smaccmpilot, the redesigned flight code. The mission board is running 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.
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 will run on seL4.
Ground Transition Team
The Ground Transition Team (GTT) is taking a slightly different approach to th e air team to build highly hack-resilient autonomous vehicles. The GTT approach is to develop a Mixed-Assurance Software Toolchain (MAST) that enables non-experts to produce mixed-assurance software. MAST systems allow software of differnt assurances 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 is lead by HRL and has contributions fom Data61, 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 has two demonstration vehicles: a research vehicle and a commercial platform. In both cases, seL4-based software will replace or combine with existing systems to provide improved securtiy using high-assurance software.
The research vehicle is a based on a TARDEC GVR-Bot while the commercial platform is a TARDEC AMAS (Autonomous Mobility Applique System) on an autonomous HET (Heavy Equipment Transporter).
- Mar 2018: Video of Kathleen Fisher explaining HACMS on Big Think.
- Oct 2017: SMACCM final report available at Data61 and Loonwerks.
- Sep 2017: The HACMS program: using formal methods to eliminate exploitable bugs in Philosophical Transaction of the Royal Society A. An overview of HACMS by the 3 program managers.
- Apr 2017: HACMS project complete. Final demo held at Sterling, VA, USA Video summarising the project and demos (both air and ground). See below for more videos of the final demos.
- May 2016: Video from Rockwell Collins showing the latest quadcopter demo.
- Feb 2016: Video of Gernot Heiser's presentation about HACMS at linux.conf.au 2016.
- Nov 2015: seL4 and SMACCM technologies will also be used on ground vehicles in the HACMS project.
- Oct 2015: Video of ULB flying with seL4 on-board.
- Sep 2015: Video of the US Secretary of Defense talking about HACMS and formal methods.
- Aug 2015: the eChronos RTOS has gone open source!
- Aug 2015: Another PI meeting and demo day, and another successful air team demo. This time we added an seL4-powered mission board to the quad copter, handling communication, encryption, and providing an untrusted virtualised Linux instance for the Red Team to attack.
- Jul 2015: ULB had a succesful flight with seL4 (including virtualisation support) and CAmkES driving the mission computer.
- Feb 2015: HACMS and SMACCM featured on CBS's 60 Minutes. With extra quad copter content.
- Jul 2014: seL4 has gone open source!
- Mar 2014: seL4 and virtualisation support running on the ULB platform.
- Feb 2014: Code-level properties of the eChronos RTOS proved by model checking.
- Jan 2014: PI meeting and demo day, successful air team demo. The eChronos RTOS now flies the SMACCMCopter.
- Sep 2013: The Unmanned Little Bird in IEEE Spectrum: Robocopters to the Rescue.
- Aug 2013: More HACMS in the news: at Signal Magazine and DIYDrones.
- Aug 2013: Milestone delivered: drivers and seL4 specification extensions.
- Jul 2013: Joint PI meeting of HACMS with two other DAPRA programs. Gernot gave a keynote seL4 and related activities. Work with partners will be concentrating on getting a quadcopter demo flying in Jan that shows off high assurance HACMS software, including Ivory components from smaccmpilot.org and a new locally-developed microcontroller RTOS.
- May 2013: SMACCM project is featured at CeBIT Australia. We are showing hacking and security demos.
- May 2013: Milestone delivered: ADL behaviour specification and preliminary protocol analysis
- Mar 2013: Our partners at Rockwell Collins show a drone hacking demo.
- Feb 2013: PI meeting. The Red Team managed to comprehensively break into and take control over all base-line research platforms (running unverified standard software) in the HACMS program. This is good. It will enable us to show that our techniques prevent attacks when the platforms start running with our own software.
- Feb 2013: Milestone delivered: drivers and extensions for research platform.
- Dec 2012: HACMS program featured by Wired.
- Nov 2012: Milestone delivered: first formal specification of component platform.
- Aug 2012: Official kickoff.
Most of the code in this project will be open source. Check out seL4 on github and the eChronos RTOS on github. Code for the ArduCopter and IRIS research platforms is available on http://smaccmpilot.org
- HACMS Explainer
and Walk In Comments
Videos from the final demo providing a good overview of the
achieved results from the project:
SMACCM ULB Videos from the final demo (Video 1,
- SMACCM quadcopter Video
from the final demo:
- Ground Team HET Video
from the final demo:
- Rockwell Collins
Video demo of the quadcopter flying and resisting
- The US Secretary of Defense about
HACMS and the use of formal methods (starting at
- Using NICTA's verified OS technology for protecting UAVs (and other cyber-physical systems): MP4 Video
- A CBS 60-Minutes
segment with former HACMS program manager Kathleen
Fisher shows our friends from Galois demonstrating the same
attack (but without the demonstration of how SMACCM
technology can defeat it):
"Creating drones that can't be hacked" by cbsnews
- DARPA program manager Kathleen Fisher introduces the
- Our partners at Rockwell Collins with a
drone hacking demo:
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.
Gerwin Klein, gerwin.klein data61.csiro.au
|Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez|
Formally verified software in the real world
Communications of the ACM
|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
|Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk and Toby Murray|
Provably trustworthy systems
Philosophical Transactions of the Royal SocietyA, Volume 375, pp. 1-23, September, 2017
|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
|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
|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
|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
|Liam O'Connor-Davis, 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
|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
|Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz|
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
||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
|Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray|
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
||Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor-Davis, 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.
||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
||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
|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.
|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
|Matthew Fernandez, Ihor Kuz and Gerwin Klein|
Formalisation of a component platform
Poster presented at Operating Systems Design and Implementation 2012, October, 2012
||Sidney Amani, Leonid Ryzhyk and Toby Murray|
Towards a fully verified file system
Poster presentation at EuroSys Doctoral Workshop, Bern, Switzerland, April, 2012
|Gernot Heiser, Toby Murray and Gerwin Klein|
It's time for trustworthy systems
IEEE Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012