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

Andrew Wilson Appel

doi:10.1145/2737924.2774972

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

Andrew Wilson Appel

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
Publisher	Association for Computing Machinery
Number of pages	1
Volume	2015-June
ISBN (Electronic)	9781450334686
DOIs	https://doi.org/10.1145/2737924.2774972
State	Published - Jun 3 2015
Event	36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 - Portland, United States Duration: Jun 13 2015 → Jun 17 2015

Other

Other	36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015
Country/Territory	United States
City	Portland
Period	6/13/15 → 6/17/15

All Science Journal Classification (ASJC) codes

Software

Access to Document

10.1145/2737924.2774972

Cite this

@inproceedings{1f880543a7bd4036902d48d8b411acc8,

title = "Verification of a cryptographic primitive: SHA-256 (abstract)",

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.",

author = "Appel, {Andrew Wilson}",

year = "2015",

month = jun,

day = "3",

doi = "10.1145/2737924.2774972",

language = "English (US)",

volume = "2015-June",

booktitle = "PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation",

publisher = "Association for Computing Machinery",

note = "36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 ; Conference date: 13-06-2015 Through 17-06-2015",

}

Appel, AW 2015, Verification of a cryptographic primitive: SHA-256 (abstract). in PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. vol. 2015-June, Association for Computing Machinery, 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, Portland, United States, 6/13/15. https://doi.org/10.1145/2737924.2774972

TY - GEN

T1 - Verification of a cryptographic primitive

T2 - 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015

AU - Appel, Andrew Wilson

PY - 2015/6/3

Y1 - 2015/6/3

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84951774625&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84951774625&partnerID=8YFLogxK

U2 - 10.1145/2737924.2774972

DO - 10.1145/2737924.2774972

M3 - Conference contribution

AN - SCOPUS:84951774625

VL - 2015-June

BT - PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

PB - Association for Computing Machinery

Y2 - 13 June 2015 through 17 June 2015

ER -

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

Abstract

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this