UAVs and other military aircraft have off-vehicle network connections for command and control, sharing sensor data, and coordination with other forces. This connectivity provides tremendous new functionality, but also exposes these military assets to the same security risks that plague our PCs and web servers.
Security is an emergent property of a system. This means there is not a special box in the system that provides security. We have to look at the whole system and how its components interact with each other and the outside world. Vulnerabilities can arise from the "front door" (network protocols), component errors (software bugs), or unintended interactions between otherwise correct components.
Current approaches to cyber security rely on patching systems after a vulnerability is discovered. What is needed is a clean-slate, mathematically-based approach for building secure software. DARPA initiated the HACMS program (High Assurance Cyber Military Systems) to develop the technologies needed to counter cyber threats to network-enabled embedded systems.
Collin Aerospace (Rockwell Collins at the time) led the Secure Mathematically-Assured Composition of Control Models (SMACCM) project in the DARPA HACMS program. The SMACCM project developed new tools for building UAV software that is provably secure against many classes of cyber attack. Our goal in SMACCM was to provide not just security, but verifiable security; that is, system designs for which we can have confidence in and evidence of security. We developed system architecture models, software components for mission and control functions, and operating system software, all of which have been mathematically analyzed to ensure key security properties.
Unique aspects our approach include:
- Integration of proof and software engineering
- Formally verified operating system software
- High-assurance control components based on formal design languages and synthesis
We prototyped these new technologies on a research quadcopter, and then transitioned them to Boeing's Unmanned Little Bird (ULB) helicopter to demonstrate their practicality and effectiveness. Our integrated tools for architectural modeling, analysis, and synthesis (shown in the figure) make this approach practical and effective. These tools for secure software development and analysis are available for transition to other vehicle programs ( AGREE and Resolute).
At the end of each phase of the project, the HACMS Red Team was given six weeks and full access to the source code for both vehicles to evaluate their cyber security claims. They were unable to compromise the security of either vehicle.
All of the models, software, and tools developed as part of this project are open source and available in the SMACCM github repository. Details on construction of the research quadcopter can be found at smaccmpilot.org. More information is available in the project final report.
Phase 3 final demonstration, including cyber attacks on the research quadcopter and video about the Boeing ULB final demonstration.
HACMS program explainer. This provides a nice overview of the technologies and accomplishments.
More interviews with current and former DARPA program managers and HACMS researchers.
Larger version of the ULB Phase 3 final demonstration video (which was embedded in the Phase 3 final demo video above).
An overview of the project, with some bits of our Phase 2 demo on the SMACCMcopter:
At the end of phase 2 (July 2015), we conducted a flight test of Boeing's ULB running SMACCM software, including the seL4 microkernel:
A brief introduction to the goals of the project:
Phase 1 SMACCM quadcopter on 60 Minutes:
A nice overview of Phase 1 of the project from our partners at Data61:
Phase 1 overview from our partners at Galois: