PLDI 2015
Sat 13 - Wed 17 June 2015 Portland, Oregon, United States
PLDI 2015 (series) / Research Papers /

Verification of a Cryptographic Primitive: SHA-256

PLDI 2015 Research Papers
Mon 15 Jun 2015 17:15 - 17:40 at PLDI Main RED (Portland 256) - TOPLAS Chair(s): Michelle Strout

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 w.r.t. the operational semantics for C, connected to the CompCert verified optimizing C compiler.

Published in ACM Transactions on Programming Languages and Systems 37(2) 7:1-7:31, March 2015

Mon 15 Jun

Displayed time zone: Tijuana, Baja California change

17:15 - 17:40
TOPLASResearch Papers at PLDI Main RED (Portland 256)
Chair(s): Michelle Strout Colorado State University
17:15
25m
Talk
Verification of a Cryptographic Primitive: SHA-256
Research Papers
A: Andrew W. Appel Princeton
Andrew W. Appel

Andrew W. AppelAuthor

Princeton