SMACCM: TS in the DARPA HACMS Program

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.

• Aim: The aim of the DARPA HACMS program was 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 was 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 reduces the effort that needs to be expended for the verification of new systems, and formal design from the start helped to integrate different formal analyses into a coherent whole.

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.

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.

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).

News

• Dec 2023: DARPA selects HACMS as their 2023 10 Year Game Changer program, as the most impactful program viewed from ten years' distance.
• Mar 2018: Video of Kathleen Fisher explaining HACMS on Big Think.
• Oct 2017: SMACCM final report available at here and at 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.

Code

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 https://smaccmpilot.org

Videos

• 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, Video 2):
  
   
   
• 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 attack:
  
   
• The US Secretary of Defense about HACMS and the use of formal methods (starting at 10:37):
  
   
• 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 HACMS program:
  
   
• Our partners at Rockwell Collins with a drone hacking demo:
  
   

Activities

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

		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
		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
		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
		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, 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
		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
		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, 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, 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
		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

People