Verification of a cryptographic primitive: SHA-256 (abstract)

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

Abstract

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 w.r.t. the operational semantics for C, connected to the CompCert verified optimizing C compiler.

Original languageEnglish (US)
Title of host publicationPLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
PublisherAssociation for Computing Machinery
Number of pages1
Volume2015-June
ISBN (Electronic)9781450334686
DOIs
StatePublished - Jun 3 2015
Event36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 - Portland, United States
Duration: Jun 13 2015Jun 17 2015

Other

Other36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015
Country/TerritoryUnited States
CityPortland
Period6/13/156/17/15

All Science Journal Classification (ASJC) codes

  • Software

Fingerprint

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

Cite this