CCS 2017 - Session 4I

Verifying Crypto

Thursday, 11:00am-12:30pm

Session chair: Micah Sherr

Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs

Ming-Hsien Tsai (Academia Sinica), Bow-Yaw Wang (Academia Sinica), Bo-Yin Yang (Academia Sinica)

A Fast and Verified Software Stack for Secure Function Evaluation

José Bacelar Almeida (HASLab – INESC TEC / Universidade do Minho), Manuel Barbosa (HASLab – INESC TEC / DCC FC Universidade do Porto), Gilles Barthe (IMDEA Software Institute), François Dupressoir (University of Surrey), Benjamin Grégoire (INRIA Sophia-Antipolis), Vincent Laporte (IMDEA Software Institute), Vitor Pereira (HASLab – INESC TEC / DCC FC Universidade do Porto)

[PDF]
[Paper]
[Artifact]

Verified Correctness and Security of mbedTLS HMAC-DRBG

Katherine Q. Ye (Princeton University / Carnegie Mellon University), Matthew Green (Johns Hopkins University), Naphat Sanguansin (Princeton University), Lennart Beringer (Princeton University), Adam Petcher (Oracle), Andrew W. Appel (Princeton University)

[PDF]
[Paper]
[Artifact]