DARPA’s hack proof code protects military systems from hackers

An autonomous helicopter gunship is flying over a military base in Arizona. Suddenly, officers on the ground lose radio contact and learn that hackers have taken control of its on-board computer, and then comes the big question - could they fly the helicopter? Fire the weapons? Crash it into the ground?

This scenario has already happened – well, almost - when the US Defense Advanced Research Projects Agency (DARPA) used this scenario in a drill to test the cybersecurity of an unmanned Boeing Little Bird helicopter.

Despite the hackers being given unfettered access to the computer, and then trying their hardest to disable the helicopter – even crashing the computer – they could not disrupt critical systems. For DARPA, which is aiming to develop an “unhackable” drone by 2018 as part of its High Assurance Cyber Military Systems (HACMS) programme, the drill was a success. This isn’t just about the military, though. The software that kept the helicopter’s computer secure was at the heart of its operating system, and it could be just what the world needs to make everything from pacemakers to insulin pumps and power stations to cars immune to hacking.

DARPA's Explainer Video

“My hope is that in 10 years’ time, anything that is security critical is running on our system or some other one built on the principles we’ve established,” says Gernot Heiser from the newly formed Australian National Research Agency, Data61. One of the Australian agencies predecessors developed the crucial component of the “unhackable” operating system – its kernel.

The kernel is the central core of any computer’s operating system. If hackers gain access to it then they can perform actions that are meant to be forbidden – like turning a mobile phone into a signal jammer, for example. Last year, Heiser’s team proved mathematically that their kernel is unhackable. Known as seL4, the kernel has a few highly secure properties - it can only do what it is designed to do, its code can’t be changed without permission and its memory and data transfers can’t be read without permission.

An earlier version of it, called OKL4, is now in millions of smartphones. Heiser says that two features underpin seL4’s security, one of which is a new way of isolating data inside the kernel. But the key development was making the code capable of being checked mathematically. Other kernels might have these properties too, but it is impossible to know for sure without mathematical proof, says Heiser. In July, two hackers pulled a prank by remotely accessing the computer of a Chrysler Jeep, making it stop suddenly on a highway and then crash into a ditch. As a result, Chrysler was forced to recall over 1.4 million vehicles.

Could seL4 prevent such episodes in the future? Heiser says you can’t stop hackers getting access to things like a car’s entertainment system, if it communicates using Wi-Fi and hackers often use a non-critical system as a springboard themselves into critical areas like steering – as happened with the Jeep prank. But the seL4 kernel can keep systems separate, Heiser says.

“There are now efforts afoot to roll this out to cars to protect them. Car hackers may access the entertainment system and use it as a springboard to a critical area like steering."

That’s what the helicopter drill demonstrated. On the assumption that not every system can be made secure, the organisers made one computer run two operating systems simultaneously, one of which included the seL4 kernel. They then gave hackers full access to the other system.

“In the past they had no problem owning that thing. But we can now stop them from breaking in,” says Heiser.

The same principles will apply in preventing hackers from gaining access to critical systems in power grids or medical devices, says Kathleen Fisher at Tufts University in Medford, who is also the HACMS programme manager. It is a big deal for cybersecurity, says Iman Shames from the University of Melbourne in Australia. But he says there are always ways to attack hardware, even if the software is impregnable. Hackers might be able to spoof a device’s sensors or jam incoming communications or other signals, which could be just as devastating so where one solution appears another problem springs up in its place.

And so the battle for hack proof systems - if there will ever be truly such a thing, continues but what isn't in question is the important step that's been taken by developing seL4.