2023
Guilhem Lacombe, David Feliot, Etienne Boespflug Marie-Laure Potet
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.