DARPA’s HACMS Program Seeks to Create New Technology

DARPA’s High-Assurance Cyber Military Systems (HACMS) program seeks to improve the security of embedded computer systems. Credit: DARPA

DARPA’s High-Assurance Cyber Military Systems program seeks to improve the security of embedded computer systems. To do this, researchers are looking to create new technology for the construction of systems by adopting a method-based approach to enable semi-automated code synthesis from executable, formal specifications.

Embedded computer systems play a part in every aspect of DoD technology. The software in these systems does everything from managing large physical infrastructures, to running peripherals such as printers and routers, to controlling medical devices such as pacemakers and insulin pumps. Networking these embedded computer systems enables remote retrieval of diagnostic information, permits software updates, and provides access to innovative features, but it also introduces vulnerabilities to the system via remote attack.

“The High-Assurance Cyber Military Systems (HACMS) program seeks to create technology for the construction of systems that are functionally correct and satisfy appropriate safety and security properties,” explained, Kathleen Fisher, DARPA program manager. “Our vision for HACMS is to adopt a clean-slate, formal method-based approach to enable semi-automated code synthesis from executable, formal specifications.”

In addition to generating code, HACMS seeks a synthesizer capable of producing a machine-checkable proof that the generated code satisfies functional specifications as well as security and safety policies. A key technical challenge is the development of techniques to ensure that such proofs are composable, allowing the construction of high-assurance systems out of high-assurance components.

Key HACMS technologies include semi-automated software synthesis systems, verification tools such as theorem provers and model checkers, and specification languages. HACMS aims to produce a set of publicly available tools integrated into a high-assurance software workbench, widely distributed to both defense and commercial sectors. In the defense sector, HACMS plans to enable high-assurance military systems ranging from unmanned ground, air, and underwater vehicles, to weapons systems, satellites, and command and control devices.