Publications HAL

Journal articles

2017

titre
A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data
auteur
Frédéric Besson, Sandrine Blazy, Pierre Wilke
article
Journal of Automated Reasoning, Springer Verlag, 2017, pp.1-48. 〈10.1007/s10817-017-9439-z〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01656895/file/jar-besson-blazy-wilke.pdf BibTex

2016

titre
Using JavaScript Monitoring to Prevent Device Fingerprinting
auteur
Nataliia Bielova, Frédéric Besson, Thomas Jensen
article
ERCIM News, ERCIM, 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01353997/file/final.pdf BibTex

2010

titre
Verifying Resource Access Control on Mobile Interactive Devices
auteur
Frédéric Besson, Guillaume Dufay, Thomas Jensen, David Pichardie
article
Journal of Computer Security, IOS Press, 2010, 18 (6), pp.971-998
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00537821/file/jcs.pdf BibTex

Conference papers

2018

titre
Modular Software Fault Isolation as Abstract Interpretation
auteur
Frédéric Besson, Thomas Jensen, Julien Lepiller
article
SAS 2018 - 25th International Static Analysis Symposium, Aug 2018, Freiburg, Germany. Springer, 11002, pp.166-186, LNCS. 〈10.1007/978-3-319-99725-4_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01894116/file/SAS-2018.pdf BibTex

2017

titre
CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics
auteur
Frédéric Besson, Sandrine Blazy, Pierre Wilke
article
ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. Springer, LNCS, 10499, pp.81-97, ITP 2017: Interactive Theorem Proving. 〈http://itp2017.cic.unb.br/〉. 〈10.1007/978-3-319-66107-0_6〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01656875/file/compcerts.pdf BibTex
titre
Confusion de Type en C++: État de l'Art et Difficultés de Détection
auteur
Florent Saudel, Sandrine Blazy, Frédéric Besson
article
RESSI 2017 - Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information , May 2017, Grenoble/Autrans, France. pp.1-5, 2017, 〈https://ressi2017.sciencesconf.org/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01656979/file/ressi.pdf BibTex

2016

titre
Hybrid Monitoring of Attacker Knowledge
auteur
Frédéric Besson, Nataliia Bielova, Thomas Jensen
article
29th IEEE Computer Security Foundations Symposium, 2016, Lisboa, Portugal
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01310572/file/hybrid_monitoring_of_attacker_knowledge.pdf BibTex

2015

titre
A Concrete Memory Model for CompCert
auteur
Frédéric Besson, Sandrine Blazy, Pierre Wilke
article
Springer. ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. Lecture Notes in Computer Science (LNCS) (9236), pp.67-83, 2015, nteractive Theorem Proving. 〈10.1007/978-3-319-22102-1_5〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01194549/file/paper.pdf BibTex

2014

titre
Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach
auteur
Frédéric Besson, Nataliia Bielova, Thomas Jensen
article
Nordic Conference on Secure IT Systems (NordSec 2014), Oct 2014, Tromsø, Norway. 2014, 〈10.1007/978-3-319-11599-3_11〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081037/file/enforcing_abstract.pdf BibTex
titre
A Precise and Abstract Memory Model for C Using Symbolic Values
auteur
Frédéric Besson, Sandrine Blazy, Pierre Wilke
article
12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. Springer, 8858, pp.449 - 468, 2014, LNCS. 〈10.1007/978-3-319-12736-1_24〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093312/file/symbolic.pdf BibTex
titre
SawjaCard: A Static Analysis Tool for Certifying Java Card Applications
auteur
Frédéric Besson, Thomas Jensen, Pierre Vittet
article
21st International Static Analysis Symposium (SAS 2014), 2014, Munich, Germany. Springer, 8858, pp.51 - 67, 2014, 〈10.1007/978-3-319-10936-7_4〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093327/file/sawjacard.pdf BibTex

2013

titre
Result Certification of Static Program Analysers with Automated Theorem Provers
auteur
Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen
article
VSTTE 2013 - Fifth Working Conference on Verified Software: Theories, Tools and Experiments, 2013, Atherthon, United States. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00924167/file/result_certification_of_static_program_analysers_with_automated_theorem_provers.pdf BibTex
titre
Hybrid Information Flow Monitoring Against Web Tracking
auteur
Frédéric Besson, Nataliia Bielova, Thomas Jensen
article
CSF - 2013 IEEE 26th Computer Security Foundations Symposium, 2013, New Orleans, United States. 2013, 〈10.1109/CSF.2013.23〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00924138/file/hybrid_information_flow_monitoring_against_web_tracking.pdf BibTex

