Verifying the SHA-3 Implementation from OpenSSL with the Software Analysis Workbench

This paper discusses a proof of SHA-3 in OpenSSL. SHA-3 is the new standard from NIST for computing digests. OpenSSL is one of the most widely used implementations of cryptographic protocols. Cryptol and the Software Analysis Workbench (SAW) are a language and verification engine to specify cryptographic primitives and prove equivalence to implementations. As digests are the basis for all cryptographic protocols, the research in this paper is an automated SAW proof of equivalence between the SHA-3 standard and its OpenSSL implementation in C. The research contributes Cryptol specifications for the standard. The equivalence proof shows the importance of overrides in SAW that replace models from C code with those from Cryptol to reduce the complexity of the proof obligations that must be accomplished relative to the implementation in C. The research establishes the viability of verifying modern cryptographic primitives and the importance of modularity in their definitions, and implementations, for overrides to manage complexity.