Table of contents

Description

  • Speaker

    Xaver Fabian - CISPA Helmholtz Center for Information Security

Speculative execution improves CPU performance but introduces vulnerabilities, known as Spectre attacks, which exploit microarchitectural side effects to leak sensitive data. Modern processors employ multiple interacting speculation mechanisms, yet existing approaches predominantly analyze them in isolation, which limits both the automated detection of complex leaks and the formal verification of compiler-level countermeasures. This thesis establishes a formal foundation that extends both the detection of speculative leaks and the verification of Spectre defences. For detection, it formalizes novel speculative semantics for stores, indirect jumps and returns, together with a composition framework that combines them to uncover complex, multi-mechanism leaks; these are implemented and evaluated in the Spectector tool. For defence, it develops a secure compilation framework with rigorous lifting conditions that determine when security properties proven against isolated hardware models can be safely transferred to stronger, composed models without new proofs, and applies it to a security analysis of nine Spectre countermeasures in mainstream compilers.

Practical infos

  • Date

    February 12, 2027 (11:00 - 12:00)

  • Location

    IETR - University of Rennes - Campus de BEAULIEU Bâtiment 11D, salle numéro 18
    Locate on OpenStreetMaps

  • Suggest a presentation

    Go to suggestion form

  • Add this presentation to my calendar

  • Video meet

    Access the meeting

Next sessions

  • Onysis: A secure European SoC FPGA 

    • November 13, 2026 (10:00 - 11:00)

    • IETR - University of Rennes - Campus de BEAULIEU - Bâtiment 11D, salle numéro 18

    Speaker : Adrien GRASSEIN - Nanoxplore

    Developed in collaboration with the DGA, the Onysis project introduces a European SoC FPGA designed to embed advanced hardware security features. This presentation will provide an overview of the Onysis architecture, focusing specifically on its native mechanisms to protect critical systems. We will detail the implementation of its integrated security subsystem, covering the secure boot sequence[…]

    • SemSecuElec

  • Using High Level Profiling Data to Early Assess the Fault Tolerance of Complex Digital Components

    • November 13, 2026 (11:00 - 12:00)

    • IETR - University of Rennes - Campus de BEAULIEU - Bâtiment 11D, salle numéro 18

    Speaker : Luc NOIZETTE - Nuclétudes (filiale Ariane group)

    This presentation outlines an innovative methodology for estimating the fault tolerance of complex components based on application profiling obtained using a high-level virtual platform.  A derating factor, derived exclusively from profiling metrics (e.g., lifetime in memory and registers), is calibrated using a reliability dataset collected from a set of benchmarks.  Applying it to test softwares[…]

    • SemSecuElec

    • Fault injection

  • Securing processor's microarchitecture against SCA in a post-quantum cryptography setting

    • February 12, 2027 (10:00 - 11:00)

    • IETR - University of Rennes - Campus de BEAULIEU - Bâtiment 11D, salle numéro 18

    Speaker : Vincent MIGLIORE - LAAS-CNRS

    Hardware microarchitecture is a well-known source of side-channel leakages, providing a notable security reduction of standard cryptographic algorithms (e.g. AES) if not properly addressed by software or hardware. In this talk, we present new design approaches to harden processor's microarchitecture against power-based side-channel attacks, relying on configurable and cascadable building blocks[…]

    • SemSecuElec

    • Side-channel

    • Micro-architectural vulnerabilities

Show previous sessions
Page top