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
2022 :
Thomas Vigouroux,
Cristian Ene,
David Monniaux, Laurent Mounier, Marie-Laure Potet:
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
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
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.