I am an associate professor at Université de Lille. I teach computer science, and my research interests include automatic program verification (static analysis), compilation, security, networks, operating systems and hardware architecture.
On my spare time, I also like coding in various hobby project, and security challenges on sites such as Root-Me.
Tool to perform binary code analysis with polyhedra.
Tool to perform symbolic computation of WCET (Worst-Case Execution Time) of binary programs by static analysis.
ANR (Agence Nationale de la Recherche) research project to handle large execution time variability in real-time systems.
ANR (Agence Nationale de la Recherche) research project to enable symbolic WCET (Worst-Case Execution Time) computation in critical real-time systems.
Open Tool for Adaptive WCET Analysis (OTAWA) is an opensource tool to statically estimate the worst-case execution time of programs.
JSAnalyzer is a tool to automatically deobfuscate JavaScript malwares using abstract interpretation and compiler optimization methods.
ARM-multitool is a very small (binary less than 4Ko) free-standing (doesn’t need C library) daemon to facilitate security experiments on ARM embedded devices. It allows file upload/download, listen/connect TCP proxy, and spawning shell with or without controlling TTY.
SalTTY is a tool to demonstrate the dangers of incorrect tty handling when dropping privileges. It may allow an attacker to gain access to a terminal used by a privileged user, in order to inject command or sniff passwords.
EccVPN is a VPN that uses ECC (actually, erasure codes) to reconstruct dropped network packets.
In this paper we propose a new abstract domain for static analysis of binary code. Our motivation stems from the need to improve the precision of the estimation of the Worst-Case Execution Time(WCET) of safety-critical real-time code. WCET estimation requires computing information such as upper bounds on the number of loop iterations, unfeasible execution paths, etc. These estimations are usually performed on binary code, mainly to avoid making assumptions on how the compiler works. Our abstract domain, based on polyhedra and on two mapping functions that associate polyhedra variables with registers and memory, targets the precise computation of such information. We prove the correctness of the method, and demonstrate its effectiveness on benchmarks and examples from typical embedded code.
Parametric Worst-case execution time (WCET) analysis of a sequential program produces a formula that represents the worst-case execution time of the program, where parameters of the formula are user-defined parameters of the program (as loop bounds, values of inputs, or internal variables, etc). In this article we propose a novel methodology to compute the parametric WCET of a program. Unlike other algorithms in the literature, our method is not based on Integer Linear Programming (ILP). Instead, we follow an approach based on the notion of symbolic computation of WCET formulae. After explaining our methodology and proving its correctness, we present a set of experiments to compare our method against the state of the art. We show that our approach dominates other parametric analyses and produces results that are very close to those produced by non-parametric ILP-based approaches, while keeping very good computing time.
Real-time embedded software often runs on a supervisory operating system software layer on top of a modern processor. Thus, to give timing guarantees on the execution time and response time of such applications, one needs to consider the timing effects of the operating system, such as system calls and interrupts - over and above modeling the timing effects of micro-architectural features such as pipeline and cache. Previous works on Worst-case Execution Time (WCET) analysis have focused on micro-architectural modeling while ignoring the operating system’s timing effects. As a result, WCET analyzers only estimate the maximum un-interrupted execution time of a program. In this work, we present a framework for RTOS aware WCET analysis - where the timing effects of system calls and interrupts can be accounted for. The key observation behind our analysis is to capture the timing effects of system calls and/or interrupts, as well as their effect on the micro-architectural states, compositionally via a damage function. This damage function is then composed in a controlled fashion to result in a RTOS-aware, micro-architecture-aware timing analysis of an application. We show the use of our analysis to compute the worst-case response time for a real-life robot controller software which runs several tasks such as balancing and/or navigation on top of a real-time operating system running on a modern processor.
You can find here the full list of my publications.