Doing What It Says on The Crypto Tin: Verified Cryptography Code For Everyone
When do developers ever create proof that their code actually does what it says it does? Well, it’s not an easy task, especially to prove against a mathematical implementation. So what we normally do is to test against a specification that matches the requirements, but this is no proof we have forgotten to test for every scenario. But a great new paper by Brett Boston, et al defines machine-assisted proofs for 256-bit AES (GCM) and SHA-384 [here]:
Within the paper, the authors focus on the LibCrypto, and which contains a range of cryptographic primitives that normally have tightly focused code and which does not have many external dependencies. One of the major challenges is that the code tends to be highly optimized (and typically written as a mixture of assembly language code and C), and where it is not easy to match these to formal proofs of operation. On the other hand, we see the “secure-by-design” software libraries, such as with EverCrypt. While these provide a good way forward in terms of security, these are not as widely adopted as the popular libraries of OpenSSL and BoringSSL. The paper provides a formal proof of implementation using…
