We have proved, with machine-checked proofs in Coq, that an OpenSSL implementation of HMAC with SHA-256 correctly implements its FIPS functional specification and that its functional specification guarantees the expected cryptographic properties. This is the first machine-checked cryptographic proof that combines a source-program implementation proof, a compiler-correctness proof, and a cryptographic-security proof, with no gaps at the specification interfaces.
środa, 10 czerwca 2015
Formal verification is not easy task, for example ComCert compiler is able to verify, that optimizations haven't modified semantic of a program. Paper Verified correctness and security of OpenSSL HMAC describes verification of the whole "stack":