4 ms·

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-depende

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.

brohee 1mo ago
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.
- Dylan16807 1mo ago
  You don't need to know how long a load will take, you just need to know the duration doesn't depend on secret data.
logdahl 1mo ago
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 :^)
- less_less 1mo ago
  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.

brohee 1mo ago

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.

Dylan16807 1mo ago
You don't need to know how long a load will take, you just need to know the duration doesn't depend on secret data.

logdahl 1mo ago

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 :^)

less_less 1mo ago
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.