Detecting of timing leaks of programs using parametric timed model checking

Submission deadline 01/09/2026
Tuesday, January 27, 2026
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.