Verification of a cryptographic primitive: SHA-256 7

Research output: Contribution to journalArticlepeer-review

61 Scopus citations

Abstract

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
Volume37
Issue number2
DOIs
StatePublished - Apr 1 2015

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Cryptography

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

Cite this