3 ms·

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

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 1mo 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.
- spectra2 1mo ago
  Sorry! I didn't read "side-channel" as also referring to microarchitectural timing channels, but mostly to refer to (architectural) storage channels. You are right, it's not covered at all until the experimental Time Protection work is completed [0]. [0] https://trustworthy.systems/projects/timeprotection/ https://trustworthy.systems/projects/timeprotection/

torginus 1mo 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.

spectra2 1mo ago
Sorry! I didn't read "side-channel" as also referring to microarchitectural timing channels, but mostly to refer to (architectural) storage channels. You are right, it's not covered at all until the experimental Time Protection work is completed [0]. [0] https://trustworthy.systems/projects/timeprotection/ https://trustworthy.systems/projects/timeprotection/