The doctoral student will be hosted at Loria, Vandœuvre-lès-Nancy, France, will
join the Pesto team, and will interact with the members of the Formosa Crypto
group. Loria is a research unit (UMR 7503), common to CNRS, the University of
Lorraine, CentraleSupélec and Inria. Pesto is an Inria research team whose aim
is to build formal models and techniques, for computer-aided analysis and design
of security protocols (in a broad sense). The Formosa Crypto Group studies and
develops formally verified cryptography and its high-efficiency implementations,
in particular through the Jasmin and EasyCrypt tools.

The Jasmin low-level programming language is designed for implementing
high-assurance cryptographic libraries. It gives to programmers enough control
so as to reach optimal run-time performances and guarantee various safety and
security properties, such as “constant-time”, a widespread software
counter-measure against timing side-channel attacks. The compiler that produces
assembly from Jasmin programs is written and certified using the Coq proof
assistant: its correctness theorem justifies that results established at the
source level do apply at the assembly level.

The aim of this doctoral work is to study how compilation techniques, dedicated
to low-level programming, can streamline both tasks of writing low-level
efficient secure programs and of verifying them. Indeed today Jasmin programmers
must take care of many low-level details, usually automatically dealt with by
compilers: instruction selection and scheduling, spilling, etc. Moreover, as
shown by the various case studies that have been carried on until now, there is
a real practical difficulty of reusing parts of existing Jasmin programs or of
their proofs. Therefore this doctoral study aims on one hand to improve the
flexibility of the compiler without compromising the ability to finely control
low-level details when necessary, and without loosing the possibility of
precisely reasoning at the source level about behaviors of the target program
after compilation. On the other hand it will explore techniques of separate
compilation so as to make Jasmin programs more modular. These works about the
Jasmin language and its certified compiler shall be validated through large
realistic case studies.

Any previous experience with the Jasmin compiler is strongly recommended.