6 ms·

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

akshithg 3y ago
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-sec59b0b31ff/1/web/1 https://support.apple.com/guide/security/secure-enclave-sec5...
- amelius 3y ago
  How much did Apple contribute back to the project?
  - gjsman-1000 3y ago
    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.
    - suavesito 3y ago
      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 3y ago
        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 3y ago
        > 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.
        suavesito 3y ago
        Absolutely, the problem I'm referring to is if Apple changed the kernel and not only built an application on top of it. I don't know, but maybe Apple just built an application on top, which seems sensible.
    - darksaints 3y ago
      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.
    - jacquesm 3y ago
      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.
    - monocasa 3y ago
      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 3y ago
        What is a macho file?
        jonpalmisc 3y ago
        It’s the executable file format for macOS/iOS/*OS, analogous to ELF or PE. https://en.m.wikipedia.org/wiki/Mach-O https://en.m.wikipedia.org/wiki/Mach-O
        flangola7 3y ago
        Oh so an .exe
    - Veserv 3y ago
      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.
    - jnwatson 3y ago
      That’s what they say about every piece of software. There are always things to fix and add.
  - CalChris 3y ago
    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-operating-system/ https://www.zdnet.com/article/minix-intels-hidden-in-chip-op...
  - bee_rider 3y ago
    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.
exsf0859 3y ago
Google's Fuchsia OS uses a microkernel: https://fuchsia.dev/fuchsia-src/concepts/kernel https://fuchsia.dev/fuchsia-src/concepts/kernel
- junon 3y ago
  Microkernels by themselves are not special; SeL4 is because it's proven to be secure.
  - senko 3y ago
    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...
    - mycall 3y ago
      Take a look at Genode.
    - langfan 3y ago
      Why is it interesting?
      - snvzz 3y ago
        Not the parent, but seL4 has very high performance (they claim the best), and the IPC latency is bound by Worst Case Execution Time proof.
      - saithound 3y ago
        Some interesting aspects, in no particular order. Pure capability-based access control, where capabilities are communicable, but not forgeable "references with rights" to objects. While this is interesting, it's not really unique: other L4 kernels also have it, and Capsicum (but not POSIX capabilities) implements something like it on Unix. But even here, seL4 has some unique twists, such as the way IPC replies are handled, which allows policies that prevent "unsolicited" replies. A unique approach to memory management, where after boot-time, the kernel does no memory management, and even kernel memory is managed completely by user-level code. In fact, the kernel has no heap. Instead, when the user requests an operation that requires kernel memory (e.g. creating an address space, which requires memory for page tables) the user provides the memory explicitly to the kernel. This sets seL4 apart not just from monokernels, but from other L4 kernels as well. Support for passive servers: one of the most exciting recent features, these are server processes that run on scheduler time "donated" by the client. Among other things, this can be used to make sure that non-critical clients will not monopolize services needed by critical clients. IIRC seL4 is also the fastest L4 kernel for most use cases - and its worst-case execution time is bounded, at least on older CPUs which have published timing data.
mshockwave 3y ago
Airbus is also using either seL4 or some other microkernels in aerospace applications.
- Veserv 3y ago
  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 3y ago
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 3y ago
  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 3y ago
    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 3y ago
      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.
eep_social 3y ago
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 https://sel4.systems/About/seL4-whitepaper.pdf
the_panopticon 3y ago
KataOS and Sparrow https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html 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.

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-sec59b0b31ff/1/web/1 https://support.apple.com/guide/security/secure-enclave-sec5...

amelius 3y ago
How much did Apple contribute back to the project?
- gjsman-1000 3y ago
  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.
  - suavesito 3y ago
    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 3y ago
      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 3y ago
        > 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.
      - suavesito 3y ago
        Absolutely, the problem I'm referring to is if Apple changed the kernel and not only built an application on top of it. I don't know, but maybe Apple just built an application on top, which seems sensible.
  - darksaints 3y ago
    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.
  - jacquesm 3y ago
    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.
  - monocasa 3y ago
    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 3y ago
      What is a macho file?
      - jonpalmisc 3y ago
        It’s the executable file format for macOS/iOS/*OS, analogous to ELF or PE. https://en.m.wikipedia.org/wiki/Mach-O https://en.m.wikipedia.org/wiki/Mach-O
        flangola7 3y ago
        Oh so an .exe
  - Veserv 3y ago
    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.
  - jnwatson 3y ago
    That’s what they say about every piece of software. There are always things to fix and add.
- CalChris 3y ago
  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-operating-system/ https://www.zdnet.com/article/minix-intels-hidden-in-chip-op...
- bee_rider 3y ago
  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.

exsf0859 3y ago

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

junon 3y ago
Microkernels by themselves are not special; SeL4 is because it's proven to be secure.
- senko 3y ago
  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...
  - mycall 3y ago
    Take a look at Genode.
  - langfan 3y ago
    Why is it interesting?
    - snvzz 3y ago
      Not the parent, but seL4 has very high performance (they claim the best), and the IPC latency is bound by Worst Case Execution Time proof.
    - saithound 3y ago
      Some interesting aspects, in no particular order. Pure capability-based access control, where capabilities are communicable, but not forgeable "references with rights" to objects. While this is interesting, it's not really unique: other L4 kernels also have it, and Capsicum (but not POSIX capabilities) implements something like it on Unix. But even here, seL4 has some unique twists, such as the way IPC replies are handled, which allows policies that prevent "unsolicited" replies. A unique approach to memory management, where after boot-time, the kernel does no memory management, and even kernel memory is managed completely by user-level code. In fact, the kernel has no heap. Instead, when the user requests an operation that requires kernel memory (e.g. creating an address space, which requires memory for page tables) the user provides the memory explicitly to the kernel. This sets seL4 apart not just from monokernels, but from other L4 kernels as well. Support for passive servers: one of the most exciting recent features, these are server processes that run on scheduler time "donated" by the client. Among other things, this can be used to make sure that non-critical clients will not monopolize services needed by critical clients. IIRC seL4 is also the fastest L4 kernel for most use cases - and its worst-case execution time is bounded, at least on older CPUs which have published timing data.

mshockwave 3y ago

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

Veserv 3y ago
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 3y ago

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 3y ago
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 3y ago
  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 3y ago
    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.

eep_social 3y ago

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 https://sel4.systems/About/seL4-whitepaper.pdf

the_panopticon 3y ago

KataOS and Sparrow https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html 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.