Marie-Laure Potet: Recent Publications



2023


Etienne Boespflug, Laurent Mounier, Marie-Laure Potet, Abderrahmane Bouguern
A compositional methodology to harden programs against multi-fault attacks
Workshop on Fault Diagnosis and Tolerance in Cryptography, (FDTC 2023)
HAL access


Soline Ducousso and Sébastien Bardin and Marie-Laure Potet. 
Adversarial Reachability for Program-level Security Analysis.
European Symposium on Programming (ESOP) april 2023
open access

Guilhem Lacombe, David Féliot, Etienne Boespflug, Marie-Laure Potet
Combining static analysis and dynamic symbolic execution in a toolchain to detect fault injection vulnerabilities
Journal of Cryptographic Engineering (JCEN-D-21-00013),  january 2023
HAL access

2022 :

Vincent Werner, Laurent Maingault, Marie-Laure Potet
An end-to-end approach to identify and exploit multi-fault injection vulnerabilities on microcontrollers
Journal of Cryptographic Engineering (JCEN-D-21-00013), october 2022


Toward Better Fault Characterization Tests. Report 28-09-2022
https://hal.science/hal-03790625


, , , , :
BAXMC: a CEGAR approach to Max\#SAT.
Formal Methods in Computer-Aided Design (FMCAD) 2022

Vincent Werner, Laurent Maingault, Marie-Laure Potet
An end-to-end approach to identify and exploit multi-fault injection vulnerabilities on microcontrollers
Journal of Cryptographic Engineering (JCEN-D-21-00013), october 2022


Vincent Werner, Laurent Maingault and Marie-Laure Potet
Fast Calibration of Fault Injection Equipment with Hyperparameter Optimization Techniques
CARDIS 2021, Smart Card Research and Advanced Conference

Guilhem Lacombe and David Féliot and Etienne Boespflug and Marie-Laure Potet.
Combining Static Analysis and Dynamic Symbolic Execution in a Toolchain to detect Fault Injection Vulnerabilities
PROOFS 2021, 6th International Workshop on Security Proofs for Embedded Systems,Friday September 17th, 2021

Frédéric Recoules, Sébastien Bardin, Richard Bonichon, Matthieu Lemerre, Laurent Mounier, Marie-Laure Potet.
Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine.
In Proceedings of the 43rd International Conference on Software Engineering (ICSE 2021)    [distinguished paper award]

Cristian Ene, Laurent Mounier, Marie-Laure Potet.
Output-sensitive Information flow analysis. Logical Methods in Computer Science, volume 17, number 1, january 2021



2020 :

Etienne Boespflug, Cristian Ene, Laurent Mounier, Marie-Laure Potet
Countermeasures Optimization in Multiple Fault-Injection Context
Workshop on Fault Diagnosis and Tolerance in Cryptography, (FDTC 2020)

Vincent Werner, Laurent Maingault, Marie-Laure Potet
An End-to-End Approach for Multi-Fault Attack Vulnerability Assessment
Workshop on Fault Diagnosis and Tolerance in Cryptography, (FDTC 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

Frédéric Recoules, Sébastien Bardin, Richard Bonichon and Marie-Laure Potet
Faites disparaître votre assembleur en ligne avec TInA !
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 :

Josselin, Feist and Laurent Mounier and Potet Marie-Laure and Bardin Sebastien and Robin David.
Finding the Needle in the Heap: Combining Static Analysis and Dynamic Symbolic Execution to Trigger Use-After-Free.  
Proceedings of the 6th Software Security, Protection, and Reverse Engineering Workshop, {SSPREW} 2016, Los Angeles, USA, December 5-6, 2016

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

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.

Josselin Feis and Laurent Mounier and Marie-Laure Potet. GUEB : Static Detection of Use-After-Free on Binary. Toorcon, San Diego, october 2015


2014 :

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.

2013 :
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


2012 :

Gregor Goessler, Daniel Le Métayer, Eduardo Mazza, Marie-Laure Potet, Lacramioara Astefanoaei.
Apport des méthodes formelles dans l'exploitation de logs informatiques dans un contexte contractuel.
AFADL 2012, Approches Formelles dans l'Assistance au Développement de logiciels, Grenoble (11-13 janvier)(.pdf)

2011 :

Proceedings of the B 2011 Workshop, ENTCS, vol 280, 14 december 2011, editors ML Potet and H. Treharne

Sylvain Steer, Nicolas Craipeau, Daniel Le Metayer, Manuel Maareck, Marie-Laure Potet, Valérie Viet Triem Tong. Définition des responsabilités pour les dysfonctionnements de logiciels :  cadre contractuel et outils de mise en oeuvre.
Droit, sciences et techniques : quelles responsabilités ? colloque international du Réseau Droit, sciences et techniques.
Edition LexisNexis

D. Le Métayer and M. Maarek and E. Mazza and M-L Potet and S. Frénot and V. Viet Triem Tong and N. Craipeau and R. Hardouin. Liability issues in software Engineering : the use of formal methods to reduce legal uncertainties.  Comm. ACM 54 (4). 2011

2010 :

E. Mazza, M-L Potet, D. Le Métayer. A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence.
SBMF 2010, LNCS 6527, 2010

Daniel Le Métayer, Eduardo Mazza, Marie-Laure Potet. Designing log architectures for legal evidence. In 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2010, September 13-18, 2010, Pisa, Italy.

D. Le Métayer and M. Maarek and E. Mazza and M-L Potet and S. Frénot and V. Viet Triem Tong and N. Craipeau and R. Hardouin. Liability in software Engineering.  ICSE 2010, International Conference on Software Engineering, 2010.
 

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 (.pdf)
 

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), (.pdf)
 

2009 :

