Pierluigi Paganini
July 29, 2014
The National ICT Australia (NICTA) has completed the development of the first micro kernel mathematically proven seL4 to be bug free, its project will be released as open source tomorrow and could be deployed on drones to prevent hacking.
The formal-methods-based secure embedded L4 (seL4) microkernel was derived from the DARPA program High-Assurance Cyber Military Systems. The microkernel seL4‘s entire source code, including proofs and additional code used to build trustworthy, will be released under the GPL v2 license.
“General Dynamics C4 Systems and NICTA are pleased to announce the open sourcing of seL4, the world’s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. It is still the world’s most highly-assured OS.”
The NICTA is Australia’s Information Communications Technology (ICT) Research Centre of Excellence, it is an organization born to conduct, promote and sustain ICT research, it is composed by experts in maths and aviation working with primary companies Boeing and Rockwell Collins.
The micro kernel was the result of High-Assurance Cyber Military Systems program promoted by DARPA, HACMS has a four-year effort and an estimated cost of $60 million with the purpose of define an innovative and secure practice of coding to avoid that software could be affected by a “pervasive vulnerability”.
The program is described on the DARPA website with following statement:
“The High-Assurance Cyber Military Systems (HACMS) program seeks to create technology for the construction of systems that are functionally correct and satisfy appropriate safety and security properties,” explained, Kathleen Fisher, DARPA program manager. “Our vision for HACMS is to adopt a clean-slate, formal method-based approach to enable semi-automated code synthesis from executable, formal specifications.”
“In addition to generating code, HACMS seeks a synthesizer capable of producing a machine-checkable proof that the generated code satisfies functional specifications as well as security and safety policies. A key technical challenge is the development of techniques to ensure that such proofs are composable, allowing the construction of high-assurance systems out of high-assurance components.”
The formal-methods-based secure embedded L4 (seL4) microkernel aims to prevent the hacking of sophisticated devices without impacting performance.
As explained in the Wiki of OS DEV.org:
“A Microkernel tries to run most services – like networking, filesystem, etc. – as daemons / servers in user space. All that’s left to do for the kernel are basic services, like memory allocation (however, the actual memory manager is implemented in userspace), scheduling, and messaging (Inter Process Communication).
In theory, this concept makes the kernel more responsive (since much functionality resides in preemptible user-space threads and processes, removing the need for context-switching into the kernel proper), and improves the stability of the kernel by reducing the amount of code running in kernel space. “
In other words a similar approach allows to develop more stable and responsive software respect canonical monolithic kernels such as the Linux and Windows kernels.
The micro kernel belonging to the seL4 family could be used in wide casuistry, every critical component could be equipped with hacking proof software.
NICTA senior researcher Doctor June Andronick said the kernel should be considered by anyone building critical systems such as pacemakers and technology-rich cars.
“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,” Andronick said earlier this month.
“We provide a formal mathematical proof that this seL4 kernel is correct and guarantees the isolation between components.” said Doctor June Andronick.
Experts at NICTA provided a fascinating video-POC which demonstrates how a drone which running the platform could detect hacking attempts and adopt necessary countermeasures.
In the video, once the demo drone has detected the intrusion it fly away preventing that the hack is successfully conducted.
“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,” Andronick said.
Are we really close to the realization of a hack-proof machine?
Security Affairs – (seL4, DARPA)
