4 ms·
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)
by mswphd 1mo ago
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 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).
- brohee 1mo agoI 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...
- Someone 1mo agoWithout cache, without virtual memory, without throttling when the more hardware is switched on or the CPU gets hot, without memory that’s unreliable under load (https://en.wikipedia.org/wiki/Row_hammer https://en.wikipedia.org/wiki/Row_hammer), etc.
- rivetfasten 1mo agoThat works fine for some crypto algorithms, but as stated in the paper not for everything. As I understand it, this proof needs to support conditionals for example.