How coders are creating software that's impossible to hack | Kathleen Fisher
HACMS is a program at DARPA that ran for four-and-a-half years
that was focused on using techniques
from what is called the ‘formal methods community’,
so techniques based on math more or less,
to produce software for vehicles that came with proofs
that the software had certain desirable properties;
that parts of it were functionally correct,
that there were no bugs and certain kinds of bugs in the software.
And the consequence of those proofs is
that the system is much harder to hack into.
So the formal methods community has been promising for, like,
50 years that they could produce
software that provably didn’t have certain kind of vulnerabilities.
And for more or less 50 years they
have failed to deliver on that promise.
Yes, they could produce proofs of correctness
for code but for ten lines of code or 100
lines of code—not enough code to make a difference
for any kind of practical purpose.
But recently there have been advances
in a bunch of different research areas that have
changed that equation,
and so now formal methods researchers can prove important properties
about code bases that are 10,000 or 100,000 lines of code.
And that’s still small potatoes compared to the size
of Microsoft Windows or the size
of Linux which are millions, hundreds of millions of lines of code.
But when you start to get to 10,000 or 100,000 lines
of code there are really interesting
software artifacts that fit in that size.
Things like compilers and microkernels,
and you can leverage those kinds of exquisite
artifacts to build much more complex software systems
where only a small part of the system
has to be verified to be functionally correct,
and then you can have lots of software running on top of it, that isn’t software correct,
that doesn’t have that same level of assurance associated with it
but that you can prove: it doesn’t matter what it does,
it’s not going to affect the operation
of the overall system.
So, for example,
HACMS researchers used the high-assurance code and put it on a Boeing
Unmanned Little Bird which is a
helicopter that can fly completely autonomously or it
can fly with two pilots.
And this helicopter has two computers on it:
one is the mission control computer that controls
things like ‘fly over there and take a picture’ or ‘fly
over there and take a picture’, and
communicate to the ground station or the operator
who’s telling the helicopter what to do.
It also has a flight control computer that controls things
like altitude hold and stability,
sort of the mechanics of flying the helicopter at any given time period.
So the researchers put seL4 microkernel,
which is a verified microkernel guaranteed to be functionally correct,
on the mission control computer,
and they used it to create different software partitions.
So one of those partitions was responsible for communicating with the ground station.
Another one of those partitions was responsible
for operating the camera that the helicopter had.
The researchers verified that the code
in the ‘communicate with the ground station’ was functionally correct and
isolated from the software in the ‘control the camera’ part.
So the camera part was all the legacy
software that had previously been on the helicopter
to control camera operation.
They allowed the red team to additionally put—the
red team is a group of people who
are charged with trying to take over control
of the helicopter against the wishes of the legitimate operator—
so they’re trying to
hack in, take over control, disrupt the
operation of the helicopter.
So in this setting,
the red team was allowed to have root access, so unfettered access
within the camera partition,
and was charged with: break out of this, take over control
of the rest of the helicopter,
disrupt the operation of the helicopter in any way, corrupt
the messages to the ground station—basically interfere
in any way you can with the legitimate
operation of this helicopter.
The red team had full access to the source code.
They understood all the design documents.
They knew as much about the system as you could reasonably expect to know.
And after six weeks they were not able to break out.
They were not able to disrupt the operation of the copter at all.
All they could do was they could fork-bomb themselves.
They could basically crash their own
process but the rest of the helicopter would then
notice that that process was crashed and restart it again,
restoring the operation of the camera.
So that’s an example
of where you could use the formal methods-based techniques to
create this kind of thin level at the bottom,
which was the seL4 microkernel, and then leverage
that to produce the full functionality ofthe helicopter.
The camera functionality might come and go as hackers break
in or don’t break in but you’re guaranteed
that the helicopter will be still able to communicate to the ground
station and fly appropriately.