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.
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].
Comments
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.
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.
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/