S. Boulmé and M-L Potet.  Relaxing restrictions on invariant composition in the B method by ownership control à la Spec#. Festschrift in honor of Egon Börger. LNCS 5115.


Twelve years of B Teaching in an engineer school: from a correct by design approach to analysis tachniques
and tools. From Research to Teachnig Formal Methods. TFM'09, 8 june, 2009, Nantes, France (.pdf).
ISBN 978-2-9512461-3-3 and the EAN 9782951246133.



2008 :

Approches formelles pour le développement de logiciels. Marie-Laure Potet et Pierre-Yves Schobbens - Technique et science informatiques. volume 27 - numéro 8. 2008


F. Dadeau, J.  Lamboley, T. Moutet, M-L Potet. A Verifiable Conformance Relationship between Smart Card Applets and Security Models.  In proceedings of ABZ 2008. September 2008. London. LNCS. vol 5115


F. dadeau, M-L Potet, Régis Tissot. A B Formal Framework for Security Developments in the domain of Smart Card Applications. 23th International Information Security Conference (SEC 2008). September 2008.  IFIP proceedingslink



2007 :

N. Stouls and M-L Potet. Security policy enforcement through refinement process. (.bib, .ps.gz, .pdf), LNCS n°4355 p.216-231, Springer-Verlag, In proceedings of B'07.

S. Boulmé and M-L Potet.  Interpreting invariant composition in the B method using the Spec# ownership relation: a way to explain and relax B restrictions. (.bib.pdf),  LNCS n°4355 p.216-231, Springer-Verlag, In proceedings of B'07.

2005 :

D. Bert, M-L. Potet et N.Stouls. GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties (.bib, LNCS), LNCS n°3455 p.299-318, Springer-Verlag, ZB 2005.

T. Deruyter, J-C Fernandez et M_L Potet. Modélisation d'architecture pour le reciblage et la paramétrisation d'une chaîne de compilateur DSP. ICSSEA05 (.pdf)

2004 :

Frédéric Badeau, Didier Bert, Sylvain Boulmé, Christophe Métayer, Marie-Laure Potet, Nicolas Stouls et Laurent Voisin. Adaptabilité et validation de la traduction de B vers C - Points de vue du projet BOM(.bib), Technique et Science Informatiques, RSTI, série TSI, numéro 7/2004, Hermès-Lavoisier.

P. Bontron, M-L. Potet. Stratégie de couverture de test à un haut niveau d'abstraction. Technique et Science Informatiques, RSTI, série TSI, numéro 7/2004, Hermès-Lavoisier.

N. Stouls et M-L. Potet. Explicitation du contrôle de développement B événementiel. Actes des Journées AFADL, Besançon, Juin 2004

2003 :

D. Bert, S. Boulmé, M-L. Potet, A. Requet, L. Voisin. Adaptable Translator of B Specifications to Embedded C Programs. in FM 2003: Formal Methods, LNCS 2805, pp. 94-113, Pise, Sept. 2003 ((.pdf)

M-L. Potet. Spécifications et développements structurés dans la méthode B. Technique et Science Informatiques, volume 22, Février 2003

F. Badeau, D.Bert, S. Boulmé, M-L. Potet, N. Stouls, L. Voisin. Traduction de B vers des langages de programmation : points de vue du projet BOM
Actes des Journées AFADL, IRISA, RENNES, Janvier 2003

P. Bontron, M-L. Potet. Stratégie de couverture de test à haut niveau d'abstraction. Actes des Journées AFADL, IRISA, RENNES, Janvier 2003


  Selected publications before 2002 :

M-L. Potet. Spécifications et développements formels: Etude des aspects compositionnels dans la méthode B. Habilitation à Diriger des Recherches, Institut National Polytechnique de Grenoble, 5 décembre 2002

Y. Ledru, L. du Bousquet, P. Bontron, O. Maury, C. Oriat, and M.-L. Potet. Test purposes: adapting the notion of specification to testing. In Proceedings of the 16th International Conference on Automated Software Engineering, San Diego, november 2001. IEEE Computer Society Press.

P. Bontron, O. Maury, L. du Bousquet, Y. Ledru, C. Oriat, M.-L.Potet. TOBIAS : un environnement pour la création d'objectifs de test à partir de schémas de test. 14th International Conference Software & Systems Engineering and their Applications-ICSSEA'2001 Paris, 2001

Pierre Bontron, Marie-Laure Potet. Automatic Construction of Validated B Components from Structured Developments. Proc. of the Conf. ZB2000, LNCS 1878, pp. 127-147, Springer-Verlag, York, U.K., Sept. 2000.

Yves Ledru, Marie-Laure Potet, Rémy Sanlaville. VDM Modules. Proc. of the User Group Meeting 11: VDM-SL, VDM in Practice. J. Fitzgerald, P. G. Larsen (Eds.): VDM Workshop at FM'99. Toulouse, Septembre 1999.

Marie-Laure Potet, Yann Rouzaud. Composition and Refinement in the B-Method. Proc. of 2nd Int. B Conference (D. Bert, ed.), LNCS 1393, Springer, pp. 46-65, April 1998.Composition and Refinement in the B method

Didier Bert, Marie-Laure Potet, Yann Rouzaud. A study on components and assembly primitives in B.
In Proc. of First B Conference, IRIN, Nantes Ed. H. Habrias, pp. 47-62, Novembre 1996.

Yves Ledru, Marie-Laure Potet. A VDM specification of the steam-boiler problem.
In Steam-Boiler Case Study, LNCS 1165, pp. 283-317, 1996.

Didier Bert, Rachid Echahed, Paul Jacquet, Marie-Laure Potet and Jean-Claude Reynaud.
Spécification, Généricité, Prototypage: Aspects du langage LPG.
In journal of Technique et Science Informatiques 9 vol 14. pp 1097-1129. 1995.