Paper 2025/1607
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt
, Universidade do Minho, INESC TEC, Universidade do Porto, INESC TEC, Max Planck Institute for Security and Privacy, Max Planck Institute for Security and Privacy, IMDEA Software Institute, Max Planck Institute for Security and Privacy, SandboxAQ, Universidade do Porto, INESC TEC, Max Planck Institute for Security and Privacy, Radboud University, PQShieldAbstract
We propose a hybrid formal verification approach that combines high-level deductive reasoning and circuit-based reasoning and apply it to highly optimized cryptographic assembly code. Our approach permits scaling up formal verifi- cation in two complementary directions: 1) it reduces the proof effort required for low-level functions where the computation logics are obfuscated by the intricate use of architecture-specific instructions and 2) it permits amortizing the effort of proving one implementation by using equivalence checking to propagate the guarantees to other implementations of the same computation using different optimizations or targeting different architectures. We demonstrate our approach via an extension to the EasyCrypt proof assistant and by revisiting formally verified implementations of ML-KEM in Jasmin. As a result, we obtain the first formally verified implementation of ML-KEM that offers performance comparable to the fastest non-verified implementation in x86-64 architectures.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Published elsewhere. Minor revision. 2025 IEEE Symposium on Security and Privacy (SP)
- DOI
- 10.1109/SP61157.2025.00214
- Contact author(s)
-
jba @ di uminho pt
gxdelerue @ gmail com
mbb @ fc up pt
gilles barthe @ mpi-sp org
luis esquivel costa @ gmail com
vincentvbh7 @ gmail com
tiago oliveira @ sandboxquantum com
hpacheco @ fc up pt
peter @ cryptojedi org
pierre-yves strub @ pqshield com - History
- 2025-09-11: approved
- 2025-09-07: received
- See all versions
- Short URL
- https://ia.cr/2025/1607
- License
-
CC0
BibTeX
@misc{cryptoeprint:2025/1607,
author = {José Bacelar Almeida and Gustavo Xavier Delerue Marinho Alves and Manuel Barbosa and Gilles Barthe and Luı́s Esquı́vel and Vincent Hwang and Tiago Oliveira and Hugo Pacheco and Peter Schwabe and Pierre-Yves Strub},
title = {Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in {EasyCrypt}},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/1607},
year = {2025},
doi = {10.1109/SP61157.2025.00214},
url = {https://eprint.iacr.org/2025/1607}
}
