Provably secure microkernel will continue in its own foundation, but the team within Data61 is no more.
The team behind the seL4 is no longer under the umbrella of Australia’s Commonwealth Scientific and Industrial Research Organisation’s (CSIRO) Data61, with members being shifted from microkernels to supporting artificial intelligence. “[CSIRO’s Data61] dismantles Trustworthy Systems (TS), the team that shook the scientific world with the first correctness proof of an OS, #seL4. TS staff to reallocate to AI projects or sacked,” professor Gernot Heiser, chairman of the seL4 Foundation, said on Friday. “Claims by [Data61] of research excellence sound hollow. I challenge you to identify work in Data61 eclipsing the TS team and #seL4. Yet it’s easy to identify highly incremental work in Data61 that seems safe.” In 2009, the security of seL4 was mathematically proven. Heiser added that total disaster was avoided thanks to the seL4 Foundation being established last year.
