SeL4 security proofs now complete on AArch64(proofcraft.systems) |
SeL4 security proofs now complete on AArch64(proofcraft.systems) |
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.
And then you'd need assurance that the Verilog is faithfully transcribed in the silicon, which is a can of worms in itself.
It’s basically a great front door lock: it does not guarantee nobody will break in through window, but it narrows the population of threat actors who have time and inclination.
We're in the philosophical territory of tasking infallible beings with stopping their own flawless creations.
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.
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.
I'm afraid it means clearing all caches at each context switch. The performance penalty is really high.
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
- 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?
There are a number of talks at the upcoming seL4 summit, but see 2025, e.g. Kry10 KOS.
Secure–boot virtualization platforms are dime a dozen nowadays.
Are you using "seL4/Linux" in the style of "GNU/Linux"? Because then it should be "GNU/seL4" - that would describe an OS exposing the GNU core utilities on top of the seL4 kernel. There's no way to mix the Linux kernel with the seL4 kernel, other than using one to run VMs of the other.
It doesn't even have to be a Linux–compatible OS in theory although that is the standard to beat.
So its more of an economic argument than that of increasing security
1. Some known set of architectures, with
2. Some known set of (constant time/variable time) operations
And then prove things about programs written against those architectures. See for example
https://github.com/PLSysSec/FaCT
That being said, practically the operations that are variable time are known, and are mostly* the same on all modern architectures. In particular
1. Branching on a secret-dependent variable, or
2. Indexing an array with a secret-dependent index, or
3. Some architecture specific operations (typically things like division, occasionally things like multiplications/shifting).
As I understand it, this proof needs to support conditionals for example.
You could have an ISA where timing information is simply not presented to the programmer, but programmers like being able to profile their programs.
Sure a hardware or model bug would render your proof non-applicable, but that is already the case for the existing proofs.
The bigger problem is simply that hardware designers do not care about timing side channels. Even if you did accurately model the timing behavior of a modern processor, you would just discover that trying to write software free from timing side channels is a practical impossibility.
> And then you'd need assurance that the Verilog is faithfully transcribed in the silicon, which is a can of worms in itself.
You would also need to prove that our model of physics accurately describes how that silicon would behave, and the the environment around the silicon is within the physical parameters you modeled...
Add to that the potential for unknown and mis-moddeled manufacturing defects, and manipulated electrical voltages and signals, random particle interactions, and there is a lot of room for known physics to break a verilog level proof of correctness.
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.
I googled a bit and found Sense Amplifier-Based Logic (SABL). Super interesting :^)
For software like seL4 it would generally be out-of-scope, because it depends too much on the specific hardware and specific application, not just on the kernel, and protection usually requires extensive countermeasures in those places.
Your version is likely good enough in practice though.
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.
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.
This is tangential to your comment, but it's worth mentioning that you can often begin securing a (Linux) system with seL4 by putting the entire system into a VM. Then, you iteratively port components to run "natively" over seL4 -- a process called "cyber retrofit" [0, 1].
BTW, it was probably just a typo but I believe "se" in seL4 is not a shortening of "secure", but an initialism for "secure embedded". Which is why it's not "secL4".
[0] https://sel4.systems/About/how-to-use.html
[1] https://trustworthy.systems/publications/abstracts/Klein_AKM...
The difference with a VM is that Linux is privileged vs the Linux user-land where most interesting things happen so a vulnerability within that blob is as critical as it was before other than for the few modules that are placed in seL4 custody.
For embedded applications, the Linux part is often just used to display a UI so the criticality math is a bit different.