Preuve et Analyse de Code pour la Sécurité

(Proof and Code Analysis for Security)


The PACS team of the Verimag laboratory 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:

See also the complete list of publications and tools related to these topics.




People involved

Current Members

  • Marie-Laure Potet (Pr)

  • Laurent Mounier (MC)

  • Cristian Ene (MC)

  • Jean-Louis Roch (MC)

  • Sylvain Boulmé (MC)

  • David Monniaux (DR)

  • Frédéric Recoules (PhD Student 2017-2020)

  • Etienne Boespflug (PhD Student 2018-2021)

  • Vincent Werner (PhD Student 2018-2021)

  • Soline Ducousso (PhD Student 2021-2024)

Past Members

  • Benjamin Farinier (PhD Student 2016-2020)

  • Jonathan Salwan (PhD Student 2016-2020)
  • Louis Dureuil (PhD Student 2013-2016)

  • Josselin Feist (PhD Student 2013-2017)

  • Maxime Puys (PhD Student 2014-2018)


  • Paolo Torrini (Postdoc)
  • Thanh-Dinh Ta (Postdoc)

  • Guillaume Petiot (Postdoc)

  • Sanjay Rawat (Postdoc)

  • Gustavo Grieco (PhD Student visitor)




Related projects




Research Areas

Vulnerability detection and analysis


We develop static analysis for binary level code dedicated to :

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:


Fault injection


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.

See also The CLAM (Cross-Layer Fault Analysis for Microprocessor Architectures) Project in collaboration with Vincent Beroulle (LCIS) and Paolo Maistri (TIMA)

Some related publications:


Non-Interference

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:


Security Countermeasures into Formally Verified Compilers


Olivier Savry's team at CEA-LETI is designing a secure crypto-processor as an extension of RISC-V architecure. See their paper "CONFIDAENT: CONtrol FLow protection with Instruction and Data Authentification ENcryption" (O. Savry, M. El-Majihi and T. Hiscock at Euromicro Conference on Digital System Design 2020). This processor provides dedicated hardware to monitor control-flow hijacking and buffer-overflows attacks (by fault injection or other means). In order to benefit from a maximal protection on the control-flow, executables have to run special encryption control instructions before each branching instructions. This is achieved by instrumenting standard compilers toward RISC-V in order to insert automatically these encryption control instructions in the assembly.

PACS team works on integrating such countermeasures inside CompCert, a formally verified C compiler. Typically, we have extended the CompCert formal description of RISC-V ISA, with a functional description of encryption-control instructions: encryption mechanisms are described at a symbolic level (assuming perfect cryptography). We have also instrumented the compiler and formally proved (with the Coq proof assistant) its functional correctness: in other words, in the absence of attack, the inserted countermeasures do not disturb the behavior expected at the source level.



Tools



Publications




2020 :

Vincent Werner, Laurent Maingault and Marie-Laure Potet
An End-to-End Approach for Multi-Fault Attack Vulnerability Assessment
FDTC 2020 (Fault, Diagnosis and Tolerance in Cryptography), September 2020

Etienne Boepsflug, Cristian Ene, Laurent Mounier, Marie-Laure Potet.
Countermeasure optimization in multiple fault injection context

FDTC 2020 (Fault, Diagnosis and Tolerance in Cryptography), September 2020

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