CSIRO's seL4 project shut down [LWN.net]

In 2018, LWN covered a talk by Gernot Heiser about the seL4 project, which has developed an open-source operating system for safety-critical applications and gone to the trouble of proving its correctness. Much of that work has been done at CSIRO in Australia. Heiser has announced via Twitter that CSIRO's support for this project is being shut down, with the staff being redirected to artificial-intelligence projects. Hopefully the seL4 Foundation, established in 2020, will be able to carry on this interesting work.

to post comments

CSIRO's seL4 project shut down

Posted May 21, 2021 23:30 UTC (Fri) by scientes (guest, #83068) [Link] (9 responses)

This project has immense application in military projects, and has already been used by Boeing (NOT the 737 Max, LOL, which may crash and burn again as the FAA reapproval appeared incompetent when I read it) in military applications. Hence part of the "military is just about jobs, and competence irrelevant" thing.

CSIRO's seL4 project shut down

Posted May 21, 2021 23:31 UTC (Fri) by scientes (guest, #83068) [Link] (3 responses)

The FAA reapproval seemed to think that computers can read English.

CSIRO's seL4 project shut down

Posted May 22, 2021 14:30 UTC (Sat) by JanC_ (guest, #34940) [Link]

I suppose the 737-AI/2022 will add an AI module which you can upload the manual to…

CSIRO's seL4 project shut down

Posted May 22, 2021 19:42 UTC (Sat) by stumbles (guest, #8796) [Link]

There's an app for that.

Boeing 737-8 and 737-9 safety

Posted May 23, 2021 19:21 UTC (Sun) by bjartur (guest, #67801) [Link]

Can you provide a link and section number?

CSIRO's seL4 project shut down

Posted May 22, 2021 23:59 UTC (Sat) by mcon147 (subscriber, #56569) [Link] (4 responses)

Is anyone going to take over funding it?

CSIRO's seL4 project shut down

Posted May 24, 2021 12:19 UTC (Mon) by sree (guest, #152384) [Link] (2 responses)

There is the seL4 foundation:

https://sel4.systems/Foundation/

seL4 is also used in Apple devices as part of the secure enclave as OKL4, a spin-off of seL4.

CSIRO's seL4 project shut down

Posted May 25, 2021 1:33 UTC (Tue) by cypherpunks2 (guest, #152408) [Link] (1 responses)

OKL4 is not a spinoff of seL4. L4 is a family of microkernels, and OKL4 is a very popular proprietary microkernel sold by Open Kernel Labs. Although seL4 is an L4 microkernel, it is not derived from OKL4 in any way.

CSIRO's seL4 project shut down

Posted May 25, 2021 19:06 UTC (Tue) by sree (guest, #152384) [Link]

Sorry, I seem to have misunderstood the relationship.

L4 is a complicated family and this provided a nice retrospective:

https://sigops.org/s/conferences/sosp/2013/papers/p133-el...

CSIRO's seL4 project shut down

Posted May 26, 2021 3:37 UTC (Wed) by wahern (subscriber, #37304) [Link]

I investigated using seL4 for a project and IME the biggest impediment is the build system, CAmkES. Admittedly, the build is crucial to the overall security guarantees of a running system, and presumably well tailored to the needs of someone implementing a specific application, but it makes it nigh impossible to poke around and explore an seL4-based system. You can't acquire mindshare with such an impenetrable system, and without significant mindshare there aren't many avenues for funding.

If it were easier to bootstrap a system, run typical test applications (e.g. a single process fielding HTTP or USB requests), etc, then presumably far more people would get involved, bringing with them more opportunities for corporate investment. But I can see how getting and *staying* there would require more time and money than the project probably ever enjoyed; more than would be typical of a specialized OS. Hopefully there's a sponsor, corporate or otherwise, willing to make a large commitment because the potential is immense, both with what exists and what is being worked on (e.g. timing side-channel defense). The value is there, it's just locked up and out of sight.