Verification of a Cryptographic Primitive

Name: Verification of a Cryptographic Primitive
Creator: Andrew W. Appel
Keywords: 2. Zero hunger, 4. Education, 0202 electrical engineering, electronic engineering, information engineering, 02 engineering and technology

Andrew W. Appel

Found an issue? Give us feedback

ACM Transactions on ...arrow_drop_down

ACM Transactions on Programming Languages and Systems

Article . 2015 . Peer-reviewed

License: https://www.acm.org/publications/policies/copyright_policy#Background

Data sources: Crossref

https://dx.doi.org/10.1145/270...

Article

Data sources: Microsoft Academic Graph

Verification of a Cryptographic Primitive

SHA-256

descriptionPublicationkeyboard_double_arrow_right Article 16 Apr 2015 English Publisher:Association for Computing Machinery (ACM)Journal:ACM Transactions on Programming Languages and Systems, volume 37, pages 1-31 (issn: 0164-0925, eissn: 1558-4593,

Copyright policy )

Authors: Andrew W. Appel;

doi: 10.1145/2701415

Verification of a Cryptographic Primitive

- Summary
- Metrics

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.

Related Organizations

College of New Jersey
United States

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	115
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Top 1%
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Top 1%
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Top 1%