Home → Magazine Archive → October 2018 (Vol. 61, No. 10) → Formally Verified Software in the Real World → Abstract

Formally Verified Software in the Real World

By Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby Murray, Gernot Heiser

Communications of the ACM, Vol. 61 No. 10, Pages 68-77

[article image]

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.

Back to Top

Key Insights


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.


No entries found