U.S. DARPA's program on High-Assurance Cyber-Secured Military Vehicles

News Report

As announced by Fbo.Gov, the U.S. Defense Advanced Research Projects Agency (DARPA) will conduct on February 21st a dedicated briefing in support of the High-Assurance Cyber Military Systems (HACMS) program. The objectives of the event are to familiarize participants with DARPA’s interest in innovative approaches to high-assurance cyber military systems, and to promote discussion of synergistic capabilities among potential program participants.

The Context

Embedded systems form a ubiquitous, networked, computing substrate that underlies much of modern technological society. Embedded systems have been networked for a variety of reasons, including the ability to conveniently access diagnostic information, perform software updates, provide innovative features, lower costs, and improve ease of use. To a first approximation, air-gapped systems no longer exist. Researchers and hackers have shown that these kinds of networked, embedded systems are vulnerable to remote attack and that such attacks can cause physical damage while hiding the effects from monitors.

The goal of the DARPA's HACMS program is to create technology for the construction of high-assurance cyber-physical systems, with a special focus on the vehicle space. HACMS will produce a set of publicly available tools integrated into a high-assurance software workbench, which will be widely distributed for use in both the commercial and defense software sectors. HACMS will use these tools to generate open-source, high-assurance operating system and control system components, and then will use these components to construct high-assurance military vehicles.

Achieving this goal requires a fundamentally different approach from what the software community has taken to date. HACMS will adopt a clean-slate, formal methods-based approach that enables semi-automated code synthesis from executable, formal specifications. In addition to generating code, such a synthesizer will produce a machine-checkable proof that the generated code satisfies the functional specification as well as appropriate security and safety policies.

Key HACMS technologies include interactive software synthesis systems, verification tools such as theorem provers and model checkers, and specification languages. Recent fundamental advances in the formal methods community, including advances in satisfiability (SAT) and satisfiability modulo theories (SMT) solvers, separation logic, theorem provers, model checkers, domain-specific languages, and code synthesis engines suggest that this approach is feasible.

References: Fbo.gov (1)