Paper 2023/185

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
Théo Winterhalter, Inria Saclay - Île-de-France Research Centre
Catalin Hritcu, Max Planck Institute for Security and Privacy
Bas Spitters, Aarhus University
Abstract

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 automatically proving the equivalence of 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, prove its security using SSProve, and also that it conforms to a specification of the AES standard written in Hacspec.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint.
Keywords
high-assurance cryptographyformal verificationcomputer-aided cryptographyAESCoq
Contact author(s)
philipp @ haselwarter org
bsh @ cs au dk
letager @ cs au dk
theo winterhalter @ inria fr
catalin hritcu @ mpi-sp org
spitters @ cs au dk
History
2023-02-15: approved
2023-02-13: received
See all versions
Short URL
https://ia.cr/2023/185
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2023/185,
      author = {Philipp G. Haselwarter and Benjamin Salling Hvass and Lasse Letager Hansen and Théo Winterhalter and Catalin Hritcu and Bas Spitters},
      title = {The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography},
      howpublished = {Cryptology ePrint Archive, Paper 2023/185},
      year = {2023},
      note = {\url{https://eprint.iacr.org/2023/185}},
      url = {https://eprint.iacr.org/2023/185}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.