Does This Drone Sport the World's Most Secure Operating System?Microkernel 'seL4' Aims to Lock Down Avionics, Cars and More
There's a custom drone sitting in a laboratory in Sydney. Unlike many drones, no hacker has been able to take control of its flight systems.
The quadcopter represents years of work by researchers with Australia's national research agency, Data 61. What makes the drone's critical software ultra secure is a relatively tiny operating system that has been optimized for maximum security benefit.
The operating system, called seL4, was a breakthrough for Australian researchers aiming to develop secure systems for use in everything from in-flight computers to automotive controls to infrastructure used by manufacturers and power plants.
seL4 is a "microkernel," or a stripped down version of a kernel. An operating system's kernel is essentially its heart: it has complete access to all software and hardware components such as memory. That's why gaining access to the kernel is especially sought after by hackers. Protecting this code from tampering is essential but difficult.
Microkernels have been developed for more than four decades. But in 2009, researchers in Australia had a major breakthrough: they mathematically proved that seL4 will only behave according to a strict specification, a concept referred to as formal verification.
A mathematical proof demonstrates that seL4 contains no software vulnerabilities at all. "The proof shows that the code implements the specification, and no more and no less," says Ihor Kuz of Data61's Trustworthy Systems division. "So if the specification doesn't have a buffer overflow, there's no buffer overflow." A buffer overflow is a common application programming mistake that in some cases can be exploited in order to run malicious code.
The seL4 microkernel maintains a strict separation between critical and non-critical functions. So if a hacker compromises an application running on top of seL4, access to other parts of the system are completely sealed off. There's simply no attack surface, and a hacker can't access or read or write to other parts of the system.
The microkernel's security, however, is dependent on some assumptions the researchers have made. For example, it could be undermined if the hardware platform it runs on contains deeply embedded spying code or has its own software vulnerabilities.
"We can't do anything against a hardware backdoor," says Gerwin Klein, research group leader for Data61's Trustworthy Systems. "Ultimately, if you can't trust what you're running on, you can't do much against that."
Also, Klein says the mathematical proof assumes that the behavior of the instruction set that the binary runs in is its actual behavior in the real world. "That's not something you can prove," he says. "It's something you write down."
Microkernel Gets a DARPA Shakedown
Kuz demonstrated an attack against the drone. Its mission computer - which is responsible for communicating with ground-based systems and instructing the flight controller - runs on seL4. If a hacker wanted to interfere with a flight, it's this computer that would be targeted.
Also running on top of seL4 is a virtualized instance of Linux, which controls the drone's camera. It's considered a non-critical system, and the camera communicates over Wi-Fi to send images. Kuz attacked the Linux instance, sending a fork bomb, which is a classic denial-of-service attack for Unix-based systems.
The camera crashes. But there's no way for Kuz to cross seL4's barrier to the mission computer, and the drone's flight systems are unaffected. "Whatever happens to the Linux stays in the Linux," Kuz says. "It's a little bit like Vegas."
Data61 has been working closely with the U.S. Defense Advanced Research Projects Agency to see how seL4 holds up in trials. Last year, a Boeing Little Bird helicopter was fitted with seL4 for an in-flight penetration test. The helicopter's critical systems couldn't be hacked.
The test was part of DARPA's High-Assurance Cyber Military Systems, a program that involves defense contractors such as Boeing and Rockwell Collins.
Data61's microkernel could be useful for a variety of industries where highly secure systems are needed. seL4 was released as open-source software about two years ago, so anyone can use it. Vehicle manufacturers would be prime candidates, especially after a flood of research has demonstrated that there are pervasive vulnerabilities in many of their software systems.
In mid-2015, for example, researchers Charlie Miller and Chris Valasek found that a vulnerability in a telematics unit could be exploited to gain control of a Jeep Cherokee's brakes. Fiat Chrysler recalled 1.4 million vehicles after the demonstration, which drew wide attention as it involved a journalist from Wired magazine driving the vehicle on a California highway.
On a related note, seL4 could be used in a vehicle's controller area network - a.k.a. CAN bus - which interfaces with a variety of sensors and systems. "Having an architecture and platform that provides isolation but integration would be of value," says Kevin Elphinstone, a principal researcher with Data61.
Products using seL4, however, may still be a few years away from reaching market. DARPA has given a number of grants to small enterprises, including a space company and a SCADA one, to use seL4. But because a microkernel is at the foundation of a product, it can take as long as five years to complete development, says Gernot Heiser, a computer science and engineering professor at the University of New South Wales.
There will likely still be a role for security software, even with systems using seL4. If untrustworthy software is used alongside seL4, there may still be a need for firewalls or intrusion detection systems, Klein says.
But not for seL4 itself. "The rootkit and virus scanners - they have a great business model, which is based on not solving the problem," Heiser says. "We hope to put them out of business."