to work on new code for them, each vehicle was subjected to
a red team software assault. Fisher reports that a penetration
and testing team led by Draper Laboratories was able to take
over all four vehicles. The team spent a total of one month on
each vehicle, which is “not a particularly significant level of
effort,” she adds.
Researchers are responsible for ripping out existing code
from these vehicles and replacing it with the program’s prod-
uct. The red team has completed early penetration exercises
on all four vehicles, she notes, and that step is repeated on
the code that others have produced at the end of each phase.
Over time, this should increase the difficulty for red teams to
break into each system.
One target platform is an ArduCopter, which Fisher
describes as a hobbyist unmanned aerial vehicle. The code in
this relatively small system is readily available, so developers
should be able to replace the code completely. Developers
already have built a domain-specific language called Ivory
that would generate flight control types of code. Half of the
original control system code has been replaced by the new
high-assurance version—enough that the helicopter can be
flown using this new code, she posits.
This effort is paired with a helicopter being produced by
Boeing that can be manned or unmanned, so the ArduCop-
ter’s architecture is being adjusted to match that of the Boeing
helicopter. This will allow for easy transfer of the software
developed for the ArduCopter to the Boeing craft. Fisher
points out that the Boeing helicopter effort does have specific
software replacement goals for each phase, unlike the other
The other two target platforms are ground vehicles. One is
the Black-I Robotics LandShark unmanned ground vehicle,
which is used mostly for border patrol and mine-clearing
exercises. Fisher notes that it is an open-source platform in
which researchers can access all of its source code.
The other platform is a U.S.-built automobile that offers
similar aspects to the LandShark. Fisher explains recent stud-
ies have shown that cars are extremely vulnerable to software
attacks. On average, a modern car has 3,200 embedded con-
trol units connected via a network accessible by a port under
the steering wheel. One study pointed out that an intruder
connecting to that network could reprogram all the comput-
ers on the car, which would allow the intruder to take over all
the vehicle’s functionality—brakes, steering and virtually all
control functions. This effect could be achieved by accessing
the network remotely through four different vectors, she says.
The program is taking three different approaches toward
achieving its goal. One approach entails program synthesis, in
which an engineer writes a high-level specification of a desired
behavior instead of just writing program code. A computer
converts this specification into the program code along with
proof that the code implements the specification correctly.
Another approach involves domain-specific languages that
are focused narrowly on specific tasks. This type of language
provides more support to the programmer, so engineers are
developing domain-specific languages for building high-assur-
ance vehicles and then using the results to generate the imple-
mentation and proof of correct behavior. A third approach
The Black-I Robotics LandShark unmanned ground vehicle is an
open-source platform being used to write assured software. It shares
some computer control features with modern automobiles, which are
becoming increasingly vulnerable to system takeover by outsiders.
uses automated theorem proving to prove the efficacy of the
code concurrent with it being written by developers.
The research is being conducted in two different domains,
Fisher relates. One is operating system code, but this is rela-
tively simple because most unmanned vehicle operating sys-
tems employ thousands of lines of code instead of millions
of lines for traditional desktop operating systems. The other
domain is control systems, which tie together sensors and con-
trol actuators. Both types of code have abstractions that allow
developers to write the desired behavior concisely, she notes.
“We’re really pushing the state of the art in terms of what we
know how to do,” Fisher says. “Because we’re being so aggres-
sive about that, we’ve given up trying to verify legacy code.
We’re focusing on producing new code and verifying that.”
Scaling the software development is a major challenge,
Fisher says. Producing high-assurance software entails meet-
ing a more stringent requirement than just writing code. One
way of achieving this is to increase the level of automation and
lower the level of expertise and time needed to generate it.
Fisher describes another challenge as compositionality.
Combining two high-assurance components into a high-
assurance composite—without redoing all the assurance
arguments—is difficult, she observes, but necessary to
achieve the program’s goal. “Compositionality is the only way
to build large systems,” she states.
George I. Seffers, email@example.com
Robert K. Ackerman, firstname.lastname@example.org
in this issue
Click to subscribe to this magazine
article text for page
< previous story
next story >
Share this page with a friend
Save to “My Stuff”
Subscribe to this magazine