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
2024- | Erwan Fasquel Automatic detection of vulnerabilities in binary code with Frédéric Tronel |
Master students
2024 | Thibaut Frin Automatic discovery of vulnerabilities in binary executables through the use of hybrid approaches mixing static and dynamic analysis with Frédéric Tronel |
2024 | Jack Royer Binary Deobfuscation: an Introduction with Frédéric Tronel and Thalès |
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
2023 | Program Committee GreHack Website |
2020 | Organization Committee Workshop BlackHoodie at GreHack Website |
2020 | Program Committee GreHack Website |
2019 | Organization Committee Workshop BlackHoodie at Sankt Pölten Website |