5 ms·

Apple Joins the SeL4 Foundation

94 points by fork-bomber 2y ago

mdhb 2y ago
Hopefully they won’t be the absolute waste of time as a company that they have been on the web standards working groups. Hard to trust them at this point in any collaborative sense.
542458 2y ago
For context, the Apple Secure Enclave chips run an NICTA L4-based microkernel, albeit not SeL4 specifically as far as I know (given the Secure Enclave launched in 2006 and NICTA released SeL4 in 2014). I wonder if this indicates plans to adopt SeL4? SeL4 is extremely cool technology. It has been formally proven to be bug-free against its specification, which massively simplifies the development of high-security high-reliability systems. I feel like there’s a lot more development to be seen in this space.
- daghamm 2y ago
  "against its specification" Which itself is not know to be bugfree. (And is 10x the size of the source code and in a language that is less readable than x64 assembler)
  - fooker 2y ago
    This is the price of contemporary formal methods. Hopefully things get better and more practically useful.
  - flawsofar 2y ago
    All code is either useless or unreadable
  - simplereally 2y ago
    Is the specification really 10x the size of the source code, or are you including the proof of the specification? Your claim about "x64 assembler" is dubious.
  - naasking 2y ago
    > Which itself is not know to be bugfree. Not totally correct, from: https://sel4.systems/Info/FAQ/proof.html https://sel4.systems/Info/FAQ/proof.html The binary code of the ARM and RISCV64 versions of the seL4 microkernel correctly implement the behaviour described in its abstract specification and nothing more. Furthermore, the specification and the seL4 binary satisfy the classic security properties called *integrity* and *confidentiality*. [...] Previously, in 2009, we had only proved functional correctness between the C code of the kernel and its specification. Now we have additionally shown binary correctness, that is, the compiler and linker need not be trusted, and we have shown that the specification indeed implies strong security properties as intended. So the specification has indeed been proven to be free of certain security bugs.
    - daghamm 2y ago
      It is always X meets Y under the assumption Z. But what if Y is incomlete or Z is invalid? Note that nowhere in that they claim X is secure.
      - naasking 2y ago
        "Secure" is ambiguous, so of course they wouldn't claim X, whatever that is, is "secure". For instance, a microkernel does not provide cryptographic confidentiality, but some readers include such properties under the umbrella of "secure", so using that term would be dumb. When talking about proofs you describe the specific properties proven in a way that leaves no ambiguity.
  - WhitneyLand 2y ago
    I’m not sure If you are really convinced that’s true or it’s supposed to be understood as an exaggeration. It is subjective, and I’ll grant it’s not the most intuitive thing to look at, but I don’t agree it’s worse than assembly. Besides the readability of the specification is not some priori limitation. Sel4 spec example definition set_endpoint :: "endpoint ⇒ data ⇒ state ⇒ state where set_endpoint ep data s ≡ s (ep := (IdleEP, data))
- snazz 2y ago
  What product from 2006 did it come with? My understanding was that the Secure Enclave came out with the iPhone 5s in 2013 (still before 2014, so your point stands, I’m just curious).
  - herpdyderp 2y ago
    Apple's own docs indicate the iPhone 5s was the first device with it as well: https://support.apple.com/guide/security/sec59b0b31ff/web https://support.apple.com/guide/security/sec59b0b31ff/web
- 2OEH8eoCRo0 2y ago
  Maybe I'm naive but why do these small single-purpose chips need kernels? Ease of development? Their use-cases sometimes seem trivial enough for a simple finite state machine.
  - surajrmal 2y ago
    It depends on how much code runs on it. After a certain scale you want better tolerance for failures by isolating those failures. Team structure can also play a role.
trollied 2y ago
If you're interested, the microkernel is open source: https://github.com/seL4/seL4 https://github.com/seL4/seL4
- repelsteeltje 2y ago
  More precisely: Generally, kernel-level code is licensed under GPLv2 and user-level code under the 2-clause BSD license.
