Journal
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS
Volume 37, Issue 2, Pages -Publisher
ASSOC COMPUTING MACHINERY
DOI: 10.1145/2701415
Keywords
Verification; Cryptography
Categories
Funding
- DARPA [FA8750-12-2-0293]
Ask authors/readers for more resources
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available
Share Paper
