Skip to main content

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 FieldValueLanguage
dc.contributor.authorAppel, Andrew W.-
dc.date.accessioned2016-10-17T14:13:45Z-
dc.date.available2016-10-17T14:13:45Z-
dc.date.issued2015-04-16en_US
dc.identifier.citationAppel, Andrew W. "Verification of a Cryptographic Primitive" ACM Transactions on Programming Languages and Systems, (2), 37, 1 - 31, doi:10.1145/2701415en_US
dc.identifier.issn0164-0925-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr19p42-
dc.description.abstractThis 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.extent1 - 31en_US
dc.relation.ispartofACM Transactions on Programming Languages and Systemsen_US
dc.rightsThis is the author’s final manuscript. All rights reserved to author(s).en_US
dc.titleVerification of a Cryptographic Primitive: SHA-256en_US
dc.typeJournal Articleen_US
dc.identifier.doidoi:10.1145/2701415-

Files in This Item:
File Description SizeFormat 
AppelACMTrans2015.pdf357.19 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.