Publications HAL de Frédéric,Besson du labo/EPI CELTIQUE; EPICURE

Journal articles

2019

titre
CompCertS: A Memory-Aware Verified C Compiler using a Pointer as Integer Semantics
auteur
Frédéric Besson, Sandrine Blazy, Pierre Wilke
article
Journal of Automated Reasoning, 2019, 63 (2), pp.369-392. ⟨10.1007/s10817-018-9496-y⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02401182/file/compcertS.pdf BibTex
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, 2019, 62 (4), pp.433-480. ⟨10.1007/s10817-017-9439-z⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01656895/file/jar-besson-blazy-wilke.pdf BibTex

2010

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

Conference papers

2023

titre
Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification
auteur
Shenghao Yuan, Benjamin Lion, Frédéric Besson, Jean-Pierre Talpin
article
SETTA 2023 - 9th International Symposium Dependable Software Engineering. Theories, Tools, and Applications, Nov 2023, Nanjing (Chine), China. pp.385-401, ⟨10.1007/978-981-99-8664-4_22⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04376380/file/setta23.pdf BibTex
titre
Type-directed Program Transformation for Constant-Time Enforcement
auteur
Frédéric Besson, Thomas Jensen, Gautier Raimondi
article
PPDP 2023 - International Symposium on Principles and Practice of Declarative Programming, Oct 2023, Lisboa, Portugal. pp.1-13, ⟨10.1145/3610612.3610618⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04268830/file/ppdp2023-6.pdf BibTex
titre
Work in Progress: Thwarting Timing Attacks in Microcontrollers using Fine-grained Hardware Protections
auteur
Nicolas Gaudin, Jean-Loup Hatchikian-Houdot, Frédéric Besson, Pascal Cotret, Gogniat Guy, Guillaume Hiet, Vianney Lapotre, Pierre Wilke
article
2023 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW), Jul 2023, Delft, Netherlands. pp.1-7
Accès au texte intégral et bibtex
https://hal.science/hal-04155139/file/silm2023-cache-protection.pdf BibTex

2022

titre
Femto-Containers: Lightweight Virtualization and Fault Isolation For Small Software Functions on Low-Power IoT Microcontrollers
auteur
Koen Zandberg, Emmanuel Baccelli, Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin
article
Middleware 2022 - 23rd ACM/IFIP International Conference Middleware, Nov 2022, Quebec, Canada. pp.1-12, ⟨10.1145/3528535.3565242⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03888109/file/usenix22.pdf BibTex
titre
End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers
auteur
Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli
article
CAV 2022 - 34th International Conference on Computer Aided Verification, Aug 2022, Haifa, Israel. pp.1-23
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03888082/file/cav22.pdf BibTex

2021

titre
Itauto: An Extensible Intuitionistic SAT Solver
auteur
Frédéric Besson
article
ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Roma, Italy. pp.1-18, ⟨10.4230/LIPIcs.ITP.2021.9⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03508736/file/LIPIcs-ITP-2021-9.pdf BibTex

2019

titre
Information-Flow Preservation in Compiler Optimisations
auteur
Frédéric Besson, Alexandre Dang, Thomas Jensen
article
CSF 2019 - 32nd IEEE Computer Security Foundations Symposium, Jun 2019, Hoboken, United States. pp.1-13
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02180303/file/paper.pdf BibTex
titre
Compiling Sandboxes: Formally Verified Software Fault Isolation
auteur
Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas Jensen, Pierre Wilke
article
ESOP 2019 - 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.499-524, ⟨10.1007/978-3-030-17184-1_18⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02316189/file/esop_papier.pdf BibTex

2018

titre
Securing Compilation Against Memory Probing
auteur
Frédéric Besson, Alexandre Dang, Thomas Jensen
article
PLAS '18 - 13th Workshop on Programming Languages and Analysis for Security, Oct 2018, Toronto, Canada. pp.29-40, ⟨10.1145/3264820.3264822⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01901765/file/main.pdf BibTex
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. pp.166-186, ⟨10.1007/978-3-319-99725-4_12⟩
Accès au texte intégral et bibtex
https://inria.hal.science/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. pp.81-97, ⟨10.1007/978-3-319-66107-0_6⟩
Accès au texte intégral et bibtex
https://inria.hal.science/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
Accès au texte intégral et bibtex
https://inria.hal.science/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://inria.hal.science/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
ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. pp.67-83, ⟨10.1007/978-3-319-22102-1_5⟩
Accès au texte intégral et bibtex
https://inria.hal.science/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. ⟨10.1007/978-3-319-11599-3_11⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01081037/file/enforcing_abstract.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. pp.51 - 67, ⟨10.1007/978-3-319-10936-7_4⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01093327/file/sawjacard.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. pp.449 - 468, ⟨10.1007/978-3-319-12736-1_24⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01093312/file/symbolic.pdf BibTex

2013

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. ⟨10.1109/CSF.2013.23⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00924138/file/hybrid_information_flow_monitoring_against_web_tracking.pdf BibTex
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
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00924167/file/result_certification_of_static_program_analysers_with_automated_theorem_provers.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
First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland
Accès au texte intégral et bibtex
https://inria.hal.science/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
First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland
Accès au texte intégral et bibtex
https://inria.hal.science/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
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00646960/file/CPP11.pdf BibTex

2010

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
The International Conference on Formal Verification of Object-Oriented Software, Beckert, Bernhard and Marché, Claude, 2010, Paris, France. pp.253--267
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00504047/file/main.pdf BibTex
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
Accès au texte intégral et bibtex
https://inria.hal.science/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
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00517308/file/floating_point_simplex.pdf BibTex

2009

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. ⟨10.1145/1557898.1557905⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00780389/file/CPA_beats_CFA.pdf BibTex
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. pp.223-257
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00538753/file/main.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. pp.51-68
Accès au texte intégral et bibtex
https://hal.science/hal-00544493/file/CONCUR99-besson.pdf BibTex

Other publications

2016

titre
Using JavaScript Monitoring to Prevent Device Fingerprinting
auteur
Nataliia Bielova, Frédéric Besson, Thomas Jensen
article
2016
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01353997/file/final.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://inria.hal.science/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://inria.hal.science/inria-00433820/file/PI-1939.pdf BibTex