- lunfard000 2y ago
  the project seems active but last (github) release was 3 years ago?
  - naasking 2y ago
    I'm not sure you should expect much development for a microkernel that has been proven to meet its specification and to be free of bugs. Microkernels are supposed to have a very small API, so there's not much development needed there unless it doesn't the specification or has other kinds of bugs, which is obviously not the case here.
    - lunfard000 2y ago
      But they keep accepting PR, shouldn't they tag from now and then so people know what is "stable"?
      - CuriousCosmic 2y ago
        By it's nature at this state (after the full proving effort is complete), any changes to the main/master branch are inherently "stable" and PRs are only accepted once they reach that state.
  - admax88qqq 2y ago
    This is the type of software that is "finished". I would expect the code to be pretty frozen.
fidotron 2y ago
Interesting if unsurprising this is shortly after the AArch64 verification was completed. And credit where it’s due, I know we love dumping on the national security apparatus, but the UK NCSC actually funded that work, which is a clear net win.
darksaints 2y ago
Any chance this could become the kernel for Darwin?
- microtonal 2y ago
  More likely future versions of the Secure Enclave (since the SE already uses L4).
- iforgotmysocks 2y ago
  macOS(and other OSes in Apple ecosystem like iOS) currently uses XNU kernel which is hybrid kernel Hybrid kernel combine both a monolithic kernel and micro kernel In macOS Mach is micro kernel and Darwin is monolithic kernel
deleted 2y ago
[deleted]
ytch 2y ago
A little bit unrelated, but reading through their member list: https://sel4.systems/Foundation/Membership/ https://sel4.systems/Foundation/Membership/ reminds me that Jobs explains why their company called "Apple Computer" is: "I worked at Atari, and it got us ahead of Atari in the phone book."[1]. Apple is the first one of all sel4 general member too. [1] https://www.businessinsider.com/apple-archive-name-apple-2011-12 https://www.businessinsider.com/apple-archive-name-apple-201...
- smugma 2y ago
  Amazon one-ups Apple in this regard.

94 points by fork-bomber 2y ago

mdhb 2y ago

Hopefully they won’t be the absolute waste of time as a company that they have been on the web standards working groups. Hard to trust them at this point in any collaborative sense.

542458 2y ago

For context, the Apple Secure Enclave chips run an NICTA L4-based microkernel, albeit not SeL4 specifically as far as I know (given the Secure Enclave launched in 2006 and NICTA released SeL4 in 2014). I wonder if this indicates plans to adopt SeL4? SeL4 is extremely cool technology. It has been formally proven to be bug-free against its specification, which massively simplifies the development of high-security high-reliability systems. I feel like there’s a lot more development to be seen in this space.

daghamm 2y ago
"against its specification" Which itself is not know to be bugfree. (And is 10x the size of the source code and in a language that is less readable than x64 assembler)
- fooker 2y ago
  This is the price of contemporary formal methods. Hopefully things get better and more practically useful.
- flawsofar 2y ago
  All code is either useless or unreadable
- simplereally 2y ago
  Is the specification really 10x the size of the source code, or are you including the proof of the specification? Your claim about "x64 assembler" is dubious.
- naasking 2y ago
  > Which itself is not know to be bugfree. Not totally correct, from: https://sel4.systems/Info/FAQ/proof.html https://sel4.systems/Info/FAQ/proof.html The binary code of the ARM and RISCV64 versions of the seL4 microkernel correctly implement the behaviour described in its abstract specification and nothing more. Furthermore, the specification and the seL4 binary satisfy the classic security properties called *integrity* and *confidentiality*. [...] Previously, in 2009, we had only proved functional correctness between the C code of the kernel and its specification. Now we have additionally shown binary correctness, that is, the compiler and linker need not be trusted, and we have shown that the specification indeed implies strong security properties as intended. So the specification has indeed been proven to be free of certain security bugs.
  - daghamm 2y ago
    It is always X meets Y under the assumption Z. But what if Y is incomlete or Z is invalid? Note that nowhere in that they claim X is secure.
    - naasking 2y ago
      "Secure" is ambiguous, so of course they wouldn't claim X, whatever that is, is "secure". For instance, a microkernel does not provide cryptographic confidentiality, but some readers include such properties under the umbrella of "secure", so using that term would be dumb. When talking about proofs you describe the specific properties proven in a way that leaves no ambiguity.
