Verification of a cryptographic primitive: SHA-256 7

Research output: Contribution to journalArticlepeer-review

105 Scopus citations


This article presents a full formal machine-checked verification of a C program: theOpenSSL implementation of SHA-256. This is an interactive proof of functional correctness in the Coq proof assistant, using the Verifiable C program logic. Verifiable C is a separation logic for the C language, proved sound with respect to the operational semantics for C, connected to the CompCert verified optimizing C compiler.

Original languageEnglish (US)
Article number7
JournalACM Transactions on Programming Languages and Systems
Issue number2
StatePublished - Apr 1 2015

All Science Journal Classification (ASJC) codes

  • Software


  • Cryptography


Dive into the research topics of 'Verification of a cryptographic primitive: SHA-256 7'. Together they form a unique fingerprint.

Cite this