2011

titre
A Nelson-Oppen based Proof System using Theory Specific Proof Systems
auteur
Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00677193/file/paper5.pdf BibTex
titre
A Flexible Proof Format for SMT: a Proposal
auteur
Frédéric Besson, Pascal Fontaine, Laurent Théry
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011, 〈http://pxtp2011.loria.fr〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642544/file/paper3.pdf BibTex
titre
Modular SMT Proofs for Fast Reflexive Checking inside Coq
auteur
Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
article
First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00646960/file/CPP11.pdf BibTex

2010

titre
Certified Result Checking for Polyhedral Analysis of Bytecode Programs
auteur
Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin
article
The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany. Springer-Verlag, 2010, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00537816/file/main.pdf BibTex
titre
On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver
auteur
Frédéric Besson
article
8th International Workshop on Satisfiability Modulo Theories, 2010, Edinburgh, United Kingdom. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00517308/file/floating_point_simplex.pdf BibTex
titre
Sawja: Static Analysis Workshop for Java
auteur
Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
article
Beckert, Bernhard and Marché, Claude. The International Conference on Formal Verification of Object-Oriented Software, 2010, Paris, France. Springer-Verlag, 2010.13, pp.253--267, 2010, Lecture Notes in Computer Science. 〈http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00504047/file/main.pdf BibTex

2009

titre
Certified Static Analysis by Abstract Interpretation
auteur
Frédéric Besson, David Cachera, Thomas Jensen, David Pichardie
article
Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. Springer-Verlag, 5705, pp.223-257, 2009, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00538753/file/main.pdf BibTex
titre
CPA beats oo-CFA
auteur
Frédéric Besson
article
FTfJP '09 - Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, 2009, Genova, Italy. 2009, 〈10.1145/1557898.1557905〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00780389/file/CPA_beats_CFA.pdf BibTex

2008

titre
Computing stack maps with interfaces
auteur
Frédéric Besson, Thomas Jensen, Tiphaine Turpin
article
ECOOP'08, 2008, Paphos, Cyprus. 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00332526/file/BessonJensenTurpinEcoop2008.pdf BibTex

1999

titre
Polyhedral Analysis for Synchronous Languages
auteur
Frédéric Besson, Thomas Jensen, Jean-Pierre Talpin
article
6th International Symposium on Static Analysis (SAS'99), Sep 1999, Venice, Italy. Springer-Verlag, pp.51-68, 1999, LNCS vol. 1694
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00544493/file/CONCUR99-besson.pdf BibTex

Other publications

2006

titre
A Formal Model of Access Control for Mobile Interactive Devices
auteur
Frédéric Besson, Guillaume Dufay, Thomas Jensen
article
2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00083453/file/main.pdf BibTex

Reports

2014

titre
Enforcing Browser Anonymity with Quantitative Information Flow
auteur
Frédéric Besson, Nataliia Bielova, Thomas Jensen
article
[Research Report] RR-8532, INRIA. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00984654/file/RR-8532.pdf BibTex

2009

titre
Computing the Least Fix-point Semantics of Definite Logic Programs Using BDDs
auteur
Frédéric Besson, Thomas Jensen, Tiphaine Turpin
article
[Research Report] PI 1939, 2009, pp.25
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00433820/file/PI-1939.pdf BibTex

2008

titre
Computing stack maps with interfaces
auteur
Frédéric Besson, Thomas Jensen, Tiphaine Turpin
article
[Research Report] PI 1879, 2008, pp.39
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00200724/file/PI-1879-V2.pdf BibTex

2007

titre
Result certification for relational program analysis
auteur
Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin
article
[Research Report] RR-6333, INRIA. 2007, pp.32
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00166930/file/RR-6333.pdf BibTex

2005

titre
A PCC Architecture based on Certified Abstract Interpretation
auteur
Frédéric Besson, Thomas Jensen, David Pichardie
article
[Research Report] PI 1764, 2005, pp.35
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000866/file/PI-1764.pdf BibTex
titre
A PCC Architecture based on Certified Abstract Interpretation
auteur
Frédéric Besson, Thomas Jensen, David Pichardie
article
[Research Report] RR-5751, INRIA. 2005, pp.35
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070268/file/RR-5751.pdf BibTex