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 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 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 of
the 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.