Data61 dismantles research group behind seL4 secure OS

The CSIRO will dismantle the research group best known for developing the secure embedded L4 (seL4) microkernel as part of a restructure of its Data61 business unit.

The government-owned scientific research agency has told the trustworthy systems team that staff will be reallocated to other artificial intelligence (AI) project or let go altogether.

It comes less than two weeks after CSIRO revealed a $100 million investment in five science and technology growth areas, one of which is AI, over the next four years.

The government has also set aside $50 million in this year's budget for a national AI centre within Data61 to coordinate Australia’s AI expertise.

A spokesperson confirmed CSIRO will “no longer maintain” the group, but said there were plans to “strengthen” work around cyber security and emerging areas like trustworthy AI.

“The [group] is focused on the areas of formal methods for design, implementation and verification of software systems,” the spokesperson said.

“It is a mature area of technology that CSIRO has invested in over a number of years and is now well supported outside the organisation.”

The group developed seL4 at Data61’s predecessor, NICTA, to provide a secure, safe and reliable base for building trustworthy operating systems that handle sensitive information.

It was the first OS kernel to be mathematically proved secure, and has since been used in defence and aerospace settings.

TS founder and UNSW scientia professor Gernot Heiser described the break up as a “sad day for Australian computer science and especially cyber security research”.

“TS group brought you #seL4, the world’s first OS kernel with a machine-checked correctness proof,” he said on LinkedIn.

He added that it was still the “only capability-based verified OS, the only verified kernel for RISC-V [and] the only 64-bit OS kernel verified to the binary”.

Heiser said trustworthy systems research would continue at UNSW and through the global not-for-profit foundation set up last year.

But he warned that this would require “stay[ing] focussed on further strengthening the seL4 ecosystem” and bringing more members into the foundation.

“By setting up the seL4 foundation a year ago, we ensured that #seL4 will survive without the support from Data61 – a wise move in hindsight,” he added.

The dissolution of the trustworthy system group is part of a wider Data61 restructure that will potentially impact up to 70 staff in the short-term, namely “indefinite staff” and “term ends”.

CSIRO said, however, that the number would likely fall as people were redeployed throughout the organisations, with approximately 100 positions recently been created.

“Within two years, given the new positions, we expect headcount to be at similar levels to today,” the spokesperson said.

Having recently developed a new strategy, Data61 will direct investment to “strategic goals” around AI and “putting digital science and technology at the heart of Australia recovery”.