Using formal methods to enable more secure vehicles: DARPA's HACMS program

Networked embedded systems are ubiquitous in modern society. Examples include SCADA systems that manage physical infrastructure, medical devices such as pacemakers and insulin pumps, and vehicles such as airplanes and automobiles. Such devices are connected to networks for a variety of compelling reasons, including the ability to access diagnostic information conveniently, perform software updates, provide innovative features, and lower costs. Researchers and hackers have shown that these kinds of networked embedded systems are vulnerable to remote attacks and that such attacks can cause physical damage and can be hidden from monitors [1, 4].

DARPA launched the HACMS program to create technology to make such systems dramatically harder to attack successfully. Specifically, HACMS is pursuing a clean-slate, formal methods-based approach to the creation of high-assurance vehicles, where high assurance is defined to mean functionally correct and satisfying appropriate safety and security properties. Specific technologies include program synthesis, domain-specific languages, and theorem provers used as program development environments. Targeted software includes operating system components such as hypervisors, microkernels, file systems, and device drivers as well as control systems such as autopilots and adaptive cruise controls. Program researchers are leveraging existing high-assurance software including NICTA's seL4 microkernel and INRIA's CompCert compiler.

Although the HACMS project is less than halfway done, the program has already achieved some remarkable success. At program kick-off, a Red Team easily hijacked the baseline open-source quadcopter that HACMS researchers are using as a research platform. At the end of eighteen months, the Red Team was not able to hijack the newly-minted "SMACCMCopter" running high-assurance HACMS code, despite being given six weeks and full access to the source code of the copter. An expert in penetration testing called the SMACCMCopter "the most secure UAV on the planet."

In this talk, I will describe the HACMS program: its motivation, the underlying technologies, current results, and future directions.