POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Mon 15 Jan 2024 11:00 - 11:30 at Kelvin Lecture - Compiler / Program Verification Chair(s): Vadim Zaliva

The field of high-assurance cryptography is quickly maturing, yet a unified foundational framework for end-to-end formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, high-assurance cryptographic implementations; and (3) the SSProve foundational verification framework for modular cryptographic proofs. We first connect Hacspec with SSProve by devising a new translation from Hacspec specifications to imperative SSProve code. We validate this translation by considering a second, more standard translation from Hacspec to purely functional Coq code and generate a proof of the equivalence between the code produced by the two translations. We further define a translation from Jasmin to SSProve, which allows us to formally reason in SSProve about efficient cryptographic implementations in Jasmin. We prove this translation correct in Coq with respect to Jasmin’s operational semantics. Finally, we demonstrate the usefulness of our approach by giving a foundational end-to-end Coq proof of an efficient AES implementation. For this case study, we start from an existing Jasmin implementation of AES that makes use of hardware acceleration and prove that it conforms to a specification of the AES standard written in Hacspec. We use SSProve to formalize the security of the encryption scheme based on the Jasmin implementation of AES.

Slides (presentation.pdf)1.81MiB

Mon 15 Jan

Displayed time zone: London change

11:00 - 12:30
Compiler / Program VerificationCPP at Kelvin Lecture
Chair(s): Vadim Zaliva University of Cambridge, UK
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter Aarhus University, Benjamin Salling Hvass Aarhus University, Lasse Letager Hansen Aarhus University, Theo Winterhalter INRIA Saclay, Cătălin Hriţcu MPI-SP, Bas Spitters Aarhus University
Pre-print File Attached
UTC time, formally verified
Ana de Almeida Borges University of Barcelona and Formal Vindications S.L., Mireia González Bedmar University of Barcelona and Formal Vindications S.L., Juan Conejero Rodríguez University of Barcelona and Formal Vindications S.L., Eduardo Hermo Reyes University of Barcelona and Formal Vindications S.L., Joaquim Casals Buñuel University of Barcelona and Formal Vindications S.L., Joost J. Joosten University of Barcelona
VCFloat2: Floating-point error analysis in Coq
Andrew W. Appel Princeton University, Ariel E. Kellison Cornell University