Detecting of timing leaks of programs using parametric timed model checking

Date limite de soumission 09/01/2026
Mardi 27 janvier 2026
Horaire : 11 h
Dylan Marinho (MoVe, LIP6, Sorbonne Université

In this presentation I will first introduce the theoretical tools for analyzing timing leaks in programs. The notion of opacity was introduced in 2009 by Franck Cassez to assess whether a system can preserve a certain secret against an attacker's (timed) observation. In our work, we focus on an extension of this approach where the attacker's observation is reduced solely to the system's execution time. However, analyzing timed properties of programs is complex : we must consider both the software behavior and the underlying hardware system. We will show how to model these two aspects using timed Petri nets and, as a proof of concept, how to verify security properties in this framework.

Salle 428, couloir 26-00, 4 place Jussieu - 75005 Paris