7 ms·

SeL4 security proofs now complete on AArch64

201 points by snvzz 24d ago

kvuj 24d ago
What operating systems use SeL4? I know of the following: - GenodeOS - LionsOS - A chinese car maker was using it as a hypervisor in their cars, IIRC - What else? Are there any private deployments you guys are aware of?
- angry_octet 24d ago
  The Secure Enclave on iOS devices runs sepOS, and earlier fork of the UNSW/NICTA L4 nano kernel work. Obviously Apple has huge resources to verify their own kernel on their own hardware, but seL4 is likely much more secure. With Apple's appetite for architectural security improvements I think they will eventually move to an seL4 derivative with special hardware security add-ons. There are a number of talks at the upcoming seL4 summit, but see 2025, e.g. Kry10 KOS. https://sel4.systems/Summit/2025/program.html https://sel4.systems/Summit/2025/program.html
StilesCrisis 24d ago
Coming soon: a side-channel timing attack which completely invalidates this result
- msdz 24d ago
  Are timing (over network) attacks, physical access, etc. typically excluded from research like this for being “out of scope”, so to speak? I’m not familiar.
  - StilesCrisis 24d ago
    Mathematical proofs tend to assume that they are built on perfect foundations (you have to stop the proof somewhere!). Unfortunately, proving that the software is correct just means you need to find a flaw in a deeper layer.
  - monster_truck 24d ago
    They aren't out of scope as much as they are irrelevant. It has been a best practice to ensure that the things you would be attempting to attack the timing of do not let you do this for a very long time. We are so far down this road that we do things like generate thousands of values and throw most of them away to mitigate the laziest attempts at what would be considered in scope.
    - less_less 24d ago
      It's still relevant (and probably also rather difficult) to prove that seL4 itself conforms to those best practices.
- avadodin 24d ago
  That's a bit unfair. Any side–channel attack that invalidates seL4 security guarantees —assuming the proofs are valid— also invalidates any other imaginable OS'. We're in the philosophical territory of tasking infallible beings with stopping their own flawless creations.
