PhD defense Gabriel Ballot: Optimal Active Cyber Defence Strategies based on Multi-Agent System Verification

Tuesday 9 December, 2025, at 15:00 (Paris time) at Télécom Paris

EDF Lab Paris-Saclay, Auditorium (7 Bd Gaspard Monge, F-91120 Palaiseau)
and in videoconferencing

Jury

Frédéric Cuppens, Professeur, Polytechnique Montréal (Reviewer)
Laurent Doyen, Chargé de recherche, CNRS LMF (Reviewer)
Francesco Belardinelli, Senior Lecturer, Imperial College London (Examiner)
Ioana Boureanu, Professor, University of Surrey (Examiner)
Catalin Dima, Professeur, Université Paris-Est Créteil, LACL (Examiner)
Eric Goubault, Professeur, École Polytechnique, LIX (Examiner)
Jean Leneutre, Maître de conférence, Télécom Paris, LTCI (Supervisor)
Vadim Malvone, Maître de conférence, Télécom Paris, LTCI (Co-Supevisor)
Jingxuan Ma, Ingénieur de recherche, EDF R&D, Lab Paris-Saclay (Guest)
Hassane Chraibi, Ingénieur de recherche, EDF R&D, Lab Paris-Saclay (Guest)

Abstract

Many computer and industrial systems are designed at a given point in time using the tools and knowledge available at that time, and then evolve little. This static nature benefits cyber-attackers, who can observe the system over long periods and plan targeted attacks. Active defence mechanisms, such as moving target defences (which frequently reconfigure the system) and adaptive honeypots (which deceive attackers and study their capabilities), help to break this attacker advantage. Current moving target defences often modify the system randomly and at an empirically defined frequency. However, a reconfiguration strategy tailored to system activity would optimise defences by targeting threatened areas and avoiding unnecessary changes. Likewise, a more effective adaptation strategy for honeypots would offer greater realism and allow for a better understanding of the attackers’ objectives and profiles.

Learn more

This thesis proposes tools for modelling systems, attackers, and defenders as games. It builds on contributions in the formal verification of multi-agent systems, notably model checking, to automatically extract adaptation or reconfiguration strategies that satisfy temporal and epistemic objectives. A logical formalism, Capacity Alternating-time Temporal Logic (CapATL), has been developed to reason about systems in which agents have different profiles. It applies to a wide range of systems, profiles, and objectives, with formal guarantees on the resulting strategy. To improve applicability, CapATL has been extended to probabilistic systems (with a prior distribution over profiles) and to systems with imperfect information, requiring the resolution of new theoretical challenges in verification. We show how these formalisms can be used to model a non-trivial adaptive honeypot and to derive a strategy suited to the objectives of realism, security, and attacker profiling.

All the PhD defenses