Breach Preparedness , Data Breach , Risk Management
Microkernel 'seL4' Aims to Lock Down Avionics, Cars, SCADA 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.
See Also: From Authentication to Advanced Attack Vectors: Top Trends in Cybercrime in Q1 2016
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 SCADA infrastructure.
The seL4 microkernel is a stripped down, slim version of the core code of an operating system. Kernels are especially security-sensitive because the code they run is allowed access to all other parts of a computer's hardware and software.
Mathematically Proven
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."
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."
Australia's Data61 research agency has developed a drone that uses an ultra-secure operating system called seL4 that is free of software vulnerabilities, making it resistant to hacking attempts.
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.
Commercial Use?
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."