Right now

My team

I'm part of the Inria SUSHI team, located at CentraleSupélec Rennes.
The team focuses on security at the interface between hardware and software, with interests ranging from hardware architecture to binary executable analysis. The goal is to find vulnerabilities, and/or ensure the absence of them, by relying at least partially on formal methods.

My work

In general, I'm interested by security at the binary-level. This includes finding vulnerabilities through code analysis, as I did during my PhD, as well as manual reverse-engineering.
I also have an interest in formal methods, such as symbolic execution, which can be used for said code analysis.

PhD students

Master students

During my PhD

My PhD work was focused on creating a trace analysis, inspired by dynamic symbolic execution, in order to guide automatic test cases generation.

The key idea is analyzing execution traces to identify constraints on user inputs, then generating solutions to those constraints. In practice, our lightweight symbolic execution reasons on execution traces, and computes approximated path predicates up to a chosen point in the trace. As path predicates, any test case satisfying these constraints will follow the target trace, up to the target point. And by approximating them, the resulting constraints are simpler to solve, at the cost of not being correct and complete.
This was implemented as a (not available) plugin to the BinSEC analysis platform.

We then modified a fuzzing tool (AFL), which searches for (and finds) vulnerabilities in programs by generating test cases (more or less) randomly. Our modified fuzzer generates specific test cases, which satisfy constraints computed by the analysis.

The resulting combination relies on the constraints generated by the symbolic analysis to guide AFL's test generation, for example to discover new paths, or to create test cases exploring specific paths.

Responsibilities