undefined

points

[-]

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.

by mswphd6 hours ago|

parent|

[-]

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).

by brohee6 hours ago|

parent|

[-]

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

by gizmo6861 hours ago|

parent|

prev|

[-]

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

by simiones7 hours ago|

parent|

prev|

[-]

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.

by logdahl6 hours ago|

parent|

[-]

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

by less_less5 hours ago|

parent|

[-]

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.

by brohee6 hours ago|

parent|

prev|

[-]

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.