The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography

TY - GEN

T1 - The Last Yard

T2 - 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, in affiliation with the annual Symposium on Principles of Programming, Languages, ,POPL 2024

AU - Haselwarter, Philipp G.

AU - Hvass, Benjamin Salling

AU - Hansen, Lasse Letager

AU - Winterhalter, Théo

AU - Hriţcu, Cǎtǎlin

AU - Spitters, Bas

N1 - Publisher Copyright: © 2024 Owner/Author.

PY - 2024/1

Y1 - 2024/1

N2 - 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.

AB - 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.

KW - AES

KW - computer-aided cryptography

KW - Coq

KW - formal verification

KW - high-assurance cryptography

U2 - 10.1145/3636501.3636961

DO - 10.1145/3636501.3636961

M3 - Article in proceedings

AN - SCOPUS:85182919079

SP - 30

EP - 44

BT - CPP 2024

A2 - Timany, Amin

A2 - Traytel, Dmitriy

A2 - Pientka, Brigitte

A2 - Blazy, Sandrine

PB - Association for Computing Machinery

Y2 - 15 January 2024 through 16 January 2024

ER -