Australian-developed secure microkernel takes to the skies

The University of NSW’s Trustworthy Systems research group has announced a collaboration with UAE-based Secure Systems Research Center (SSRC) to adopt its seL4 secure microkernel technology.

Scientia Professor Gernot Heiser.
UNSW

Last May, UNSW threw a funding lifeline to the Data61-developed technology, after the CSIRO division decided to dismantle the seL4 research team. That allowed the project to continue under its own foundation.

The UNSW-SSRC collaboration will focus on scaling the adoption of seL4 on devices like smartphones, drones, and wireless computing devices.

“This collaborative effort between UNSW and SSRC will aim to extend the formally verified seL4 microkernel to support tight integration of virtualised systems,” said UNSW Trustworthy Systems leader and John Lions Chair, Scientia Professor Gernot Heiser.

Starting as a research project by the former NICTA research centre of excellence in 2006, seL4 went through several years of formal mathematical verification, which means since 2009 it’s been described as “provably secure”.

Extending that formal verification is the focus of the UNSW-SSRC project. 

Heiser, who created seL4, said the two groups “will aim to extend the formally verified seL4 microkernel to support tight integration of virtualised systems”.

“The project will develop a device-sharing framework that allows virtual machines, as well as critical native functionality, to securely share input/output devices with low overhead, without interfering with each other, and without blowing out the size of the trusted computing base (TCB)”, UNSW said in a statement.

Heiser explained that this allows for the construction of systems with a minimal TCB, where critical functionality depends on as little code as possible. 

“Owing to the infeasibility of integrating complex software systems free of faults, it is important to keep the TCB minimal,” he said.

“This will enable the construction of cyber-secure edge systems with rich functionality.”
SSRC is a research centre at the Abu Dhabi government-funded Technology Innovation Institute.