Industry News

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).

Bug-Free MicroKernel for Protecting Drones Goes Open Source

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

About the author

Lucian Ciolacu

Still the youngest Bitdefender News writer, Lucian is constantly after flash news in the security industry, especially when something is vulnerable or exploited. Besides digging for 'hacker' scoops and data leaks, he enjoys sports, such as football and tennis.
He has also combined an interest for social and political sciences, as a graduate of the Political Science Faculty, with a passion for guitar and computer games.