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 Data61'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.
Data61'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.
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, Data61 (formerly NICTA), 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 (Data61), 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.
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 differnt 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 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 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 http://smaccmpilot.org
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.
|
 |
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 |
Past
|