59 citations · 188 across the 17 of their papers we have counts for
20 papers
A Quantitative Flavour of Robust Reachability
Sébastien Bardin, Guillaume Girol
Many software analysis techniques attempt to determine whether bugs are reachable, but for security purpose this is only part of the story as it does not indicate whether the bugs…
Scalable Program Clone Search Through Spectral Analysis
Tristan Benoit, Jean-Yves Marion, Sébastien Bardin
We consider the problem of program clone search, i.e. given a target program and a repository of known programs (all in executable format), the goal is to find the program in the r…
Binsec/Rel: Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-Erasure
Lesly-Ann Daniel, Sébastien Bardin, Tamara Rezk
This paper tackles the problem of designing efficient binary-level verification for a subset of information flow properties encompassing constant-time and secret-erasure. These pro…
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…
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…
A Deductive Verification Framework for Circuit-building Quantum Programs
Christophe Chareton, Sébastien Bardin, François Bobot +2
While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of su…
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…
Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level
Lesly-Ann Daniel, Sébastien Bardin, Tamara Rezk
The constant-time programming discipline (CT) is an efficient countermeasure against timing side-channel attacks, requiring the control flow and the memory accesses to be independe…
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…
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…
Freeing Testers from Polluting Test Objectives
Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov +3
Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting efficient test suites, able to detect a maximum number of bugs w…
CDCL-inspired Word-level Learning for Bit-vector Constraint Solving
Zakaria Chihani, François Bobot, Sébastien Bardin
The theory of quantifier-free bit-vectors (QF_BV) is of paramount importance in software verification. The standard approach for satisfiability checking reduces the bit-vector prob…
Targeting Infeasibility Questions on Obfuscated Codes
Robin David, Sébastien Bardin, Jean-Yves Marion
Software deobfuscation is a crucial activity in security analysis and especially, in malware analysis. While standard static and dynamic approaches suffer from well-known shortcomi…
Generic and Effective Specification of Structural Test Objectives
Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov +2
While a wide range of different, sometimes heterogeneous test coverage criteria have been proposed, there exists no generic formalism to describe them, and available test automatio…
A Combined Approach for Constraints over Finite Domains and Arrays
Sébastien Bardin, Arnaud Gotlieb
Arrays are ubiquitous in the context of software verification. However, effective reasoning over arrays is still rare in CP, as local reasoning is dramatically ill-conditioned for…
Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria
Sébastien Bardin, Nikolai Kosmatov, François Cheynier
Automatic test data generation (ATG) is a major topic in software engineering. In this paper, we seek to bridge the gap between the coverage criteria supported by symbolic ATG tool…