Congrats to all the folks on the sel4 project
ACM Software System Award Given to seL4 Microkernel
11–20 of 66 posts
Re: ACM Software System Award Given to seL4 Microkernel
#12Congrats!
Re: ACM Software System Award Given to seL4 Microkernel
#13Can someone tell me how much these microkernels are used and where?
I think this quotation from page 5 of the seL4 whitepaper [1] about a different micro kernel might help:
> our L4- embedded kernel from the mid-Noughties runs on the secure enclave of all recent iOS devices (iPhones etc)
Re: ACM Software System Award Given to seL4 Microkernel
#14Can someone tell me how much these microkernels are used and where?
KataOS and Sparrow https://opensource.googleblog.com/2022/10/announcing-kataos-... represent another use of seL4. This time with Rust as services code outside of the provably-correct seL4 c code.
Re: ACM Software System Award Given to seL4 Microkernel
#15Earlier quoted context omitted.
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?
Does it matter? A microkernel isn’t a huge scope, and once it is proven mathematically correct, there’s not a ton left to do; other than maybe adding very niche features or doing touch-ups here and there.
Re: ACM Software System Award Given to seL4 Microkernel
#16Every 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.
Yes. The Turing Award by comparison seems to have become a lifetime achievement award.
Re: ACM Software System Award Given to seL4 Microkernel
#17Every 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.
And also GCC.
Re: ACM Software System Award Given to seL4 Microkernel
#18Makes me wonder when we finally get proper government funding of FOSS projects.
That’s an interesting idea, there should be a technology incubating grant program that supports FOSS, which the government is fundamentally dependent on and fosters domestic and global growth at least as much as NSF grant funding does.
Re: ACM Software System Award Given to seL4 Microkernel
#19Earlier quoted context omitted.
How much did Apple contribute back to the project?
Does it matter? A microkernel isn’t a huge scope, and once it is proven mathematically correct, there’s not a ton left to do; other than maybe adding very niche features or doing touch-ups here and there.
Except that making changes can actually invalidate the proof that were made. At least it matters in the sense that Apple should have made an arrangement so the things added didn't invalidate the correctness.
Re: ACM Software System Award Given to seL4 Microkernel
#20Earlier quoted context omitted.
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?
I think that is a relevant question because in related news, Intel didn't acknowledge MINIX.
https://www.zdnet.com/article/minix-intels-hidden-in-chip-op...