Gregory Maxwell <[email protected]> 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
signature.asc
Description: Digital signature
_______________________________________________ Curves mailing list [email protected] https://moderncrypto.org/mailman/listinfo/curves