- fosslinux 24d ago
  Although, there is ongoing research regarding time protection (https://trustworthy.systems/projects/timeprotection/ https://trustworthy.systems/projects/timeprotection/) which prevents exactly timing channels. Including proofs of seL4 providing time protection.
  - brohee 24d ago
    Security-partition switches that carefully reset all shared micro-architectural state, while making switch times completely deterministic, and in particular, independent of previous execution history. I'm afraid it means clearing all caches at each context switch. The performance penalty is really high.
    - spectra2 23d ago
      Not all caches are cleared. There are some clever techniques to partition off-core caches (i.e. the L3) as part of the isolation boundaries enforced by the kernel. What I think is particularly exciting is that a new RISCV64 instruction to clear microarchitectural state is in the process of being standardised! So I'm hopeful that, while it should not be ignored, the performance penalty will not be too high.
- torginus 24d ago
  I don't think a side channel attack against L4 would be particularly useful - the kernel's tiny, and doesn't really do much other than scheduling, IPC and capabilities. Anything you might want to learn lives in other processes. That said, the big caveat of the whole thing, is that by pushing stuff traditionally considered to be sensitive to user space doesn't solve security or stability, it makes it other people's problem. There's no reason you couldn't do a side channel (or a different kind of) attack against a process that hosts the filesystem.
  - spectra2 23d ago
    I think the danger of a side-channel attack against seL4 is more dangerous than you believe. The security proofs ensure that threads should not be able to read data they do not have permission to, or write to places they do not have permission to etc., through any part of the kernel's interface, which includes the mechanisms for inter-process communication. That means a side-channel, or some gap in this proof, would allow learning about what lives in processes! While seL4 is definitely not a silver bullet for building a secure and stable system, I would argue that its security guarantees mitigate the risks. seL4's security proofs guarantee that the kernel obeys the information flow policy of your system, derived from the runtime distribution of permissions ("capabilities") in your system. If the interface to your filesystem, for example, is through the judicious granting of capabilities, then you can rest assured there is no side-channel.
    - torginus 23d ago
      > That means a side-channel, or some gap in this proof, would allow learning about what lives in processes! This is true, but outside of the scope of the kernel (which is a theme with microkernel). Side channels are unfortunately a side effect of how hardware works. This is kind of a theme with microkernels, they are not a silver bullet, I agree. The Linux kernel handles a lot of things L4 doesn't like memory management, drivers, file systems that L4 doesn't. So a filesystem bug would not be a kernel bug in L4 but would have just as serious implications as on Linux. So while what they're claiming about security imo is true, they're claiming much less here than people here assume. > If the interface to your filesystem, for example, is through the judicious granting of capabilities, then you can rest assured there is no side-channel. How do you mean? Caps are a software contract, and side channels, like manipulating CPU cache with speculative execution is lower level than that. I don't see how that would mitigate issues like that.
- brohee 24d ago
  The assumptions the proof makes are pretty clearly listed: https://sel4.systems/Verification/assumptions.html https://sel4.systems/Verification/assumptions.html The one covering side channels is pretty honest: Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels. So the proof won't be invalidated at it does not cover that particular threat. Now the question is how useful the is a proof not covering side channels? I'd say pretty useful and it doesn't mean they don't have counter measures for to counter their exploitation, nor that they are not effective, just that a proof of efficiency is out of reach for now.
  - brohee 24d ago
    To add to that, the only way I see proof of absence of timing channels is by proving both the software and the hardware design side by side, and then the proof would hold only for a specific core. Something that would look both at the code manipulating secrets and at the Verilog for the specific core/memory chips. I've not been working in that space in a long while but AFAIK such a thing is nowhere near ready. I suspect it will be a lot easier if the hardware design is optimised for provability, which won't be good at all for performance. But there are plenty of contexts where security matters a lot more than performance (SMC, BMC, RoT and co at the very least). And then you'd need assurance that the Verilog is faithfully transcribed in the silicon, which is a can of worms in itself.
    - simiones 24d ago
      I don't think it needs to be so dramatic. You could have a proof that the algorithms don't contain data-dependent logic, and perhaps ensure that no data-dependent instructions are generated; and that all branches have the same number of instrution-cycles (adding padding if not). You'd then simply rely on the architecture-specific instruction timing differences to be respected by the compiler. Would something like this guarantee that no side-channels are possible on any architecture? Perhaps not, but it would still get you most of the way there.
- IsTom 24d ago
  There's another can of worms that are rowhammer-esque attacks.
- dathinab 24d ago
  you are missing the point just because something isn't perfect and handles everything you can come up with doesn't mean it isn't still very very useful nothing in nature is truly perfect and down-talking grate but not perfect things will just make us stuck in a pretty shitty world which never improves because no improvement by itself "perfectly/fully" solves whatever problem set you are looking at
- CalChris 24d ago
  Side channel timing attacks are micro architectural. The SeL4 security proofs are architectural.
  - warkdarrior 23d ago
    Is cache hierarchy considered part of the microarchitecture?
- saidnooneever 23d ago
  the proofs prove certain things they do not prove a system is infallable or actually secure they rule out certain things in certain parts of the code.
i_am_a_peasant 24d ago
Read the fine print, "non-MCS (mixed criticality systems), unicore"
avadodin 24d ago
The embedded and military markets may keep funding them for the foreseeable future but they need a native seL4/Linux if they want to honestly claim they are improving systems' security with their capability model. Secure–boot virtualization platforms are dime a dozen nowadays.
- jdub 24d ago
  "native seL4/Linux"? seL4 can already host Linux VMs, and there are various methods of running Linux code / binaries without hardware virtualisation.
  - avadodin 24d ago
    A real OS user-land kernel handling real workloads within the capability model. A Linux VM isn't it.
  - adastra22 24d ago
    And what would be the point of that?
    - jdub 23d ago
      It's frequently done in research and industry when there's a component that has strict timing and separation requirements, and a bunch of supporting software that doesn't. Like an autonomous helicopter. Flight control? Very important. A bunch of hardware drivers and services for imaging, navigation, comms... not so much, and not worth the (long term ongoing) effort of replatforming.
      - adastra22 23d ago
        I don't understand though. If it's all running on the Linux VM, then you haven't inherited any of the secL4 benefits.
        spectra2 23d ago
grommet_kit 23d ago
[dead]

201 points by snvzz 24d ago

kvuj 24d ago

What operating systems use SeL4? I know of the following: - GenodeOS - LionsOS - A chinese car maker was using it as a hypervisor in their cars, IIRC - What else? Are there any private deployments you guys are aware of?

angry_octet 24d ago
The Secure Enclave on iOS devices runs sepOS, and earlier fork of the UNSW/NICTA L4 nano kernel work. Obviously Apple has huge resources to verify their own kernel on their own hardware, but seL4 is likely much more secure. With Apple's appetite for architectural security improvements I think they will eventually move to an seL4 derivative with special hardware security add-ons. There are a number of talks at the upcoming seL4 summit, but see 2025, e.g. Kry10 KOS. https://sel4.systems/Summit/2025/program.html https://sel4.systems/Summit/2025/program.html

StilesCrisis 24d ago

Coming soon: a side-channel timing attack which completely invalidates this result

msdz 24d ago
Are timing (over network) attacks, physical access, etc. typically excluded from research like this for being “out of scope”, so to speak? I’m not familiar.
- StilesCrisis 24d ago
  Mathematical proofs tend to assume that they are built on perfect foundations (you have to stop the proof somewhere!). Unfortunately, proving that the software is correct just means you need to find a flaw in a deeper layer.
- monster_truck 24d ago
  They aren't out of scope as much as they are irrelevant. It has been a best practice to ensure that the things you would be attempting to attack the timing of do not let you do this for a very long time. We are so far down this road that we do things like generate thousands of values and throw most of them away to mitigate the laziest attempts at what would be considered in scope.
  - less_less 24d ago
    It's still relevant (and probably also rather difficult) to prove that seL4 itself conforms to those best practices.
avadodin 24d ago
That's a bit unfair. Any side–channel attack that invalidates seL4 security guarantees —assuming the proofs are valid— also invalidates any other imaginable OS'. We're in the philosophical territory of tasking infallible beings with stopping their own flawless creations.
fosslinux 24d ago
Although, there is ongoing research regarding time protection (https://trustworthy.systems/projects/timeprotection/ https://trustworthy.systems/projects/timeprotection/) which prevents exactly timing channels. Including proofs of seL4 providing time protection.
- brohee 24d ago
  Security-partition switches that carefully reset all shared micro-architectural state, while making switch times completely deterministic, and in particular, independent of previous execution history. I'm afraid it means clearing all caches at each context switch. The performance penalty is really high.
  - spectra2 23d ago
    Not all caches are cleared. There are some clever techniques to partition off-core caches (i.e. the L3) as part of the isolation boundaries enforced by the kernel. What I think is particularly exciting is that a new RISCV64 instruction to clear microarchitectural state is in the process of being standardised! So I'm hopeful that, while it should not be ignored, the performance penalty will not be too high.
torginus 24d ago
I don't think a side channel attack against L4 would be particularly useful - the kernel's tiny, and doesn't really do much other than scheduling, IPC and capabilities. Anything you might want to learn lives in other processes. That said, the big caveat of the whole thing, is that by pushing stuff traditionally considered to be sensitive to user space doesn't solve security or stability, it makes it other people's problem. There's no reason you couldn't do a side channel (or a different kind of) attack against a process that hosts the filesystem.
- spectra2 23d ago
  I think the danger of a side-channel attack against seL4 is more dangerous than you believe. The security proofs ensure that threads should not be able to read data they do not have permission to, or write to places they do not have permission to etc., through any part of the kernel's interface, which includes the mechanisms for inter-process communication. That means a side-channel, or some gap in this proof, would allow learning about what lives in processes! While seL4 is definitely not a silver bullet for building a secure and stable system, I would argue that its security guarantees mitigate the risks. seL4's security proofs guarantee that the kernel obeys the information flow policy of your system, derived from the runtime distribution of permissions ("capabilities") in your system. If the interface to your filesystem, for example, is through the judicious granting of capabilities, then you can rest assured there is no side-channel.
  - torginus 23d ago
    > That means a side-channel, or some gap in this proof, would allow learning about what lives in processes! This is true, but outside of the scope of the kernel (which is a theme with microkernel). Side channels are unfortunately a side effect of how hardware works. This is kind of a theme with microkernels, they are not a silver bullet, I agree. The Linux kernel handles a lot of things L4 doesn't like memory management, drivers, file systems that L4 doesn't. So a filesystem bug would not be a kernel bug in L4 but would have just as serious implications as on Linux. So while what they're claiming about security imo is true, they're claiming much less here than people here assume. > If the interface to your filesystem, for example, is through the judicious granting of capabilities, then you can rest assured there is no side-channel. How do you mean? Caps are a software contract, and side channels, like manipulating CPU cache with speculative execution is lower level than that. I don't see how that would mitigate issues like that.
brohee 24d ago
The assumptions the proof makes are pretty clearly listed: https://sel4.systems/Verification/assumptions.html https://sel4.systems/Verification/assumptions.html The one covering side channels is pretty honest: Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels. So the proof won't be invalidated at it does not cover that particular threat. Now the question is how useful the is a proof not covering side channels? I'd say pretty useful and it doesn't mean they don't have counter measures for to counter their exploitation, nor that they are not effective, just that a proof of efficiency is out of reach for now.
- brohee 24d ago
  To add to that, the only way I see proof of absence of timing channels is by proving both the software and the hardware design side by side, and then the proof would hold only for a specific core. Something that would look both at the code manipulating secrets and at the Verilog for the specific core/memory chips. I've not been working in that space in a long while but AFAIK such a thing is nowhere near ready. I suspect it will be a lot easier if the hardware design is optimised for provability, which won't be good at all for performance. But there are plenty of contexts where security matters a lot more than performance (SMC, BMC, RoT and co at the very least). And then you'd need assurance that the Verilog is faithfully transcribed in the silicon, which is a can of worms in itself.
  - simiones 24d ago
    I don't think it needs to be so dramatic. You could have a proof that the algorithms don't contain data-dependent logic, and perhaps ensure that no data-dependent instructions are generated; and that all branches have the same number of instrution-cycles (adding padding if not). You'd then simply rely on the architecture-specific instruction timing differences to be respected by the compiler. Would something like this guarantee that no side-channels are possible on any architecture? Perhaps not, but it would still get you most of the way there.
IsTom 24d ago
There's another can of worms that are rowhammer-esque attacks.
dathinab 24d ago
you are missing the point just because something isn't perfect and handles everything you can come up with doesn't mean it isn't still very very useful nothing in nature is truly perfect and down-talking grate but not perfect things will just make us stuck in a pretty shitty world which never improves because no improvement by itself "perfectly/fully" solves whatever problem set you are looking at
CalChris 24d ago
Side channel timing attacks are micro architectural. The SeL4 security proofs are architectural.
- warkdarrior 23d ago
  Is cache hierarchy considered part of the microarchitecture?
saidnooneever 23d ago
the proofs prove certain things they do not prove a system is infallable or actually secure they rule out certain things in certain parts of the code.

i_am_a_peasant 24d ago

Read the fine print, "non-MCS (mixed criticality systems), unicore"

avadodin 24d ago

The embedded and military markets may keep funding them for the foreseeable future but they need a native seL4/Linux if they want to honestly claim they are improving systems' security with their capability model. Secure–boot virtualization platforms are dime a dozen nowadays.

jdub 24d ago
"native seL4/Linux"? seL4 can already host Linux VMs, and there are various methods of running Linux code / binaries without hardware virtualisation.
- avadodin 24d ago
  A real OS user-land kernel handling real workloads within the capability model. A Linux VM isn't it.
- adastra22 24d ago
  And what would be the point of that?
  - jdub 23d ago
    It's frequently done in research and industry when there's a component that has strict timing and separation requirements, and a bunch of supporting software that doesn't. Like an autonomous helicopter. Flight control? Very important. A bunch of hardware drivers and services for imaging, navigation, comms... not so much, and not worth the (long term ongoing) effort of replatforming.
    - adastra22 23d ago
      I don't understand though. If it's all running on the Linux VM, then you haven't inherited any of the secL4 benefits.
      - spectra2 23d ago

grommet_kit 23d ago

[dead]