6 ms·

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 Encl

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.

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.