[curves] Summary of ECC 2015 Workshop
peter at cryptojedi.org
Thu Oct 1 21:39:43 PDT 2015
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
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 173 bytes
Desc: Digital signature
More information about the Curves