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.
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.
I don't think you can ignore memory access. The whole "hyperthreading considered harmful" was because of shared cache between contexts. That's why I think a proof is in reach without cache, much harder with one...
What you want is a proof that microarchitectural timing differences (ie. the difference between a cache hit and cache miss) cannot possibly turn into architecturally-visible timing differences. If a program cannot reliably distinguish between two points in time, time is not a suitable channel for programs.
You could have an ISA where timing information is simply not presented to the programmer, but programmers like being able to profile their programs.
You don't need to prove the hardware correct to prove that the software is free from timing side-channels. You just need a model of the hardware that captures timing information.
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...
Interesting, but not unheard of. Think of attacks like Row Hammer. No revolutionary physics needed. But chip designers cannot fully apply quantum field theory to an entire CPU, so they necessarily use simplified a simplified physics model. The resulting chips then need to be empirically verified to correct places where that simplified model diverges to much from the messy reality, which means that the chip design is only as good as the empirical testing done to it.
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.
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.
What about power draw? Maybe that doesn't count as a side channel (I'm not a security guy). Afaik, CMOS transistors mostly draw power on switching state, so a normal adder adding 0+0 or 1+1 is visible in the power draw.
I googled a bit and found Sense Amplifier-Based Logic (SABL). Super interesting :^)
Power draw is a side channel, yeah. It's not as easy to exploit in software as timing (including memory timing), but there are software exploits in some cases if it affects the CPU's frequency (HertzBleed) or if it can be read through channels like a sound card or radio receivers. For attackers who have physical access it's very much in scope.
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.
I'm not so sure. It's pretty hard to know how many cycles a register load instruction will take if there is a cache, or worse a cache hierarchy. That's why I think it will be a lot easier to have a proof on simple cache less designs...
Your version is likely good enough in practice though.
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.
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.
Although, there is ongoing research regarding time protection (https://trustworthy.systems/projects/timeprotection/) which prevents exactly timing channels. Including proofs of seL4 providing time protection.
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.
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.
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.
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.
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
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.
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.
> but they need a native seL4/Linux if they want to honestly claim they are improving systems' security with their capability model.
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.
I mean something like MkLinux with seL4 at its core with all processes and drivers running under seL4 and taking advantage of the seL4 capability model.
It doesn't even have to be a Linux–compatible OS in theory although that is the standard to beat.
Just securing the whole billion lines of Linux kernel code would make a huge difference even if the user-land ABI remains the same.
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.
The current value is that you can take an existing specialist/military device that used distinct physical chips for provable isolation, and consolidate them all onto one chip (lowering cost/power/space), while still saying that you met the security requirements
So its more of an economic argument than that of increasing security
Coming soon: a side-channel timing attack which completely invalidates this result
The assumptions the proof makes are pretty clearly listed: 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.
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.
In general you don’t need things that fancy. Instead, you can take
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).
I don't think you can ignore memory access. The whole "hyperthreading considered harmful" was because of shared cache between contexts. That's why I think a proof is in reach without cache, much harder with one...
What you want is a proof that microarchitectural timing differences (ie. the difference between a cache hit and cache miss) cannot possibly turn into architecturally-visible timing differences. If a program cannot reliably distinguish between two points in time, time is not a suitable channel for programs.
You could have an ISA where timing information is simply not presented to the programmer, but programmers like being able to profile their programs.
You don't need to prove the hardware correct to prove that the software is free from timing side-channels. You just need a model of the hardware that captures timing information.
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...
A backdoor in physics would be interesting indeed, but not as likely as a rogue agent in a TSMC fab...
Interesting, but not unheard of. Think of attacks like Row Hammer. No revolutionary physics needed. But chip designers cannot fully apply quantum field theory to an entire CPU, so they necessarily use simplified a simplified physics model. The resulting chips then need to be empirically verified to correct places where that simplified model diverges to much from the messy reality, which means that the chip design is only as good as the empirical testing done to it.
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.
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.
What about power draw? Maybe that doesn't count as a side channel (I'm not a security guy). Afaik, CMOS transistors mostly draw power on switching state, so a normal adder adding 0+0 or 1+1 is visible in the power draw.
I googled a bit and found Sense Amplifier-Based Logic (SABL). Super interesting :^)
Power draw is a side channel, yeah. It's not as easy to exploit in software as timing (including memory timing), but there are software exploits in some cases if it affects the CPU's frequency (HertzBleed) or if it can be read through channels like a sound card or radio receivers. For attackers who have physical access it's very much in scope.
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.
I'm not so sure. It's pretty hard to know how many cycles a register load instruction will take if there is a cache, or worse a cache hierarchy. That's why I think it will be a lot easier to have a proof on simple cache less designs...
Your version is likely good enough in practice though.
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.
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.
Although, there is ongoing research regarding time protection (https://trustworthy.systems/projects/timeprotection/) which prevents exactly timing channels. Including proofs of seL4 providing time protection.
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.
Side channel timing attacks are micro architectural. The SeL4 security proofs are architectural.
Is cache hierarchy considered part of the microarchitecture?
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.
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.
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.
It's still relevant (and probably also rather difficult) to prove that seL4 itself conforms to those best practices.
There's another can of worms that are rowhammer-esque attacks.
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
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?
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
Read the fine print, "non-MCS (mixed criticality systems), unicore"
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.
> but they need a native seL4/Linux if they want to honestly claim they are improving systems' security with their capability model.
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.
https://en.wikipedia.org/wiki/L4Linux
Per that link, this runs a Linux kernel as a VM on top of an L4-based hypervisor.
I mean something like MkLinux with seL4 at its core with all processes and drivers running under seL4 and taking advantage of the seL4 capability model.
It doesn't even have to be a Linux–compatible OS in theory although that is the standard to beat.
But running Linux on top of seL4 does not take advantage of the capability model at all. You need a new non-unix-like userspace for that.
Just securing the whole billion lines of Linux kernel code would make a huge difference even if the user-land ABI remains the same.
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.
The current value is that you can take an existing specialist/military device that used distinct physical chips for provable isolation, and consolidate them all onto one chip (lowering cost/power/space), while still saying that you met the security requirements
So its more of an economic argument than that of increasing security
"native seL4/Linux"? seL4 can already host Linux VMs, and there are various methods of running Linux code / binaries without hardware virtualisation.
A real OS user-land kernel handling real workloads within the capability model.
A Linux VM isn't it.
And what would be the point of that?