NICTA has created a video that demonstrates how its seL4 microkernel, the “world’s most highly assured OS”, can be used to operate drones.
In June, NICTA announced the seL4 microkernel will be made open source on 29 July. The project also involves US-based company General Dynamics C4 Systems, and is targeted at smartphones, military systems, medical devices, and unmanned aerial vehicles or drones.
SeL4 is the most advanced of the L4 microkernels – a small, third generation microkernel with about 8700 lines of C code.
A kernel is the software part of an operating system that runs in the privilege mode of a microprocessor. A microkernel is like a compact kernel that performs only minimal functions such as inter-process communication (IPC) with core functions such as file systems removed from the microkernel to run in user mode.
Not having all functions run in privilege mode means that if one process breaks down, the other can still run efficiently.
seL4 has full ‘functional correctness proof’, so the implementation (written in C) adheres to its specification. The binary code that executes on the hardware is a correct translation of the C code, meaning that the compiler does not have to be trusted and extends the functional correctness property to the binary.
According to NICTA, the operating system is bug free and enforces integrity and confidentiality.
Functional programming language Haskell was used to develop a high-performance C-based implementation of seL4 for ARM processors.
In the video, the NICTA team demonstrated how the seL4 can detect and deter cyber-attacks against an aerial drone. The system is able isolate different flight controls or components, so if one is compromised the attack does not propagate to the other controls.
“We provide a formal mathematical proof that seL4 is correct and guarantees isolation between components,” said Dr June Andronick, senior researcher, NICTA.
“If one of the ground station [has a] malicious [attack] and sends a command to the drone to stop the flight software, a commercially available drone will accept the command, kill the flight control software, and it will just drop from the sky and crash on the ground.”
Professor Gernot Heiser, software systems research group leader at NICTA, pointed out some of the sophisticated attacks that the seL4 is designed to pick up and deter:
“This is not scaremongering, these threats are real. Cars have been demonstrated to be remotely attackable where someone from another car driving on a highway was able to engage breaks or airbags.
“We have seen people remotely from thousands of metres distance controlling a heart pacemaker implanted in a person.
“And we’ve seen attacks where people remotely got ATMs to spit out dollar notes.”
Check out the video here:
Follow Rebecca Merrett on Twitter: @Rebecca_Merrett