activity
20132022
most citedA Deductive Verification Framework for Circuit-building Quantum Programs

59 citations · 188 across the 17 of their papers we have counts for

collaborators
Showing cs.CRShow all

9 papers · 1 filter

cs.CR2022

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…

cs.CR2022★ 2 cited

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…

cs.CR2021★ 3 cited

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…

cs.CR2020★ 8 cited

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…

cs.CR2020

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…

cs.CR2020★ 18 cited

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…

cs.CR2019★ 55 cited

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…

cs.CR2019

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…

cs.CR2016

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…