Thèse de Jasmin à Wasm H/F - Doctorat.Gouv.Fr

Établissement : Université Côte d'Azur École doctorale : STIC - Sciences et Technologies de l'Information et de la Communication Laboratoire de recherche : Secure Programming Languages & Tools for Security Direction de la thèse : Benjamin GRÉGOIRE ORCID 0000000166509924 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-05-03T23:59:59 Ce projet de thèse s'inscrit dans le domaine de la cryptographie sûre et performante, en s'appuyant sur Jasmin, un environnement de développement conçu pour produire des implémentations cryptographiques à la fois efficaces, correctes et sécurisées. Le langage Jasmin combine des abstractions de haut niveau avec un contrôle fin proche de l'assembleur, permettant d'écrire du code optimisé tout en conservant une sémantique formelle facilitant les preuves de correction.

Le compilateur Jasmin génère du code assembleur prévisible sans surcoût d'exécution et est formellement vérifié, garantissant que les propriétés prouvées au niveau source (sécurité, terminaison, correction fonctionnelle) sont préservées. Grâce à des outils comme EasyCrypt, il permet également de vérifier des propriétés cryptographiques avancées, notamment le temps constant, essentiel pour se protéger contre les attaques par canaux auxiliaires.

Parallèlement, WebAssembly (Wasm) est une machine virtuelle moderne, sûre et portable, conçue pour exécuter du code efficacement dans divers environnements. Fortement typé, sécurisé et proche du matériel, Wasm constitue une cible pertinente pour des applications critiques comme la cryptographie, notamment grâce à ses extensions SIMD favorisant les performances.

L'objectif principal de la thèse est de développer un backend du compilateur Jasmin vers WebAssembly. Cela implique d'adapter l'infrastructure existante aux spécificités de Wasm (structure en bytecode, contrôle structuré) et d'étendre le langage Jasmin pour supporter certaines fonctionnalités de Wasm, comme les types de référence liés au garbage collector.

Un enjeu central est de préserver les garanties formelles de Jasmin lors de la compilation vers Wasm. En particulier, il s'agit de prouver que la correction fonctionnelle et les propriétés de temps constant sont maintenues. Pour cela, la thèse s'appuiera notamment sur ct-Wasm, une extension de Wasm conçue pour garantir l'exécution en temps constant.

Un autre axe important concerne l'impact des modes d'exécution de Wasm, notamment l'interprétation et la compilation Just-In-Time (JIT). La thèse cherchera à déterminer si ces mécanismes respectent les propriétés de sécurité, et si le JIT ou ses optimisations dynamiques peuvent introduire des fuites d'information.

Le programme de recherche est structuré en trois axes :

Développement du backend Wasm : adaptation du compilateur Jasmin et preuve formelle de correction de la compilation.
Préservation du temps constant : compilation vers ct-Wasm et analyse des implémentations Wasm pour détecter d'éventuelles fuites.
Étude du JIT : analyse de l'impact des optimisations dynamiques sur la sécurité et exploration de méthodes pour garantir le temps constant au niveau du code natif.

