Verification of a Cryptographic Primitive: SHA-256

Author(s): Appel, Andrew W.

Download

To refer to this page use: http://arks.princeton.edu/ark:/88435/pr19p42

Full metadata record

DC Field	Value	Language
dc.contributor.author	Appel, Andrew W.	-
dc.date.accessioned	2016-10-17T14:13:45Z	-
dc.date.available	2016-10-17T14:13:45Z	-
dc.date.issued	2015-04-16	en_US
dc.identifier.citation	Appel, Andrew W. "Verification of a Cryptographic Primitive" ACM Transactions on Programming Languages and Systems, (2), 37, 1 - 31, doi:10.1145/2701415	en_US
dc.identifier.issn	0164-0925	-
dc.identifier.uri	http://arks.princeton.edu/ark:/88435/pr19p42	-
dc.description.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.	en_US
dc.format.extent	1 - 31	en_US
dc.relation.ispartof	ACM Transactions on Programming Languages and Systems	en_US
dc.rights	This is the author’s final manuscript. All rights reserved to author(s).	en_US
dc.title	Verification of a Cryptographic Primitive: SHA-256	en_US
dc.type	Journal Article	en_US
dc.identifier.doi	doi:10.1145/2701415	-

Files in This Item:

File	Description	Size	Format
AppelACMTrans2015.pdf		357.19 kB	Adobe PDF	View/Download