18 citations · 21 across the 4 of their papers we have counts for
7 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…
AI-based Blackbox Code Deobfuscation: Understand, Improve and Mitigate
Grégoire Menguy, Sébastien Bardin, Richard Bonichon +1
Code obfuscation aims at protecting Intellectual Property and other secrets embedded into software from being retrieved. Recent works leverage advances in artificial intelligence w…
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…
How to Kill Symbolic Deobfuscation for Free; or Unleashing the Potential of Path-Oriented Protections
Mathilde Ollivier, Sébastien Bardin, Richard Bonichon +1
Code obfuscation is a major tool for protecting software intellectual property from attacks such as reverse engineering or code tampering. Yet, recently proposed (automated) attack…
Get rid of inline assembly through verification-oriented lifting
Frédéric Recoules, Sébastien Bardin, Richard Bonichon +2
Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable s…
Model Generation for Quantified Formulas: A Taint-Based Approach
Benjamin Farinier, Sébastien Bardin, Richard Bonichon +1
We focus in this paper on generating models of quantified first-order formulas over built-in theories, which is paramount in software verification and bug finding. While standard m…
A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization
Richard Bonichon, Olivier Hermant
We prove the syntactic soundness of classical tableaux with free variables and on-the-fly Skolemization. Soundness proofs are usually built from semantic arguments, and this is to…