En résumé, cette thèse vise à combiner vérification formelle, compilation et sécurité cryptographique, afin de produire des programmes fiables et résistants aux attaques, tout en tirant parti des avantages de WebAssembly comme plateforme d'exécution moderne. Jasmin [1, 3, 2] is a workbench for high-assurance and high-performance cryptography. Its imple-
mentations are designed to be efficient, safe, correct, and secure. The Jasmin programming language
seamlessly combines high-level and low-level constructs, enabling a programming style often described
as assembly in the head. Its formal semantics enables rigorous reasoning about program behavior.
The Jasmin compiler produces predictable assembly code and guarantees that high-level abstrac-
tions incur no run-time overhead. The compiler is formally verified for correctness in Rocq, ensuring
that properties established at the source level are preserved at the assembly level. These properties
include safety, termination, and functional correctness.
The Jasmin workbench leverages the EasyCrypt toolset1 for formal verification. Jasmin programs
can be translated into EasyCrypt 2 to prove functional correctness and cryptographic security prop-
erties. Furthermore, Jasmin provides tools to verify that programs are cryptographic constant-time,
meaning that they are resistant to low-level side-channel attacks such as cache attacks. Although this
verification is performed at the source level, the compiler guarantees that this property is preserved
down to the generated machine code.
WebAssembly [4, 8, 6] (Wasm) is a modern virtual machine designed to serve as a universal
execution platform. Despite its name suggesting a web-oriented design, Wasm is a general-purpose
low-level language, similar in spirit to other virtual machines such as the JVM [5]. It is strongly typed,
memory-safe, sandboxed, and enforces structured control flow (e.g., loops and functions only).
Wasm distinguishes itself by being language-agnostic, relatively close to the underlying hardware,
and relying on a minimal runtime system. One of its key strengths lies in its strong safety guarantees,
which make it a particularly attractive compilation target for safety-critical applications, including
cryptographic software. In addition, the SIMD extension, which introduces 128-bit vector instructions,
further enhances Wasm's suitability for high-performance cryptographic implementations, where data-
parallel operations are essential. The primary objective of this PhD is to develop a new backend for the Jasmin compiler targeting
Wasm. While a significant portion of the existing compiler infrastructure can be reused, several
components will need to be adapted to account for the structured, bytecode-based nature of Wasm,
which differs from traditional machine assembly languages.
Part of the work will also involve extending the Jasmin language to support specific features of
Wasm and its extensions, in particular the reference types introduced by the Wasm garbage collector.
A key objective is to preserve the strong guarantees provided by Jasmin. First, we aim to formally
establish that compilation to Wasm preserves the functional correctness of Jasmin programs.
Second, we aim to prove that the compilation process preserves cryptographic constant-time prop-
erties. To this end, we will target the constant-time extension of Wasm (ct-Wasm).
Since Wasm programs can be executed either through interpretation or via Just-In-Time (JIT)
compilation, an important research question is the impact of these execution models on constant-time
guarantees. In particular:
- Can we ensure that JIT-compiled code preserves constant-time properties?
- How can we guarantee that the JIT compiler itself, including its runtime monitoring mechanisms,
does not introduce side-channel leaks? To address these challenges, the PhD will be structured along three main research axes:
- Axis 1: Design and implementation of a Wasm backend for Jasmin
In this first axis, the Jasmin compiler will be extended to target WebAssembly. This requires
adapting the existing compiler, developed and verified in Rocq, to account for the structured,
bytecode-based nature of Wasm as a target architecture.
Since the Jasmin compiler is formally proven to preserve semantics, any modification must be
accompanied by a corresponding formal proof. To achieve this, we will rely on an existing for-
malization of Wasm semantics [8], which will serve as the foundation for proving the correctness
of the compilation process.
In addition, we plan to extend the Jasmin language with new types in order to support features
specific to Wasm, in particular reference types introduced by the Wasm garbage collector.
- Axis 2: Constant-time compilation using ct-Wasm
The second axis focuses on preserving cryptographic constant-time guarantees. The compiler
will be extended to target ct-Wasm [7], a variant of Wasm designed to enforce constant-time
programming disciplines.
The main objective is to formally establish that any Jasmin program verified as constant-time
at the source level is compiled into a Wasm program that preserves this property.
In parallel, we will investigate existing Wasm interpreter implementations to assess whether
they effectively ensure constant-time behavior in practice, and to identify potential sources of
side-channel leakage.
- Axis 3: Impact of JIT compilation on constant-time guarantees
The third axis investigates the impact of Just-In-Time (JIT) compilation on cryptographic
constant-time guarantees, and aims to develop techniques to ensure that the generated native
code remains constant-time.
2
This part is inherently more exploratory. Due to their size and complexity, JIT compilers are
likely out of reach for full formal verification. Instead, we will explore alternative approaches,
such as analysis or verification techniques applied to the generated machine code.
A key challenge stems from the adaptive nature of JIT compilation: runtime monitoring in-
formation is used to guide optimization decisions. This raises the question of whether such
mechanisms may introduce side-channel leaks. A central goal of this axis is therefore to under-
stand and mitigate the potential leakage induced by these dynamic behaviors.

Anglais: lu, écrit, parlé
Connaissance de la programmation fonctionnelle
Connaissance des langages d'assembleur
Connaissance d'assistants de preuve formelle (Rocq)