2 papers
cs.PL2026
(Dis)Proving Spectre Security with Speculation-Passing Style
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter +2
Constant-time (CT) verification tools are commonly used for detecting potential side-channel vulnerabilities in cryptographic libraries. Recently, a new class of tools, called spec…
cs.PL2025
KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter +4
High-assurance cryptography provides strong guarantees that source implementations are functionally correct and provably secure. In this paper, we demonstrate that the Jasmin compi…