How do we know if a crypto function is correctly implemented?

Re:How do we know if a crypto function is correctly implemen... by leni536 on Wednesday August 19, 2015 @07:34AM (#10084781)

Can proof assistants help (like coq)? My best bet is the specification of crypto algorithms are essentially the algorithm themselves, so maybe not. Of course if you want to avoid state than maybe you want to program your crypto in a functional language, although there could be non-trivial attack vectors too (like timing).

[ Parent | on HN ]

Re:How do we know if a crypto function is correctly implemen... by giech on Wednesday August 19, 2015 @08:40AM (#10085018)

It can, but it is highly non-trivial. Here are a couple of 2015 papers on OpenSSL verification from the same group at Princeton:

SHA verification (ACM TOPLAS): https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf

HMAC verification (Usenix Security): http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf

[ Parent | on HN ]

Re:How do we know if a crypto function is correctly implemen... by matthavener on Wednesday August 19, 2015 @08:14AM (#10084927)

Cryptol does something pretty similar. You implement your functions in Cryptol and then verify them with SAT/SMT solvers, or generative testing. Its less about verifying the C/C++ implementations and more about verifying properties of the algorithms themselves. (Example: https://github.com/GaloisInc/cryptol/blob/master/examples/ZU...)

[ Parent | on HN ]

Re:How do we know if a crypto function is correctly implemen... by grogers on Wednesday August 19, 2015 @07:49AM (#10084832)

I heard a talk by a group that is doing exactly this. They built their own language to model crypto primitives, and machine check that a java or c implementation satisfies the specification. It is neat stuff, but unfortunately their system can't model timing differences, which is an important part of crypto implementation.

[ Parent | on HN ]