contributed articles

IN FEBRUARY 2017, a helicopter took off from a Boeing facility in Mesa, AZ, on a routine mission around nearby hills. It flew its course fully autonomously, and the safety pilot, required by the Federal Aviation Administration, did not touch any controls during the flight. This was not the first autonomous flight of the AH- 6, dubbed the Unmanned Little Bird (ULB); 3 it had been doing them for years. This time, however, the aircraft was subjected to mid-flight cyber attacks. The central mission computer was attacked by rogue camera software, as well as by a virus delivered through a compromised USB stick that had been inserted during maintenance. The attack compromised some subsystems but could not affect the safe operation of the aircraft.

One might think surviving such an attack is not a big deal, certainly that military aircraft would be robust against cyber attacks. In reality, a “red team” of professional penetration testers hired by the Defense Advanced Research Projects Agency (DARPA) under its High-Assurance Cyber Military Systems (HACMS) program had in 2013 compromised the baseline version of the ULB, designed for safety rather than security, to the point where it could have crashed it or diverted to any location of its choice. In this light, risking an in-flight attack with a human on board indicates that something had changed dramatically.

This article explains that change and the technology that enabled it. Specifically, it is about technology developed under the HACMS program, aiming to ensure the safe operation of critical real-world systems in a hostile cyber environment—multiple autonomous vehicles in this case. The technology is based on formally verified software, or software with machine-checked mathematical proofs it behaves according to its specification. While this article is not about the formal methods themselves, it explains how the verified artifacts can be used to secure practical systems. The most impressive outcome of HACMS is ar-guably that the technology could be retrofitted onto existing real-world systems, dramatically improving their cyber resilience, a process called “ seismic security retrofit” in analogy to, say, the seismic retrofit of buildings. Moreover, most of the re-engineering

Formally
Verified
Software in
the Real World

DOI: 10.1145/3230627

Verified software secures the Unmanned Little Bird autonomous helicopter against mid-flight cyber attacks.

BY GERWIN KLEIN, JUNE ANDRONICK, MATTHEW FERNANDEZ,
IHOR KUZ, TOBY MURRAY, AND GERNOT HEISER

key insights

˽ Formal proof based on micro-kernel-enforced software architecture can scale to real systems at low cost.

˽ Mixed assurance levels and security levels within one system are possible and desirable; not all code has to be assured to the highest level.

˽ High assurance can be retrofitted to suitable existing systems with only moderate redesign and refactoring.