[HN Gopher] ACM Software System Award Given to seL4 Microkernel
___________________________________________________________________
ACM Software System Award Given to seL4 Microkernel
Author : pjmlp
Score : 174 points
Date : 2023-05-06 15:25 UTC (7 hours ago)
(HTM) web link (awards.acm.org)
(TXT) w3m dump (awards.acm.org)
| tunnuz wrote:
| Congrats!
| fh973 wrote:
| 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
| pfdietz wrote:
| It's such a shame he died so young.
| beoberha wrote:
| 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.
| CalChris wrote:
| Yes. The Turing Award by comparison seems to have become a
| lifetime achievement award.
| suavesito wrote:
| And also GCC.
| glhaynes wrote:
| Software's pretty cool.
| bee_rider wrote:
| Is there a seL4 implementation targeted at, like, dinking around
| on some desktop, or is this stuff mostly interesting to embedded-
| ish folks?
| bjoli wrote:
| 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.
| ratmice wrote:
| 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...
| BoardsOfCanada wrote:
| Can someone tell me how much these microkernels are used and
| where?
| eep_social wrote:
| 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)
|
| [1] https://sel4.systems/About/seL4-whitepaper.pdf
| exsf0859 wrote:
| Google's Fuchsia OS uses a microkernel:
| https://fuchsia.dev/fuchsia-src/concepts/kernel
| junon wrote:
| Microkernels by themselves are not special; SeL4 is because
| it's proven to be secure.
| senko wrote:
| 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...
| kjs3 wrote:
| It's proven correct against specification. That's not the
| same thing as 'secure' (although it helps).
| the_panopticon wrote:
| 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.
| mshockwave wrote:
| Airbus is also using either seL4 or some other microkernels in
| aerospace applications.
| Veserv wrote:
| 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.
| jcrawfordor wrote:
| 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.
| sterlind wrote:
| 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.
| Veserv wrote:
| 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.
| kjs3 wrote:
| Well, Microsoft made some half-assed runs at Orange Book
| compliance (e.g. Windows NT without floppies/CDs...or
| networking), but Trusted AIX was a real thing with real
| users. Having been involved in a couple of MLS Unix
| implementations, IMO it didn't fall out of favour because
| no vendor could do it, it fell out of favour because no
| one could effectively run it in production. The admin
| overhead of a 'real' TCSEC validate system is formidable,
| and at some point someone decided 'useable with admins
| with 6 months of training (e.g. privates and corporals)'
| was more important than 'checks all the boxes', and the
| boxes that needed to be checked changed.
| akshithg wrote:
| 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...
| amelius wrote:
| How much did Apple contribute back to the project?
| gjsman-1000 wrote:
| 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.
| jnwatson wrote:
| That's what they say about every piece of software. There
| are always things to fix and add.
| jacquesm wrote:
| 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.
| suavesito wrote:
| 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.
| tptacek wrote:
| 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.
| monocasa wrote:
| > 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.
| monocasa wrote:
| 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.
| flangola7 wrote:
| What is a macho file?
| jonpalmisc wrote:
| It's the executable file format for macOS/iOS/*OS,
| analogous to ELF or PE.
|
| https://en.m.wikipedia.org/wiki/Mach-O
| Veserv wrote:
| 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.
| darksaints wrote:
| 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.
| CalChris wrote:
| 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...
| bee_rider wrote:
| 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.
| LanternLight83 wrote:
| I would love to see Qubes rebuilt on this
| snvzz wrote:
| Makatea[0] is trying to do something like that.
|
| 0. https://trustworthy.systems/projects/TS/makatea
| amelius wrote:
| Makes me wonder when we finally get proper government funding of
| FOSS projects.
| bee_rider wrote:
| 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.
| pavlov wrote:
| 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...
| fnordpiglet wrote:
| 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.
| endgame wrote:
| A lot of the seL4 work was actually funded by several nations'
| taxpayers, and developed by the late Trustworthy Systems group
| at Data61 (formerly NICTA). Sadly, they were disbanded a few
| years back and had to rush to set up a standalone seL4
| Foundation: https://microkerneldude.org/2020/04/07/the-
| sel4-foundation-w...
|
| > seL4 is the result of big investments. Firstly by the
| Australian tax payers, who (through NICTA) funded its creation,
| and (through NICTA and then CSIRO's Data61) continued
| supporting it. Over the past 6 years, US taxpayers (mostly
| through DARPA, but also other parts of the DoD as well as DHS)
| invested a lot in completing and extending the verification
| story, as well as deploying on real-world systems. And most
| recently, HENSOLDT Cyber funded verification of the RISC-V port
| of the kernel.
| carterschonwald wrote:
| Congrats to all the folks on the sel4 project
___________________________________________________________________
(page generated 2023-05-06 23:00 UTC)