[curves] Summary of ECC 2015 Workshop

[Peter Schwabe]

Gregory Maxwell <gmaxwell at gmail.com> wrote:

Dear Gregory, dear all,

> "Peter Schwabe gave a stimulating talk about the problem of using
> automated tools to prove the correctness and security of crypto
> software. He demonstrated how the valgrind profiling tool can be used
> on real crypto code, but emphasised that such tools create a massive
> overhead for software developers."

Well, the summary is slightly misleading: the valgrind part is not
really a massive overhead. The correctness verification with SMT solvers
(second part of the talk) does create a massive overhead.

> I'm interested in this-- in libsecp256k1 in the past we've used
> valgrind by setting secret data to 'uninitialized'  with the memcheck
> macros and then valgrind whines about conditional branches on the
> secret data. This is far from complete, but not bad automated backstop
> on boneheaded mistakes. I'm wondering if it was just something like
> this, or something somewhat more advanced?

It was pretty much this as a small warm-up for the more serious
verification of correctness. I know about this trick by ctgrind by Adam
Langley: https://github.com/agl/ctgrind.

> In theory valgrind could be instrumented to catch any leak-prone
> operations on secret data this way... but creating a new valgrind
> checker is a somewhat daunting prospect.

I have a student who is currently looking into this. First step: make
ctgrind work for current versions of valgrind. Then we'll see where to
go from there.

Cheers,

Peter
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 173 bytes
Desc: Digital signature
URL: <http://moderncrypto.org/mail-archive/curves/attachments/20151002/cb7b8d86/attachment.sig>