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

31–40 of 66 posts

Re: ACM Software System Award Given to seL4 Microkernel

#31

Post by Veserv »

sterlind wrote: post #29
jcrawfordor wrote: post #8

Earlier quoted context omitted.

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.

Nah, multilevel security fell out of favor because no large commercial vendor could do it. They retracted the requirements over a decade ago because it prevented Microsoft and IBM from bidding on government contracts to “secure” their infrastructure.

Re: ACM Software System Award Given to seL4 Microkernel

#32

Post by bjoli »

bee_rider wrote: post #25

Is there a seL4 implementation targeted at, like, dinking around on some desktop, or is this stuff mostly interesting to embedded-ish folks?

Maybe an ARM desktop once multi core is implemented and verified. Verifying the whole thing for x86 seems scary. It is a kind of undertaking that gives normal people a glimpse of how ADHD is. It is a huge task and I would not know how to structure it, where to start and how to predict and plan all the intermediate steps.

Re: ACM Software System Award Given to seL4 Microkernel

#33

Post by Veserv »

mshockwave wrote: post #7
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.

As far as I am aware seL4 is not used in any DO-178 Level A systems. As far as I am aware Airbus is using Integrity-178 microkernel which is the industry standard in commercial aerospace and is used in almost every commercial airliner and military aircraft.

Re: ACM Software System Award Given to seL4 Microkernel

#34

Post by monocasa »

tptacek wrote: post #21
suavesito wrote: post #19

Earlier quoted context omitted.

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 ver…

> I'm not sure Apple publishes which variant of L4 it runs on

The SEPOS kernel is an apparently derived from a fork of L4-embedded they used in Darbat (a fork of XNU to run on top of L4). Not formally verified unless Apple internally has done so.

Re: ACM Software System Award Given to seL4 Microkernel

#35

Post by jnwatson »

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.

That’s what they say about every piece of software. There are always things to fix and add.

Re: ACM Software System Award Given to seL4 Microkernel

#36

Post by junon »

exsf0859 wrote: post #6
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

Microkernels by themselves are not special; SeL4 is because it's proven to be secure.

Re: ACM Software System Award Given to seL4 Microkernel

#37

Post by ratmice »

bee_rider wrote: post #25

Is there a seL4 implementation targeted at, like, dinking around on some desktop, or is this stuff mostly interesting to embedded-ish folks?

The only thing I know of that provides a desktop is genode, which can run on top of seL4 (but also quite a few other kernels). Given that it'll be more like dinking around with genode than seL4 proper, exactly because of this multi kernel abstraction layer...

Re: ACM Software System Award Given to seL4 Microkernel

#38

Post by flangola7 »

monocasa wrote: post #28
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.

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.

What is a macho file?

Re: ACM Software System Award Given to seL4 Microkernel

#39

Post by senko »

junon wrote: post #36
exsf0859 wrote: post #6

Earlier quoted context omitted.

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

Microkernels by themselves are not special; SeL4 is because it's proven to be secure.

SeL4 is a very interesting kernel even without taking the proof into account (eg in platforms/builds that the proof doesn't cover).

I wish someone would build a beyond-posix desktop OS on top of it...

Post reply on HN