Verification of a cryptographic primitive: SHA-256 7

Andrew W. Appel

doi:10.1145/2701415

Verification of a cryptographic primitive: SHA-256 7

Andrew W. Appel

Research output: Contribution to journal › Article › peer-review

126 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 language	English (US)
Article number	7
Journal	ACM Transactions on Programming Languages and Systems
Volume	37
Issue number	2
DOIs	https://doi.org/10.1145/2701415
State	Published - Apr 1 2015

All Science Journal Classification (ASJC) codes

Software

Keywords

Cryptography

Access to Document

10.1145/2701415

Cite this

@article{314e022545c446e7bf0c39f19834c91e,

title = "Verification of a cryptographic primitive: SHA-256 7",

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

keywords = "Cryptography",

author = "Appel, \{Andrew W.\}",

note = "Publisher Copyright: {\textcopyright} 2015 ACM 0164-0925/2015/04-ART7 \$15.00 Additional.",

year = "2015",

month = apr,

day = "1",

doi = "10.1145/2701415",

language = "English (US)",

volume = "37",

journal = "ACM Transactions on Programming Languages and Systems",

issn = "0164-0925",

publisher = "Association for Computing Machinery",

number = "2",

}

TY - JOUR

T1 - Verification of a cryptographic primitive

T2 - SHA-256 7

AU - Appel, Andrew W.

PY - 2015/4/1

Y1 - 2015/4/1

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

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

KW - Cryptography

UR - https://www.scopus.com/pages/publications/84928543472

UR - https://www.scopus.com/pages/publications/84928543472#tab=citedBy

U2 - 10.1145/2701415

DO - 10.1145/2701415

M3 - Article

AN - SCOPUS:84928543472

SN - 0164-0925

VL - 37

JO - ACM Transactions on Programming Languages and Systems

JF - ACM Transactions on Programming Languages and Systems

IS - 2

M1 - 7

ER -

Verification of a cryptographic primitive: SHA-256 7

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this