6 citations · 7 across the 3 of their papers we have counts for
6 papers
Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine
Frédéric Recoules, Sébastien Bardin, Richard Bonichon +3
Inline assembly is still a common practice in low-level C programming, typically for efficiency reasons or for accessing specific hardware resources. Such embedded assembly codes i…
No Crash, No Exploit: Automated Verification of Embedded Kernels
Olivier Nicole, Matthieu Lemerre, Sébastien Bardin +1
The kernel is the most safety- and security-critical component of many computer systems, as the most severe bugs lead to complete system crash or exploit. It is thus desirable to g…
Automatically Proving Microkernels Free from Privilege Escalation from their Executable
Olivier Nicole, Matthieu Lemerre, Sébastien Bardin +1
Operating system kernels are the security keystone of most computer systems, as they provide the core protection mechanisms. Kernels are in particular responsible for their own sec…
Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities
Manh-Dung Nguyen, Sébastien Bardin, Richard Bonichon +2
Directed fuzzing focuses on automatically testing specific parts of the code by taking advantage of additional information such as (partial) bug stack trace, patches or risky opera…
Abstract Interpretation using a Language of Symbolic Approximation
Matthieu Lemerre, Sébastien Bardin
The traditional abstract domain framework for imperative programs suffers from several shortcomings; in particular it does not allow precise symbolic abstractions. To solve these p…
An Introduction to Time-Constrained Automata
Matthieu Lemerre, Vincent David, Christophe Aussaguès +1
We present time-constrained automata (TCA), a model for hard real-time computation in which agents behaviors are modeled by automata and constrained by time intervals. TCA actions…