- WhitneyLand 2y ago
  I’m not sure If you are really convinced that’s true or it’s supposed to be understood as an exaggeration. It is subjective, and I’ll grant it’s not the most intuitive thing to look at, but I don’t agree it’s worse than assembly. Besides the readability of the specification is not some priori limitation. Sel4 spec example definition set_endpoint :: "endpoint ⇒ data ⇒ state ⇒ state where set_endpoint ep data s ≡ s (ep := (IdleEP, data))
snazz 2y ago
What product from 2006 did it come with? My understanding was that the Secure Enclave came out with the iPhone 5s in 2013 (still before 2014, so your point stands, I’m just curious).
- herpdyderp 2y ago
  Apple's own docs indicate the iPhone 5s was the first device with it as well: https://support.apple.com/guide/security/sec59b0b31ff/web https://support.apple.com/guide/security/sec59b0b31ff/web
2OEH8eoCRo0 2y ago
Maybe I'm naive but why do these small single-purpose chips need kernels? Ease of development? Their use-cases sometimes seem trivial enough for a simple finite state machine.
- surajrmal 2y ago
  It depends on how much code runs on it. After a certain scale you want better tolerance for failures by isolating those failures. Team structure can also play a role.

trollied 2y ago

If you're interested, the microkernel is open source: https://github.com/seL4/seL4 https://github.com/seL4/seL4

repelsteeltje 2y ago
More precisely: Generally, kernel-level code is licensed under GPLv2 and user-level code under the 2-clause BSD license.
lunfard000 2y ago
the project seems active but last (github) release was 3 years ago?
- naasking 2y ago
  I'm not sure you should expect much development for a microkernel that has been proven to meet its specification and to be free of bugs. Microkernels are supposed to have a very small API, so there's not much development needed there unless it doesn't the specification or has other kinds of bugs, which is obviously not the case here.
  - lunfard000 2y ago
    But they keep accepting PR, shouldn't they tag from now and then so people know what is "stable"?
    - CuriousCosmic 2y ago
      By it's nature at this state (after the full proving effort is complete), any changes to the main/master branch are inherently "stable" and PRs are only accepted once they reach that state.
- admax88qqq 2y ago
  This is the type of software that is "finished". I would expect the code to be pretty frozen.

fidotron 2y ago

Interesting if unsurprising this is shortly after the AArch64 verification was completed. And credit where it’s due, I know we love dumping on the national security apparatus, but the UK NCSC actually funded that work, which is a clear net win.

darksaints 2y ago

Any chance this could become the kernel for Darwin?

microtonal 2y ago
More likely future versions of the Secure Enclave (since the SE already uses L4).
iforgotmysocks 2y ago
macOS(and other OSes in Apple ecosystem like iOS) currently uses XNU kernel which is hybrid kernel Hybrid kernel combine both a monolithic kernel and micro kernel In macOS Mach is micro kernel and Darwin is monolithic kernel

deleted 2y ago

[deleted]

ytch 2y ago

A little bit unrelated, but reading through their member list: https://sel4.systems/Foundation/Membership/ https://sel4.systems/Foundation/Membership/ reminds me that Jobs explains why their company called "Apple Computer" is: "I worked at Atari, and it got us ahead of Atari in the phone book."[1]. Apple is the first one of all sel4 general member too. [1] https://www.businessinsider.com/apple-archive-name-apple-2011-12 https://www.businessinsider.com/apple-archive-name-apple-201...

smugma 2y ago
Amazon one-ups Apple in this regard.