Jean-Christophe Léchenet

Home

About me

Since October 2020, I am a postdoc/research engineer in the STAMP team of Inria, located in Sophia-Antipolis, France. I am working with Benjamin Grégoire on Jasmin, a formally verified compiler. We are part of the Formosa Crypto effort aiming at producing high-speed and high-assurance cryptography. One of the main results of Formosa Crypto is the libjade cryptographic library featuring some post-quantum cryptographic primitives.

Before joining STAMP, I was a postdoc in the Celtique team of the IRISA laboratory, Rennes, France, working with David Pichardie on CompCertSSA, a formally verified C compiler. Before joining Celtique, I was a PhD student at CEA and CentraleSupélec, under the supervision of Pascale Le Gall and Nikolai Kosmatov.

Research

My research interests include formal methods, programming languages and software safety. I am a regular and pleased user of the Coq proof assistant.

Research engineer in team STAMP (2020-...)

I am currently working on Jasmin, a compiler written in Coq used to write high-assurance and high-speed cyptography. Programs are written in the Jasmin language and compiled to assembly. Jasmin is a rather low-level language that lets users control the low-level details of their programs but also features high-level constructs to make their lives easier than if they wrote these programs directly in assembly.

When I joined STAMP, I worked on adapting the proof of one pass of the compiler following the addition of major features to the language and the compiler (in particular, internal functions and sub-arrays). This was included in release 2022.04.0 of Jasmin. More recently, I worked on adding the ARM architecture as a supported target of the Jasmin compiler (only x86_64 was supported initially), and on a compilation pass automatically inserting some code zeroing the stack at the end of the main function (for security reasons). These two works should be included in the next major version of Jasmin.

Postdoc in team Celtique (2018-2020)

During my first postdoc, I worked on the formalization in CompCertSSA of a liveness analysis due to Boissinot et al. (2008). This analysis, unlike traditional dataflow-based ones, does not compute the whole liveness of a program at once, but instead answers so-called liveness queries of the form "is variable a live at program point q?". Another particularity of this analysis is that it specifically targets programs under SSA form.

I also worked on strengthening the dominance test of CompCertSSA, since this was a requirement for the formalization of the liveness analysis.

PhD thesis (2015-2018)

During my PhD, I worked on program slicing as a tool for software verification. More precisely, the goal was to give a formal justification to program slicing in the presence of runtime errors. This is explained in more details here.

The second part of my PhD was based on an elegant theory of control dependence due to Danicic et al. (2011) (control dependence is one of the two pillars of program slicing). The contributions were a formalization of part of this theory in Coq, and the design of an algorithm optimizing the one described by Danicic et al. This algorithm was written and proved correct in the Why3 proof system. This is detailed here.

Introductory examples to Coq and Why3 can be found here.

Contact