The PACSS team develops code analysis techniques
and tools for software security. We address both source-level and
low-level codes, and we study effective combinations of static and
dynamic analysis techniques (abstract interpretation, concolic
execution and fuzzing). We currently focus on the following research
areas:
The complete list of publications related to these topics
is available here.
|
Current Members
|
Past Members
|
Related
projects
MSTIC CODEC (2019-2021) : HW/SW
co-design of processor countermeasures
IRT Pulse - CLAPS (2017-2020) :
Software robustness analysis against fault injections
IRT Pulse - NanoTrust (2017-2020)
: Design and certification of a secure processor
FUI SecurIoT (2017-2020) : Development of Secure Micro-Controller for the IoT. Web Site
ASTRID Sacade (2017-2020) : Model-based attack scenario generation for Industrial Control Systems
PEPS SISC ASSI (2016) : Security
Analysis of Industrial Control Systems
ASTRID Sertif (2014-2017) : Simulation based robustness evaluation of embedded applications against fault injection. Web Site
PIA Sécurité Numérique ARAMIS (2014-2018) : Secure architecture for Industrial Control Systems
ANR BINSEC (2013-2017) : BINary code analysis for SECurity. Web Site
We develop static analysis for binary level code dedicated to :
taint analysis
Use-After-Free vulnerability detection
Buffer overflow pattern recognition
Trace generalization for exploitability
Our approach combines a Value Set Analysis in order to determine
address and memory transfer, complex pattern recognition and
concolic execution to produce concrete attacks. Challenges are the
following ones : taking into account dynamic allocation, combining
static and dynamic analysis for scalability, and using
memory model both suitable to symbolic execution and
exploitability analysis.
We developed a set of prototypes (LIsTT, Gueb, etc.) based on
the REIL intermediate format (using BinNavi and Ida
Pro). We are also implied in the development of the BINSEC platform in which
we propose a dynamic-symbolic execution engine.
Some related publications:
Security of embedded systems like smart-cards, secured dongles and
IoTs relies on the robustness of devices against physical
fault attacks (such as laser or electromagnetic attacks).
Current certification schemes (e.g., Common Criteria) require
protection mechanisms against multi-fault injection attacks. For a
given system, such kind of attacks leads to an exponential number
of unintended behaviors. In order to help both developers and
auditors to master this complexity, an important challenge is to
propose faithful fault models and automated code analysis
taking into account the impact of physical attacks.
We develop the Lazart
tool (Laser Attack and Robustness) allowing to
evaluate the code robustness against multi-fault injections
with respect to some behavioral properties. Lazart operates at the
LLVM level and relies on Klee, a dynamic-symbolic
execution tool. We currently investigate the use of Lazart
for counter-measure analysis.
In addition, within the ANR Sertif project, we built FISCC,
the first benchmark dedicated to fault injection robustness
evaluation.
Some related publications:
Constant-time programming is a countermeasure to
prevent side-channel attacks. This policy can be
safely relaxed if one can prove that the program does not leak
more information than the intended public output. In this
framework, we proposed a static analysis based on a new
information flow property, called output sensitive
noninterference. The novelty of this approach is that we track the
dependence of leakage variables with respect not only to the
initial values of input variables (as in classical approaches for
noninterference), but taking also into account the final values of
output variables.
We adapted this approach to LLVM IR
and we developed a prototype to verify LLVM implementations.
We are currently extending our prototype towards a tool able to
deal with cryptographic libraries.
Some related publications:
Security of Industrial Control Systems
Industrial Control
Systems (e.g. SCADA and PLC) are mostly based on proprietary
infrastructures and legacy software. Because of this
specificity, despite the fact that their security is
critical, these systems have been less studied in the literature.
Within the FUI Aramis project, we proposed an
end-to-end approach to take into account applicative filtering
rules for industrial protocols, dealing both with safety and
security concerns.
Our model based approach allows to take into account both the
industrial process, the weakness of protocols and an attacker
model.
In the framework of the PEPS ASSI (2016-2017), we developed security proofs for the industrial standard OPC-UA focusing on integrity (generally not addressed by cryptographic verification tools).
Currently, in collaboration within the Cyber@Alps
Institute, we investigate the use of code
reverse-engineering techniques for vulnerability detection in
PLCs.
Some related publications:
2019 :
Frédéric Recoules, Sébastien Bardin, Richard Bonichon, Laurent
Mounier, Marie-Laure Potet.
Get rid of inline assembly through trustable
verification-oriented lifting. International
Conference on Automated Software Engineering (ASE 2019)
Cristian Ene, Laurent Mounier, Marie-Laure Potet.
Output-Sensitive Information Flow Analysis
FORTE 2019 - 39th International Conference on Formal
Techniques for Distributed Objects, Components, and Systems, LNCS
11535, June 2019
Mohamad Kaouk,Jean-Marie Flaus, Marie-Laure Potet, Roland Groz
A Review of Intrusion Detection Systems for Industrial Control
Systems. CoDIT
2019: 1699-1704
Benjamin Farinier, Sébastien Bardin, Richard Bonichon, Laurent
mounier and Marie-Laure Potet
En finir avec les faux positifs avec l’exécution symbolique
robuste
Journées Francophones des Langages Applicatifs
Février 19
2018 :
Jannik Dreier, Maxime Puys, Marie-Laure Potet, Pascal Lafourcade,
Jean-Louis Roch
Formally and practically verifying flow properties in
industrial systems.
Computers & Security
https://www.sciencedirect.com/science/article/pii/S016740481831441X?via%3Dihub#aep-article-footnote-id
Benjamin Farinier, Sébastien Bardin, Richard Bonichon
and Marie-Laure Potet.
Model Generation for Quantified Formulas: A Taint-Based
Approach.
30th International Conference on Computer Aided Verification}
CAV 18
Jonathan Salwan, Sebastien Bardin and Marie-Laure Potet
Binary Deobfuscation and Dynamic Symbolic Execution
DIMVA'18, 15th Conference on Detection of Intrusions and Malware
& Vulnerability Assessment
2017 :
Jannik Dreier and Maxime Puys and Marie-Laure Potet and Pascal
Lafourcade and Jean-Louis Roch.
Formally Verifying Flow Properties in Industrial Systems.
SECRYPT 2017, Madrid, Spain, July 24-26, 2017.
Maxime Puys and Marie-Laure Potet and Abdelaziz Khaled.
Generation of Applicative Attacks Scenarios Against Industrial
Systems.
Foundations and Practice of Security - 10th International
Symposium,
FPS 2017, Nancy, France, October 23-25, 2017.
Jonathan Salwan and Sébastien Bardin and Marie-Laure Potet.
Deobfuscation of VM based software protection.
Symposium sur la s{\'{e}}curit{\'{e}} des technologies de
l'information et des communications, SSTIC, France, Rennes, June
7-9 2017.
2016-2012 :
Louis Dureuil, Guillaume Petiot, Marie-Laure Potet, Thanh-Ha Le,
Aude Crohen,
Philippe De Choudens. FISSC: a Fault Injection and Simulation
Secure Collection.
SAFECOMP 2016.
Maxime Puys, Marie-Laure Potet, Pascal Lafourcade. Formal
Analysis of Security Properties on the OPC-UA SCADA Protocol.
SAFECOMP 2016.
R. David, S. Bardin, J. Feist, L. Mounier, M-L Potet, T. Ta, J-Y
Marion. Specification of Concretization and
Symbolization Policies in Symbolic Execution. ISSTA 2016.
Robin David and Sébastien Bardin and Josselin Feist and Jean-Yves
Marion and Marie-Laure Potet and Thanh Dinh Ta. BINSEC/SE: A
Dynamic Symbolic Execution Toolkit for Binary-level Analysis.
Proceedings of SANER 2016. Osaka, Japan. March 2016
Gustavo Grieco, Guillermo Luis Grinblat, Lucas Uzal, Sanjay Rawat,
Josselin Feist and Laurent Mounier. Toward large-scale
vulnerability discovery using Machine Learning. Proceedings
of CODASPY 2016, ACM, New Orleans, USA, March 2016
Franck de Goer and Roland Groz and Laurent Mounier. Lightweight
Heuristics to Retrieve Parameter Associations from Binaries.
Proceedings of PPREW 2015, Los Angeles, USA, best paper award.
Josselin Feist and Laurent Mounier and Marie-Laure Potet. GUEB
: Static Detection of Use-After-Free on Binary. Toorcon San Diego 2015
Louis Dureuil and Marie-Laure Potet and Philippe de Choudens and
Cécile Dumas and Jessy Clédière. From
Code Review to Fault Injection Attacks: Filling the Gap
using Fault Model Inference. Cardis 2015.
Pascal Lafourcade and Maxime Puys. Performance Evaluations of
Cryptographic Protocols Verication Tools Dealing with
Algebraic Properties. FPS 2015.
Lionel Rivière and Marie-Laure Potet and Thanh-Ha Le and Julien
Bringer and Hervè Chabanne and Thanh-Ha Le and
Maxime Puys. Combining High-Level and Low-Level Approaches to
Evaluate Software Implementations Robustness Against Multiple
Fault Injection Attacks. International Symposium on
Foundations and Practice of Security, FPS 2014,
Lecture Notes in Computer Science.
Rawat, Sanjay and Mounier, Laurent and Potet, Marie-Laure. LiSTT
: An Investigation into Unsound-incomplete Yet Practical Result
Yielding Static Taintflow Analysis. Proceedings of SAW 2014
(ARES Workshop)},Fribourg (Switzerland), IEEE, September 2014.
Potet, Marie-Laure and Feist, Josselin and Mounier, Laurent.
Analyse
de Code et Recherche de Vulnérabilités. Revue MISC,
Hors-série juin 2014, Editions Diamond.
Marie-Laure Potet, Laurent Mounier, Maxime Puys and Louis
Dureuil.
Lazart: a symbolic approach to evaluate the impact of fault
injections by test inverting.
ICST 2014, International Conference on Software Testing.
Josselin Feist and Laurent Mounier and Marie-Laure Potet.
Statically Detecting Use After Free on Binary Code.
Journal of Computer Virology and Hacking Techniques, january 14
Gregor Gössler, Daniel Le Métayer, Eduardo Mazza, Marie-Laure
Potet and Lacramioara Astefanoaei.
Apport des méthodes formelles pour l'exploitation des logs
informatiques dans un contexte contractuel.
Technique et Science Informatiques, vol 33, no 1-2, 2014.
Gustavo Grieco, Laurent Mounier and Marie-Laure Potet.
A stack model for symbolic buffer overflow
exloitability analysis (Extended abstract).
CSTVA 2013, Luxembourg, 22 March 2013
Josselin Feist and Laurent Mounier and Marie-Laure Potet.
Statically Detecting Use After Free on Binary Code.
Grehack 2013
Dumitru Ceara and Laurent Mounier and M-L PotetTaint
Dependency Sequences: a characterization of insecure execution
paths based on input-sensitive cause sequences.
MDV'10, Modeling and Detecting Vulnerabilities workshop,
associated to ICST 2010, IEEE digital Library
P-A. Masson and M-L Potet and J. Julliand and all. An Access
Control Model Based Testing Approach for Smart Card
Applications: Results of the POSE project.
Journal of Information Assurance and Security, n 5, 2010 (335-351)
Sofia Bekrar, Chaouki Bekrar, Roland Groz, Laurent Mounier. A
Taint Based Approach for Smart Fuzzing. In Proceedings of SecTest,
Giuliano Antoniol, Antonia Bertolino, Yvan Labiche (eds.), Pages
818-825, 2012.
Sanjay Rawat, Laurent Mounier. Finding Buffer Overflow
Inducing Loops in Binary Executables. In Proceedings of
Sixth International Conference on Software Security and
Reliability (SERE), Pages 177-186, Gaithersburg, Maryland, USA,
2012