The SMACCM project @ Data61
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.
Despite 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 SMACCM is the operating-system layer, the lowest and most critical software layer of any high-assurance systems. The main activities in SMACCM are part of our Trustworthy Systems umbrella.
Aim: The aim of the DARPA HACMS program and of the SMACCM project in this 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.
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, the Iris quad copter, for which the software is being replaced from the ground up, and on a real helicopter, the Unmanned Little Bird (see below), where HACMS software, including the seL4 kernel, will run together with existing systems.
The research vehicle 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.
- May 2016: Video from Rockwell Collins showing the latest quadcopter demo.
- 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
- 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
ULB flying with seL4 on-board:
- 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:
- Rockwell Collins Video demo of the quadcopter flying and resisting attack:
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 nicta.com.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