The
Silent
Tower

I'm a PhD student at Laboratoire de Conception et d'Intégration des Systèmes (LCIS) (Lab for the Design and Integration of Systems) in Valence, France. I have the pleasure to work with Laure Gonnord and Christophe Deleuze. I got a theoretical background from my masters' at ENS de Lyon and now work to apply it on compilation and embedded software, where I have the most experience.

Here is a copy of my résumé.

Contact email: Show email address

Research projects#

In embedded systems#

My Ph.D work focuses on getting countermeasures for fault injection and side-channels attacks up the compilation chain, by making the compiler generate fault-resistant code from source annotations. This is difficult for multiple reasons all related directly or indirectly to the abstraction stack, but mostly:

• The effect of these low-level attacks is completely lost on source code, which doesn't model any of the micro-architectural or physical phenomena manipulated by the attacks;
• And even once you can conceive a way for a program to do its stuff without being vulnerable to attacks, it's generally going to mix source code and assembler code changes and the compiler will makes things ugly very quickly by not cooperating.

I played with the first problem in [MDG24], a project in which I built a software/hardware countermeasure to a pretty nasty fault attack that skips code by the byte, corrupting instructions. Modeling the fetch unit's behavior as part of a semantics of assembly allows us to close the (small) abstraction gap between the assembler code and the attacked encodings. Even then, getting the toolchain to generate protected requires us to intervene both in the back-end and the linker (foreshadowing).

In formal verification#

• Extensions of the congruence closure algorithm

  Congruence closure is a standard algorithm for deciding equality — it essentially saturates a set of equalities using equivalence relation properties and the congruence rule f = g -> x = y -> f x = g y. Interestingly, it can be generalized if we extend it to partial equivalence relations (PERs), leading to a more versatile semi-decision procedure. This work was supervised by Pierre Corbineau at Verimag (detailed report here).

• Abstract semantics for monadic interpreters

  A project with Yannick Zakowski. The Vellvm project has a fascinating semantic model for programs called Interaction Trees, which is a free monad (with non-termination). It makes it possible to define language semantics by starting with symbolic events for all non-trivial features (memory accesses, division, exceptions, etc.) then progressively refining the model by applying monad transformers onto the interaction tree, replacing each feature's symbolic events with their actual implementation.

  I've worked on designing certified abstract interpreters using this progressive refinement model. The key is that it enables proving each feature's abstraction independently and then composing correctness proofs to prove the entire interpreter correct. This cuts down on the proof effort significantly. Challenges arise due to differences in control flow between the original program and its abstract version, which must be tracked. Paper on that coming to ICFP'24!

• Composable formal semantics for MLIR

  On a trip to Tobias Grosser's team (then in Scotland) I worked on prototyping formal semantics for MLIR, whose dialect-based extensibility is a very good match for Interaction Trees. This project was implemented in Lean 4, which has an incredibly satisfying meta-programming side. The now-Cambridge team published these results a while later.

Teaching#

I work as a teaching assistant designing and supervising practicals at Grenoble INP - Ésisar, an engineering school with pretty wide coverage of automatics, electronics, and computer science. I've taught practicals and the occasional lecture with the following classes:

• 2nd-year Algorithms and C programming;
• 2nd-year Recursive and functional programming (Haskell);
• 3rd-year Algorithms and C programming (up to a basic MIPS emulator).

Publications#