|
|
|
|
|
|
by schoen
2636 days ago
|
|
|
This is terrific stuff. One thing to think about might be that when we use the C output of this project in a non-formally-verified compiler (something other than CompCert), there might be compiler bugs that undo some of these guarantees. (The easiest one to see is that optimizers in the compiler could undo the constant-time guarantee -- I assume that the output or documentation indicates using keywords or pragmas or compiler options to disable some kinds of optimizations, but there could for example be a compiler bug where some optimizations can't be disabled this way.) |
|
|
Even though Curve25519 is built to be easy to implement in constant time, there was a non-constant time bug in a Curve25519 library: https://research.kudelskisecurity.com/2017/01/16/when-consta...
Basically the compiled code ends up using a run-time Windows library for 64-bit multiplication. That library decided to skip the upper 32-bit multiplication when the operands had 32 all zero MSBs. Oops.
ChaCha20 is also easy to implement in constant time. Which tends to be true. But most ChaCha20 implementations have other side channels. Turns out, when CPUs access non-register memory, the EM and power characteristics of that access are dependent on the bits of the data being accessed. Which means you can perform power or EM analysis on a CPU running ChaCha20 and extract the key. Oops. (Search for bricklayer attack)
In other words, become a cryptographer because you'll always have more work :)