Sébastien BARDIN Researcher in Computer Science
	Education Ph.D. in Computer Science, ENS Cachan (France), 2005 M.S. in Computer Science, ENSIIE (France), 2002 Current position Senior Researcher, CEA Fellow Software Safety and Security Lab., Commissariat à l'Energie Atomique (CEA),  Paris-Saclay, France Contact information Email    : sebastien.bardin(at)cea.fr Phone   : +33 (0)1 69 08 54 16 Address: CEA NanoInnov, Palaiseau, France

• Expert in Formal Methods, Cybersecurity and Quantum Computing
• [from 2012] Founder and lead of the BINSEC group on binary-level security analysis
  
• [from 2020] Founder and lead of the QBricks group on quantum program verification
• [2021 - 2023] In charge of the Software Quantum Program of the CEA LIST Institute

Research Interests

• Main areas: formal methods & program analysis, logic & constraint solving, software security, software engineering, quantum programming
  
• Techniques:  symbolic execution, abstract interpretation, software model checking, SMT solving, Constraint Programming
  
• Application domains:  cybersecurity, embedded systems, critical systems, software safety, software productivity

Binary-level security analysis

• Develop and take advantage of binary-level program analysis techniques for security analysis, especially vulnerability detection and deobfuscation
• Some results:  ESOP 2023, IJCAI 2022, NDSS 2021, ICSE 2021, S&P 2020, RAID 2020, BlackHat 2020, ASE 2019, ACSAC 2019, CAV 2018, LPAR 2018, DIMVA 2018, S&P 2017, BlackHat Europe 2016, ISSTA 2016
  
• The BINSEC platform     (also: the old page of the ANR project)

[past] Automatic and efficient software testing: a coverage-objective specification language plus automated analyses

• Develop a generic and efficient way to automate the testing process for most code-coverage criteria
  
• results: see our papers at SCP 2021, ICSE 2018, ICST 2017, ICST 2015, ICST 2014, TAP 2014
  
• Prototype: the Frama-C plugin LTest (open source, github)
  

[past] Constraint solving based solvers for security- and verification- oriented problems

• Combine Constraint Programming and SMT solving techniques for attacking hard-to-solve formulas from industrial problems. We are especially looking for the theories of bitvectors and floats
  
• recent results: see our papers at CAV 2018, LPAR 2018, IJCAI 2017, CPAIOR 2017
  
• SOPRANO project      
  

Publications

• Publications
  
• DBLP
• Google Scholar

Service & distinctions

• Expert in Cybersecurity, Formal Methods and Quantum Computing
• [from 2012] Founder and lead of the BINSEC group on binary-level security analysis
  
• [from 2020] Founder and lead of the QBricks group on quantum program verification
• [2021 - 2023] Head of the Software Quantum Program of the CEA LIST institute

• Personal awards
• [from 2021] CEA Fellow
  
• [from 2021] ACM Senior Member

• Paper awards
• ICSE 2021 ACM SIGSOFT Distinguished Paper Award
• RTAS 2021 best paper award
• CAV 2021  selected paper
  

• Student awards
• 2022: GDR Sécurité PhD award, 2nd place for Lesly-Ann Daniel 
  
• 2022: GDR GPL PhD award, 2nd place for Frédéric Recoules
• 2022: Ecole Polytechnique research internship award for Matthéo Vergnolle (intern)  
  
• 2021: Ecole Polytechnique research internship award for Stéphane Latil (intern)
  
• 2021: GDR GPL PhD Award, 1st place for Benjamin Farinier
  
• 2020: L'Oréal -Unesco "For Women in Science (young talents)" 2020 Research Award for Lesly-Ann Daniel  

• [from 2017] board member of GDR Sécurité  (CNRS working group for cybersecurity)  
• [from 2017] co-chair of  working group  Formal Methods and Security of GDR Sécurité
  

• [from 2017] board member of working group  Software Security of GDR Sécurité
• [from 2018] board member of RESSI (French network on research and teaching in cybersecurity)
  
• [from 2018] steering committee of the DIMVA Conference on Detection of Intrusions and Malware & Vulnerability Assessment
• [from 2020] steering committee of the SAD workshop on Software Attack and Defense 
• [2018-2019] external expert of the SecUnity initiative
  
• [2017-2018] member of the French-German working group on cybersecurity
  
• [from 2017] steering committe of the CSTVA workshop (Constraints for Testing, Verification and Analysis)

• [2023] CAV 2023 (sponsor co-chair), FIC 2023 (scientific program chair), French Meeting on Formal Methods for Security
• [2022] Dagstuhl Seminar "Machine Learning and Logical Reasoning: The New Frontier", French Meeting on Formal Methods for Security
• [2021] Cyber in Saclay Winter School, French Meeting on Formal Methods for Security
  
• [2020] Cyber in Saclay Winter School (postponed 2021), French Meeting on Formal Methods for Security
  
• [2019] Dagstuhl Seminar on Next Challenges in Constraint Solving, SSPREW workshop, French Meeting on Formal Methods for Security,  GDR Sécurité Annual Meeting
• [2018] DIMVA 2018, ESSOS 2018, SSPREW workshop, first French Meeting on Formal Methods for Security, GDR Sécurité Annual Meeting, first French Obfuscation Day
• [2017] ISSISP 2017 Summer School, CSTVA 2017
  

• [2024] ICSE 2024
  
• [2023] AAAI 2023, CAV 2023, Usenix Security 2023, ISSTA 2023, CSF 2023, ICST 2023, RTAS 2023, DIMVA 2023, ARES 2023, SecDev 2023, PrisC 2023
  
• [2022] CAV 2022, ESEC/FSE 2022, AAAI 2022, ISSTA 2022, RTAS 2022, ESORICS 2022, ACSAC 2022, DIMVA 2022, CP 2022, SAS 2022, AITest 2022, SecDev 2022
  
• [2021] CP 2021, ISSTA 2021, ESORICS 2021, ACSAC 2021, DIMVA 2021, SAC 2021, BAR 2021, AITest 2021,  SecureComm 2021, CYBER 2021, FPS 2021, CRISIS 2021, VALID 2021, SecurWare 2021
  
• [2020] ACSAC 2020, CP 2020, DIMVA 2020, AITest 2020, SAC 2020, BAR 2020, MLBA 2020, CRISIS 2020, SEAD 2020, VALIDS 2020
  
• [2019] CP 2019, AITest 2019, SAC 2019, VALIDS 2019, SEAD 2019, SYNASC 2019, Spring School FORMAL 2019
• [2018] CP 2018, SAC 2018
• [2017] CP 2017, SSPREW 2017, Malware 2017, VALIDS 2017
  

News

• Very happy to be promoted as a CEA Fellow
  
• Very happy to be nominated as an ACM Senior Member
  

• [**NEW**] Our RAID 2020 paper cited in ACM Queue  as highly inspiring for fuzzing research 
• Our RTAS 2021 paper gets a Best Paper Award
  
• Our ICSE 2021 paper gets an ACM SIGSOFT Distinguished Paper Award
• Our CAV 2021 paper is selected for inclusion in a journal edition

• [**NEW**] Matthéo Vergnolle (intern) won a research internship award from Ecole Polytechnique
  
• [**NEW**] Lesly-Ann Daniel (PhD student) ranks 2nd at GDR Sécurité 2022 PhD Award (all fields of cybersecurity: network, crypto, hardware, software & system, etc.). 
  
• [**NEW**] Frédéric Recoules (PhD student) ranks 2nd at GDR GPL 2022 PhD Award (all fields of software engineering, programming languages and formal methods). 
• Stéphane Latil (intern) won a research internship award from Ecole Polytechnique
  
• Benjamin Farinier (PhD student) won the GDR GPL 2021 Best Thesis Award (software engineering, programmaing languages and formal methods).
  
• Lesly-Ann Daniel (PhD student) won a L'Oréal -Unesco "For Women in Science (young talents)" 2020 Research Award. 
  

• [**NEW**] Guillaume Girol got his PhD, on robust reachability and robust symbolic execution. Congratulations!!
  
• Yaëlle Vinçont just got her PhD, on the combination of symbolic execution and fuzzing. Congratulations!!
  
• Lesly-Ann Daniel just got her PhD, on relational symbolic execution for binary-level security purposes. Congratulations!!
  
• Frédéric Recoules just got his PhD, on the analysis of inline assembly code. Congratulations!!
  
• Manh Dung Nguyen just got his PhD, on directed fuzzing for complex vulnerabilities. Congratulations!!
  

• [**NEW**] Our work on adversarial reachability and adversarial symbolic execution is accepted @ ESOP 2023
  
• [**NEW**] Our work on combining fuzzing with fine-grain coverage objectives through labels is accepted @ ACM TOSEM
  

• [**NEW**] Our journal article extending our previous S&P 2020 work on constant-time analysis is accepted @ Transations On Privacy and Security
  
• [**NEW**] Our journal article extending our previous CAV 2021 work on robust reachability is accepted @ Formal Methods in System Design
• [**NEW**] Our work on achieving black-box specification inference from code through AI techniques is accepted @ IJCAI 2022
  
• [**NEW**] Our work on finer coverage metrics for fuzzing is accepted @Fuzzing workshop@NDSS 2022

• [2021] Our experience report on the evaluation of the BINSEC/Haunted paper (NDSS 2021) is on its way to the proceedings of @ LASER 2021
• [2021] Our work on tight integration between fuzzing and symbolic execution is accepted @ FPS 2021
• [2021] Our work on blackbox ai-based code deobfuscation is accepted @ CCS 2021
• [2021] Our work on software-based hardware abstraction for deobfuscation is accepted @ SECrypt 2021
• [2021] Our work on robust reachability and its implications for security and symbolic execution is accepted @ CAV 2021 [selected paper]
  
• [2021] A journal article giving a comprehensive overview of our work on automated white-box testing is accepted @ Journal of Science Computer Programming
  
• [2021] Our work on automated binary-level security verification of embedded kernels is accepted @ RTAS 2021  [best paper award]
  
• [2021] Our work on binary-level toolchain provenance identification by machine learning is accepted @ SANER 2021
• [2021] Our work on automated verification of speculative constant-time attacks is accepted @ NDSS 2021 
  
• [2021] Our work on deductive verification of circuit-building quantum programs is accepted @ ESOP 2021
  
• [2021] Our work on automatically detecting and patching bugs in inline assembly code is accepted @ ICSE 2021  [distinguished paper award]
• [2020] Our talk on "About Directed Fuzzing and Use-After-Free: How to Find Complex & Silent Bugs?" is accepted @ Black Hat USA 2020
• [2020] Our work on efficient bounded verification of constant-time property for cryptographic primitives is accepted @ S&P 2020
• [2020] Our work on directed fuzzing for UAF vulnerabilities is accepted @ RAID 2020
• [2019] Our work on verification-oriented decompilation of inline assembly is accepted @ ASE 2019
• [2019] Our wok on software protection with dedicated anti-symbolic analysis is accepted @ ACSAC 2019
• [2019] SecUnity roadmap on Cybersecurity Research: Challenges and Course of Action
• [2018] Our work on efficient reasoning for the theory of arrays is accepted @ LPAR 2018
• [2018] Presentation of our work on model generation over quantified formulas @ CAV 2018
• [2018] Presentation of our work on symbolic devirtualization @ DIMVA 2018
• [2018] Presentation of our work on automatic detection of infeasible test objectives @ ICSE 2018
• [2017] Presentation of our work on deobfuscation through backward-bounded DSE  @ S&P 2017 
  

• [upcoming] Annual Meeting of the French Research Network on Cybersecurity JN GDR Sécurité 2023 [board member] (June 26-28, 2023)
  
• [upcoming] The 35th International Conference on Computer-aided Verification CAV 2023 [sponsor co-chair, pc member] (July 17-22, 2023)
  
• [upcoming] Scientific masterclasses @ Forum International de la Cybersécurité FIC 2023 [program chair]
  
• [upcoming] Rendez-Vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information RESSI 2023 [board member] (May 10-12, 2023) 
• [upcoming] The 6th French meeting on Formal Methods and Security Working Group [steering board] (March 28-30, 2023)
  

• [2022] Rendez-Vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information RESSI 2022 [board member] (May 10-12, 2022) 
• [2022] The 5th French meeting on Formal Methods and Security Working Group [general co-chair]
• [2022] Dagstuhl Seminar "Machine Learning and Logical Reasoning: The New Frontier" [co-organizer]

• [2021] The 4th French meeting on Formal Methods and Security Working Group [general co-chair]
  
• [2021] The 5th GDR Winter School on Cybersecurity  Cyber in Saclay [general co-chair]
  
• [2020] Rendez-Vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information RESSI 2020 [board member] (December 16-18, 2020) 
• [2020] The 3rd French meeting on Formal Methods for Security [co-organizer] (January 30, 2020)
• [2019] The 9th Software Security, Protection, and Reverse Engineering Workshop SSPREW 2019 [general chair]
• [2019] The annual meeting of the French GDR Cyber-Security [general co-chair]   (June 12-14, 2019)
• [2019] The Digicosme Spring School on Formal Methods and Machine Learning ForMal 2019 [scientific committee] (June 4-7, 2019)
• [2019]  Rendez-Vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information RESSI 2019 [board member] (May 15-17, 2019)
• [2019] The 2nd French meeting on Formal Methods for Security [co-organizer] (March 18, 2019)
  
• [2019] Dagstuhl seminar on  Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving [co-organizer]
• [2018] The 1st French meeting on Code and Data Protection, Obfuscation and White-box Cryptography [co-organizer] (December 13, 2018)
  
• [2018] The 8th Software Security, Protection, and Reverse Engineering Workshop SSPREW 2018 [general chair]
• [2018] The 15th Conference on Detection of Intrusions and Malware & Vulnerability Assessment DIMVA 2018 [general co-chair]
  
• [2018] The 9th International Symposium on Engineering Secure Software and Systems ESSoS 2018 [local chair]
• [2018] The annual meeting of the French GDR "Cyber-Security", May 30th - June 1st  [general co-chair]
• [2017] International Summer School on Information Security and Protection ISSISP 2017 @ Gif-sur-Yvettes, Paris, France  [general co-chair]

• [upcoming] Keynote talk @ GDR GPL 2023
  
• [upcoming] Dagstuhl seminar on Vulnerability analysis [invitee]
  
• [2023] Talk on robust reachability and robust symbolic execution @ Meta
  
• [2023] Talk on BINSEC @ Thales
  
• [2023] Talk on side-channel analysis @ ARM France
  

• [2022] Talk entitled From white-box to black-box reverse attacks @ French - Japaneese meeting on Cybersecurity
  
• [2022] Invited talk entitled Five Shades of Symbolic Execution for Vulnerability Hunting    @ Klee workshop 2022
  
• [2022] Master Class on advanced obfuscation - deobfuscation techniques @ Forum International de la cybersécurité
  
• [2022] Dagstuhl seminar on Machine Learning and Logical Reasoning [organizer]
  
• [2022] Talk on binary-level security analysis @ Telecom Paris
  
• [2022] Talk on automated vulnerability hunting @ TII
  
• [2022] Talk on binary-level security analysis @ Huawei Germany
  
• [2022] Talk on binary-level security analysis @ Qualcomm San Diego
  

• [2021] Talk @ the Facebook TAV symposium 2021
• [2021] Talk on formal methods for binary-level security @ seminar DGA / Inria SoSySec
  
• [2021] Talk on formal methods for binary-level security @ ENS Paris-Saclay
  
• [2021] Invited talk @ SOAP 2021
  
• [2021] Talk @ Quantum Business Europe about Quantum Software and Program Analysis
  
• [2020] Invited talk @  The Scientific Day on "Security and Safety of Embedded Systems" by GDR SOC2, IRT St Exupéry, IRT NanoElec and GDR Sécurité Informatique
• [2020] Lecture and talk on automated program analysis, testing and security @ Imperial College
  
• [2020] Talk on formal methods for binary-level security @ Université Grenoble Alpes
  
• [2020] Master Class on advanced cyber-reasoning systems @Forum International de la Cybersecurté 2020
• [2019]  Dagstuhl seminar on Software Protection Decision Support and Evaluation Methodologies [invitee]
• [2019]  Talk @ Workshop on Machine Learning & Security (Beijing, China)
  
• [2019]  Lecture @ International Summer School on Information Security and Protection ISSISP 2019
  
• [2019]  Talk  @  5th France-Japan Cybersecurity Workshop
• [2019] Invited talk @ University South California
• [2018] Invited talk @ journée des GT Sécurité Réseaux et Logiciels
  
• [2018] Dagstuhl seminar on Quantum Programming Languages [invitee]
• [2018] Talk on binary-level program analysis @ Eurecom
• [2018] Talk on binary-level program analysis @ Digicosme Day 2018
• [2018] Talk on binary-level program analysis @ IMDEA
  
• [2018] Invited tutorial on  automatic testing for advanced coverage criteria @ TAP 2018
  
• [2018] Talk on model generation over quantified formulas @AFADL 2018
  
• [2018] Talk on deobfuscation and malware analysis@ 4th Franco-Japanese Cybersecurity Workshop
• [2018] Talk on efficient symbolic execution for advanced coverage criteria  @ Klee Workshop 2018
  
• [2018]  Nii Shonan Meeting on Intensional and extensional aspects of computation: From computability and complexity to program analysis and security  [invitee]
• [2017] Tutorial on binary-level semantic program analysis for security @ ACSAC 2017
  
• [2017] Invited talk on symbolic deobfuscation @ GreHack 2017 security conference
  
• [2017] Dagstuhl seminar on malware analysis [invitee]
  
• [2017] Invited talk @ journées du GDR Sécurité
• [2017] Talk on binary-level formal methods @ ENS Paris-Saclay
  

Projects and grants

Current

• ANR TAVA (2021-2025) [automated vulnerability analysis] [project leader]    
• CEA, UGA, Amossys
  
• FUI Caesar (2020-2023) [partner leader]  
• Gatewatcher,  BNP,  Thales, CEA, CyberTest, Amossys
  
• H2020 C4IIOT (2020-2024) 
  
• H2020 IRIS (2021-2024) [partner leader] 
  
• Carnot Flexsecurity (2021-2024) [automated code securization] [project leader]  
• Carnot  QStack (2021-2024) [quantum software]  [project leader] 
  
• ANR  SoftQPro  (2017-2021) [optimization of quantum programs]

Some past projects

• Project ANR BINSEC (2013-2017) [binary-level security analysis] [project leader]    
• CEA, IRISA, LORIA, VERIMAG, Airbus
  
• Project ANR SOPRANO (2015-2018) [combination of solvers for verification]
• CEA, INRIA, Uni. Paris-Sud, AdaCore, OCaml Pro
• Project DGA SASSE (2013-2016) [partner leader]  
• AMOSSYS, CEA
• Project ANR BINCOA (2008-2012) [project leader]    
• CEA, LABRI, Uni. Paris-Diderot, EDF, Trusted Lab
  

Software

• BINSEC                            (since 2012)   [binary-level program analysis]
• QBricks                             (since 2021)   [formal verification of quantum programs]

• [old] Frama-C/LTest          (2014-2021)   [automated testing of C programs for advanced coverage criteria]
• [old] OSMOSE                  (2006-2011)  [automatic executable testing]
• [old] FAST and FASTeR  (2002-2006)  [counter system model checking]

PhD students and postdocs

Current PhD students

• Guilhem Lacombe [2021-...] Bug prioritization
  
• Charles Babu [2020-...] Formal methods and Machine Learning
  
• Soline Ducoussot [2020-...] Attackers in code analysis
  
• Tristan Benoit [2019-...] Machine learnng and binary code analysis
  
• Grégoire Menguy [2019-...] Code contract inference
  

Current Postdoc

• Raounak Benabidallah [2021-...]  security bug prioritization
  

Happily graduated PhD students

• Guillaume Girol [2019-2022] Robust reachability for code-level security analysis
  
• Yaëlle Vinçont [2017-2021] Smart fuzing
• Lesly-Ann Daniel [2018-2021] Software analysis of non-interference properties
• Frédéric Recoules [2017-2021] Formal analysis of inline assembly code
• Manh Dung Nguyen [2017-2021] Advanced vulnerability analysis
• Benjamin Farinier [2015-2020] Decision Procedures for Vulnerability Analysis
  
• Jonathan Salwan [2015-2020] Symbolic execution for deobfuscation in an industrial setting
• Adel Djoudi [2013-2016]  Safe static analysis  of executables
  
• Robin David [2013-2016] Automatic analysis of obfuscated executables

Former postdoc

• Salwa Souaf [2021-2023]  binary-level program securization
• Christophe Chareton [2018-2019] Formal methods for quantum programs
• Michael Marcozzi [2015-2017]  Hyperproperty testing
  
• Mickaël Delahaye [2014-2015] A unified framework for automatic white-box testing
  

Postdocs, PhDs and trainee proposals

Teaching [partly in French]

Current

• Cybersecurity -- 21h, ENSTA
  

• Software model checking -- 10h, Uni. Paris Saclay
• Formal methods and software testing  -- 20h, INSA Centre-Val de Loire
• Basis of model checking  -- 15h, École Polytechnique & ENSTA
• Software testing -- 40h, Uni. Paris Diderot
• Software testing and symbolic execution -- 20h, Uni. Strasbourg
• Quick introduction to numerical analysis, algorithmic and Maple 40h -- Classes Préparatoires
  

Other stuff [partly in French]

• How to reach my lab
• Infos sur le séminaire du CEA/LSL
  
• Conseils aux (futurs) thésards 
• My LinkedIn page