Bug-Free MicroKernel for Protecting Drones Goes Open Source

The alleged mathematically proven bug-free microkernel for drone protection is going open source, according to The Register.

This piece of code, developed by the National ICT Australia (NICTA), was used to stop hackers from compromising unmanned drones. Development was also part of the High-Assurance Cyber Military Systems program patronized by the US Defense Advanced Research Projects Agency (DARPA).

“If your software runs the seL4 kernel, you have a guarantee that if a fault happens in one part of the system it cannot propagate to the rest of the system and in particular the critical parts,” said NICTA senior researcher June Andronick.

“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.”

The L4 microkernel is said to be very performant due to its use of formal method and will be more stable as it runs as much as code as possible in the user space. It will be released as open source under the GPL v2 license.

“The world’s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is going open source,” the announcement concluded.