LWN: Comments on "CSIRO's seL4 project shut down"

CSIRO's seL4 project shut down

wahern — Wed, 26 May 2021 03:37:52 +0000

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.

CSIRO's seL4 project shut down

sree — Tue, 25 May 2021 19:06:44 +0000

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

cypherpunks2 — Tue, 25 May 2021 01:33:34 +0000

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

sree — Mon, 24 May 2021 12:19:50 +0000

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.

Boeing 737-8 and 737-9 safety

bjartur — Sun, 23 May 2021 19:21:39 +0000

Can you provide a link and section number?

CSIRO's seL4 project shut down

mcon147 — Sat, 22 May 2021 23:59:16 +0000

Is anyone going to take over funding it?

CSIRO's seL4 project shut down

stumbles — Sat, 22 May 2021 19:42:52 +0000

There's an app for that.

CSIRO's seL4 project shut down

JanC_ — Sat, 22 May 2021 14:30:51 +0000

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

CSIRO's seL4 project shut down

scientes — Fri, 21 May 2021 23:31:35 +0000

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

CSIRO's seL4 project shut down

scientes — Fri, 21 May 2021 23:30:36 +0000

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.