This page is under construction

Code analysis for security evaluation


We develop code analysis tools in order to evaluate source or low-level code. We aim two types of diagnostic: robustness or  vulnerabilty detection. We consider both source and low-level code. Our approaches are based on static analysis and concolic execution.

We are also interested for modeling and verifying other security requirements (confidentiality, integrity, isolation...) in particular in the context of Common Criteria certification.



People involved
and


Current projects



Application domains : librairies, web server, embedded code, secure infrastructures and secure element, industrial  application, Common Criteria Certification



Vulnerability detection

We develop static analysis for low level code dedicated to :

Our approach is based on Value Set Analysis in order to determine address and memory transfer, complex pattern recognition and concolic execution to produce attacks. Challenges are the following ones : take into account dynamic allocation, combine static and dynamic analysis for scalability, use memory model both adapted to symbolic execution and exploitability.

We developped a set of prototypes (LIsTT, Gueb, ..) based on the REIL intermediate format (using BinNavy and Ida). We are also implied in the development of the BINSEC platform in which we propose a DSE engine.


Fault injection


In the domain of secure devices (smartcard or secured dongle) vulnerability analysis requires to evaluate the robustness of devices against fault attacks (such as laser  or electromagnetic attacks). Challenges are the following ones : propose some processes including both code analysis and physical attack impact allowing to evaluate the accuracy of fault models ans results and take into account the state of the art in term of multi-fault which requires to design more sophisticated tools (including static analysis to master the combinatorial of fault consequences).


We developped Lazart (Laser Attack and Robustness), a tool evaluating the robustness of LLVM codes against multi-fault injection and some attack scenarii. Lazart uses Klee, a concolic tool. We are in charge of the Sertif project. One of the result is FISCC, the first benchmark dedicated to fault injection robustness evaluation.





Publications


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. Speci fication 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 Feis 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 Veri cation 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