Drone Brain Goes Open Source

Jul 29, 2014

DARPA and NICTA release the code for the ultra-secure microkernel system used in aerial drones.

The US Defense Advanced Research Projects Administration (DARPA) and Australia’s National Information and Communication Technology Agency (NICTA) have released the code for the ultra-secure embedded microkernel operating system that is used with flying drone devices. The seL4 (Secure L4) system is based on the L4 microkernel. The kernel is available for download at the seL4 system website.
L4 is a microkernel system used in mobile devices throughout the world. A microkernel design implements a modular architecture, minimizing the size of the kernel itself and maximizing the number of services that are able to run in userspace. The modular design and minimal use of code in kernel space means microkernel systems are (at least theoretically) more stable and more secure. Famous microkernels include Minix (which influenced the early development of Linux) and GNU Herd. The L3 and L4 systems were originally developed by German computer scientist Jochen Liedtke, who wanted to build a microkernel that was free of the performance issues associated with previous attempts. Researchers at NICTA joined with DARPA and aviation industry experts to develop seL4 from the L4 microkernel.
The seL4 system came from the need to create a microkernel that could be used in aerial drones and would be completely and verifiably free from the possibility of attack. The code for the kernel has undergone formal verification, a mathematical proof that the algorithms used in the system will perform as specified and won't be subject to intrusion.
Now that the highly stable and secure seL4 is in open source, other vendors will probably start to consider it for other mission critical embedded systems, such as medical implants and navigation devices.  

Related content

  • Linux News

    Updates on Technologies, Trends, and Tools

  • Minix 3

    Minix is often viewed as the spiritual predecessor of Linux, but these two Unix cousins could never agree on the kernel design. Now a new Minix with a BSD-style free license is poised to attract a new generation of users.

  • Exploring the Hurd

    The GNU project hasn't given up on the venerable Hurd project, and this long-running GNU Free OS project has recently received a burst of new energy with the release of a new Debian port.

  • Why Can't Computers Just Work All the Time?

    The feud between Minix inventor and operating system czar Andrew W. Tanenbaum and Linux Torvalds is legendary in the OS world. Before Linux there was Minix. Torvalds used to be a Minix user who set up his first Linux version in 1991 on Professor Tanenbaum’s operating system. Mr. Tanenbaum has now agreed to write a guest editorial for Linux Magazine. His opinion has not changed over the years: Linux (and Windows) are “unreliable.”

  • Qubes OS

    Most operating systems claim to be secure; however, most fail terribly. Newcomer Qubes OS tries a different approach, relying on a microkernel and pervasive virtualization.

comments powered by Disqus

Issue 180/2015

Buy this issue as a PDF

Digital Issue: Price $9.99
(incl. VAT)