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.