16 citations · 27 across the 8 of their papers we have counts for
10 papers
Combining static analysis and dynamic symbolic execution in a toolchain to detect fault injection vulnerabilities
Guilhem Lacombe, David Feliot, Etienne Boespflug +1
Certification through auditing allows to ensure that critical embedded systems are secure. This entails reviewing their critical components and checking for dangerous execution pat…
A tool assisted methodology to harden programs against multi-faults injections
Etienne Boespflug, Abderrahmane Bouguern, Laurent Mounier +1
Fault attacks consist in changing the program behavior by injecting faults at run-time in order to break some expected security properties. Applications are hardened against fault…
BAXMC: a CEGAR approach to Max#SAT
Thomas Vigouroux, Cristian Ene, David Monniaux +2
Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free p…
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…
Output-sensitive Information flow analysis
Cristian Ene, Laurent Mounier, Marie-Laure Potet
Constant-time programming is a countermeasure to prevent cache based attacks where programs should not perform memory accesses that depend on secrets. In some cases this policy can…
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…
Combining Static and Dynamic Analysis for Vulnerability Detection
Sanjay Rawat, Dumitru Ceara, Laurent Mounier +1
In this paper, we present a hybrid approach for buffer overflow detection in C code. The approach makes use of static and dynamic analysis of the application under investigation. T…
GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties.
Didier Bert, Marie-Laure Potet, Nicolas Stouls
In this paper, we present a method and a tool to build symbolic labelled transition systems from B specifications. The tool, called GeneSyst, can take into account refinement level…
Security Policy Enforcement Through Refinement Process
Nicolas Stouls, Marie-Laure Potet
In the area of networks, a common method to enforce a security policy expressed in a high-level language is based on an ad-hoc and manual rewriting process. We argue that it is pos…