Verification of a Cryptographic Primitive
Abstract
This article presents a full formal machine-checked verification of a C program: the OpenSSL 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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Apr 16, 2015
- Source ID
- 10.1145/2701415
Entities
People
- Andrew Appel
Organizations
- Defense Advanced Research Projects Agency
- Princeton University