Paper 2025/1607 Original: eprint.iacr.org/2025/1607 ↗
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt
Abstract
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
- Preprint.
- History
- 2025-09-07: last updated
- 2025-09-07: published
- Short URL
- https://ia.cr/2025/1607
- License
- https://creativecommons.org/publicdomain/zero/1.0/
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},
url = {https://eprint.iacr.org/2025/1607}
}