The Open Source Code That Defends Drones From Hackers
The "world's most highly assured" operating system is going open source.
The drone test. Image: YouTube screenshot/NICTA
Starting tomorrow, you'll be able to get your hands on a tool developed to counter cyberattacks against drones. The Register reports that researchers at Australian research centre NICTA will make their project, which was initially developed as part of a DARPA program, available open source beginning July 29. That means anyone will be able to look at the code, use it, manipulate it, and distribute it as they see fit.
In a video released earlier this month, NICTA senior researcher June Andronick demonstrated what could happen to a drone without adequate protections in place (the test starts about a minute in). The team had two commercial-style quadcopters—one loaded with the anti-hacking software, and one without. A selection of laptops on the ground formed a control station poised to mount an attack.
When the test gets underway and the ground station attempts to hack the drones, the one that has the system installed remains stable, flying without incident. In a pre-programmed response, it flashes its lights to alert its pilot to an attack and moves out of the way. The other plummets to the ground.
“What we are demonstrating here is that if one of the ground stations is malicious, and sends a command to the drone to stop the flight software, the commercially-available drone will accept the command, kill the software, and just drop from the sky,” Andronick explained.
This is where the newly developed software steps in. Its purpose is to detect incoming hacking attempts, inform the operator that it's being attacked, and then isolate different components of the drone, so that if one section is compromised the attack doesn't spread enough to control shut down the device completely.
The software is what's known as a secure embedded L4 (or seL4) microkernel. On its website, the seL4 team explains that a microkernel is the "minimal core of an operating system," i.e. the minimum you need to form out the very basics of an OS. “This is the piece of software that runs at the heart of the system, and controls accesses to everything,” Andronick said.
The researchers claim that their system is proven to be bug free, not owing to standard product testing, but because of mathematical law. “At NICTA, we provide a formal, mathematical proof that this kernel, seL4, is correct and guarantees isolation between components,” Andronick continued, and the site claims that seL4 is "the world's most highly-assured OS." The mathematical proof is being released along with the code, so it can be checked by everyone. In typical open-source fashion, this will hopefully lead to a more secure piece of software.
Once it's released, the code will likely be of most interest to security researchers and the wider open-source community. But it could also be picked up by those working on other technologies, such as autonomous vehicles, or even in the health sector.
In the same video, Professor Gernot Heiser, leader of Sofrware Systems Research Group at NICTA, referenced some previous examples of remote hacking, such as electronically taking control of cars, hacking pacemakers, or making ATMs spew out money. "This is not scare-mongering; these threats are real," he said. The idea is that developers could adapt the operating system to help secure those sorts of devices too.