Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

ACM Software System Award Given to seL4 Microkernel

awards.acm.org

Post reply on HN
Print view View original

21–30 of 66 posts

Re: ACM Software System Award Given to seL4 Microkernel

#21

Post by tptacek »

suavesito wrote: post #19
gjsman-1000 wrote: post #15

Earlier quoted context omitted.

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.

That's not really how any of this works. The formally verified kernel of the operating system gives you some assurance that your primitives are reliable (unlike on, say, Linux, where you're always a kernel reference tracking bug away from an LPE). But the "application" code you build on top of L4 doesn't "inherit" that formal verification; it's just code, with code bugs. If you formally verify your own code, it's verified, but otherwise you still own your own bugs.

For what it's worth, I'm not sure Apple publishes which variant of L4 it runs on, and there are many of them. The whole formal verification conversation here might be moot.

Re: ACM Software System Award Given to seL4 Microkernel

#22

Post by bee_rider »

amelius wrote: post #10
akshithg wrote: post #4

Earlier 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?

It looks like there’s a good bit of industry energy behind this stuff (defense contractors and intelligence agencies don’t want their side’s stuff broken into). So I don’t think this is one of those “Apple takes from the little guy and doesn’t contribute back” stories.

Re: ACM Software System Award Given to seL4 Microkernel

#23

Post by darksaints »

gjsman-1000 wrote: post #15
amelius wrote: post #10

Earlier 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.

True, but as with every other OS project out there, nobody is gonna use it without userland. The kernel itself is already pretty mature, but now the effort should be put into making a full fledged OS out of it.

Re: ACM Software System Award Given to seL4 Microkernel

#24

Post by bee_rider »

amelius wrote: post #9

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

It could be nice, although I’d expect a government to (justifiably) expect some “supply chain” type audits that lots of smaller open source projects wouldn’t want to go for.

Re: ACM Software System Award Given to seL4 Microkernel

#26

Post by pavlov »

amelius wrote: post #9

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

The EU supports open source projects, for example through the Horizon program which distributes 95 billion euros:

https://research.redhat.com/blog/article/look-to-the-horizon...

Re: ACM Software System Award Given to seL4 Microkernel

#27

Post by jacquesm »

gjsman-1000 wrote: post #15
amelius wrote: post #10

Earlier 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.

The last thing you want to do is to add niche features, those really should be handled in different processes. MM, IPC, interrupts, process creation/destruction/scheduling. That's about it.

Re: ACM Software System Award Given to seL4 Microkernel

#28

Post by monocasa »

gjsman-1000 wrote: post #15
amelius wrote: post #10

Earlier 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.

Apple doesn't use sel4 in the secure enclave, but instead another l4 variant that isn't formally verified.

And they've made a lot of pretty deep changes for example adding native support for Mach-O files.

Re: ACM Software System Award Given to seL4 Microkernel

#29

Post by sterlind »

jcrawfordor wrote: post #8
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 pl…

I thought commingling classification/user clearance levels on the same hardware fell out of favor a while ago, because of side channels (with speculative execution being the final nail in the coffin.)

Isn't seL4 more used for things like data diodes, cryptographic equipment and military hardware? Stuff that you need to keep from getting hacked or malfunctioning, but not time-shared with untrusted users.

Re: ACM Software System Award Given to seL4 Microkernel

#30

Post by Veserv »

gjsman-1000 wrote: post #15
amelius wrote: post #10

Earlier 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.

Apple is not using seL4 which is the proven one and which required sizable modifications to the original L4 variant seL4 was descended from. Apple is using a modified version of one of the many other L4 variants.
Post reply on HN