ACM Software System Award Given to seL4 Microkernel

#1

Post by pjmlp » Sat, May 06, 2023, 3:25 PM UTC

ACM Software System Award Given to seL4 Microkernel
awards.acm.org

Re: ACM Software System Award Given to seL4 Microkernel

#2

Post by fh973 » Sat, May 06, 2023, 4:25 PM UTC

Congratulations, well deserved!

Also in memoriam Jochen Liedtke [0], who started the L4 kernel project and rekindled research in microkernels by showing that they don't have to be slow ('slow' as in Mach's long IPC latencies).

[0] https://en.m.wikipedia.org/wiki/Jochen_Liedtke

Re: ACM Software System Award Given to seL4 Microkernel

#3

Post by BoardsOfCanada » Sat, May 06, 2023, 5:02 PM UTC

Can someone tell me how much these microkernels are used and where?

Re: ACM Software System Award Given to seL4 Microkernel

#4

Post by akshithg » Sat, May 06, 2023, 5:09 PM UTC

BoardsOfCanada wrote: post #3

Can someone tell me how much these microkernels are used and where?

On that I’m aware of is in newer Apple devices with a Secure Enclave.

It is signed by apple and verified as part of the secure boot process.

> The Secure Enclave Processor runs an Apple-customized version of the L4 microkernel.

[1] https://support.apple.com/guide/security/secure-enclave-sec5...

Re: ACM Software System Award Given to seL4 Microkernel

#5

Post by beoberha » Sat, May 06, 2023, 5:16 PM UTC

Every year I’m reminded how diverse the recipients of this award are. You have a provably correct microkernel, DNS, Wireshark, and Jupyter Notebooks all being recognized as significant software systems.

Re: ACM Software System Award Given to seL4 Microkernel

#6

Post by exsf0859 » Sat, May 06, 2023, 5:17 PM UTC

BoardsOfCanada wrote: post #3

Can someone tell me how much these microkernels are used and where?

Google's Fuchsia OS uses a microkernel: https://fuchsia.dev/fuchsia-src/concepts/kernel

Re: ACM Software System Award Given to seL4 Microkernel

#7

Post by mshockwave » Sat, May 06, 2023, 5:33 PM UTC

BoardsOfCanada wrote: post #3

Can someone tell me how much these microkernels are used and where?

Airbus is also using either seL4 or some other microkernels in aerospace applications.

Re: ACM Software System Award Given to seL4 Microkernel

#8

Post by jcrawfordor » Sat, May 06, 2023, 5:34 PM UTC

BoardsOfCanada wrote: post #3

Can someone tell me how much these microkernels are used and where?

provably-correct microkernels like seL4 are popular for "cross-domain solutions" that simultaneously handle unclassified and classified information while ensuring separation. NSA requirements for such systems are strict and right now most of the options are commercial, like BAE XTS-400. More defense contractors are looking towards seL4 and the NSA seems to be encouraging it for the benefit of a shared, open-source platform across these specialized projects.

I believe seL4 is also used for the firmware on Qualcomm modems now, but it's a little hard to follow if they've switched from OKL4 which was a related project.

Re: ACM Software System Award Given to seL4 Microkernel

#9

Post by amelius » Sat, May 06, 2023, 5:35 PM UTC

Makes me wonder when we finally get proper government funding of FOSS projects.

Re: ACM Software System Award Given to seL4 Microkernel

#10

Post by amelius » Sat, May 06, 2023, 5:36 PM UTC

akshithg wrote: post #4

BoardsOfCanada wrote: post #3

Can someone tell me how much these microkernels are used and where?

On that I’m aware of is in newer Apple devices with a Secure Enclave. It is signed by apple and verified as part of the secure boot process. > The Secure Enclave Processor runs an Apple-customized version of the L4 microkernel. [1] https://support.apple.com/guide/security/secure-enclave-sec5...

How much did Apple contribute back to the project?