3 ms·
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
by leni536 11y ago
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).
- grogers 11y agoI 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.
- matthavener 11y agoCryptol 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/ZUC.cry#L296-L308 https://github.com/GaloisInc/cryptol/blob/master/examples/ZU...)
- giech 11y agoIt 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 https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf HMAC verification (Usenix Security): http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf