Jonathan Certes

Home / Research

This page is dedicated to my research activity. A brief introduction to my thesis is available here.

Technical insights

Here are some technical details regarding my past research activities:

• Automated formal verification of hardware designs
• Static root of trust on microprocessor ARM Cortex-A9
• Attestation of configuration for ARM cortex-A9 processor

Safety/Security tools

• Abstraction of Verilog HDL at netlist level
• Extension for LTL_Coq library
• Open Hardware Logic Analyser empowered with Verilator

Publications

Formal verification of hardware architectures

• Jonathan Certes, Benoît Morgan, An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs, ERTS 2022

Defensive security research

• Jonathan Certes, Benoit Morgan, Remote attestation of bare-metal microprocessor software: a formally verified security monitor, IWCFS 2021
• Jonathan Certes, Benoît Morgan, Attaque et sécurisation d'un schéma d'attestation à distance vérifié formellement (French), SSTIC 2022
• Jonathan Certes, Benoit Morgan, Attestation à distance de microprocesseurs vérifiée formellement (French), RESSI 2020

Thesis

• Jonathan Certes, Méthodes et modèles pour la vérification formelle de l'attestation à distance sur microprocesseur (French), 2023

Open archive: hal

Recorded presentations

English

• Ph.D defense 2023 (translation)
• THCon 2022: Attacking formally verified hardware monitors
• ERTS 2022: An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs (replay)
• IWCFS 2021: Remote attestation of bare-metal microprocessor software: a formally verified security monitor (replay)

French

• Soutenance de Thèse 2023
• SSTIC 2022: Attaque et sécurisation d'un schéma d'attestation à distance vérifié formellement

---