[openssl-dev] curve25519

[Nico Williams]

On Sun, Jun 21, 2015 at 10:36:30PM +0000, Pascal Cuoq wrote:
> Short answer:
> 
> No tools that are useful for usable implementations of asymmetric
> cryptography, that I know of, but useful tools for confirming that
> symmetric cryptography designed for constant-time implementation was
> correctly implemented.
> 
> Long answer:
> 
> [...]
> 
> Following this line of reasoning gives you two tools that you can use:
>
> [...]
> 
> There are two problems with both these approaches:
> 
> - the assumption about knowledge about the time taken by assembly
> instructions. Both Frama-C and, to the best of my knowledge, ctgrind,
> ignore intermediate values computed from secrets and passed as
> arguments to the division instruction. On a modern processor the
> execution time of division reveals information about its inputs:

That's correct.

Reasoning about CT is hard, and doing so from C source is harder because
the optimizer can potentially convert CT code to not-CT code.

This argues for analyzing assembly, not C.

> So to summarize the first problem, there are a lot of assumptions.
> That doesn't prevent going forward, and taking any new discovery of an
> information leak through timing as a bug and fixing them as flaws are
> discovered in our assumptions, but you won't be “checking” that C code
> is “constant-time” in the sense that you might check the proof of a
> theorem. But even more serious is the second problem:
> [...]
>                                                      [...]. Also you
> should bear in mind that when implementing cache-aware constant-time
> look-up tables, you are really assuming a lot of things about the
> behavior of the processor.  [...]

At some point one is forced to dispense with -or, rather, augment-
static analysis with dynamic analysis.

The beauty of dynamic analysis is that it really short-circuits all of
these considerations and gives you an answer you can trust.  But one
does have to make sure to eliminate sources of jitter (e.g., quiesce the
system, disable interrupts on the CPU doing the benchmarking, ...).  If
one is able to trace execution to pinpoint sources of variability, then
dynamic analysis can even point out where secrets leak into timing.

Nico
--