arXiv subjects

Vincent Laporte

Publications and source records attributed to Vincent Laporte.

3 recordsLinked to original sources

arXiv2025

KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM

High-assurance cryptography provides strong guarantees that source implementations are functionally correct and provably secure. In this paper, we demonstrate that the Jasmin compiler preserves functional correctness and KEM-IND-CCA security (which were established in prior work) of a highly optimized Jasmin implementation of ML-KEM used in the popular messenger Signal. Our proof of preservation is fully mechanized in the Rocq prover and is based on three general contributions: (1) A general framework for modeling game-based security and for reasoning about preservation of game-based security under compilation. (2) A new, interaction-trees-based semantics of Jasmin and assembly programs. Our new semantics supports features required by ML-KEM, such as probabilistic computations and rejection sampling routines. (3) A new relational Hoare logic for interaction trees, which we use to prove correctness of the JASMIN compiler under our new semantics.

cs.PL↗

arXiv2019

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations

We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as hand-written assembly. We illustrate ur approach using ChaCha20-Poly1305, one of the mandatory ciphersuites in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code. We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking. We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt.

cs.CR↗

arXiv2013

Formal Verification of a C Value Analysis Based on Abstract Interpretation

Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone. This paper presents a formal verification using the Coq proof assistant: a formalization of a value analysis (based on abstract interpretation), and a soundness proof of the value analysis. The formalization relies on generic interfaces. The mechanized proof is facilitated by a translation validation of a Bourdoncle fixpoint iterator. The work has been integrated into the CompCert verified C-compiler. Our verified analysis directly operates over an intermediate language of the compiler having the same expressiveness as C. The automatic extraction of our value analysis into OCaml yields a program with competitive results, obtained from experiments on a number of benchmarks and comparisons with the Frama-C tool.

cs.PL↗