Research and Development Engineer in Formal Methods

Who we are ?

Télécom Paris, part of the IMT (Institut Mines-Télécom) and a founding member of the Institut Polytechnique de Paris, is one of France's top 6 general engineering schools.

The mainspring of Télécom Paris is to train, imagine and undertake to design digital models, technologies and solutions for a society and economy that respect people and their environment.

Modern distributed systems are increasingly complex, with multiple interconnected components, services, and autonomous agents interacting in dynamic environments. Ensuring their cybersecurity requires analysing both potential attacks and the strategies that defenders can adopt in response. Attackers may exploit sequences of vulnerabilities to compromise a system, while defenders may react through countermeasures such as access restrictions, system reconfigurations, or Moving Target Defense mechanisms. Traditional cybersecurity analysis techniques often focus on identifying vulnerabilities and possible attack paths, with limited support for reasoning about the strategic interactions between attackers and defenders.

The VITAMIN-C (VerIficaTion of A MultI-ageNt system for Cybersecurity) project aims to address these challenges through formal verification. Building on VITAMIN, an existing modular model-checking platform for multi-agent systems, the project develops methods and tools for modelling and verifying cybersecurity properties in distributed and autonomous systems. Attackers and defenders are represented as agents with specific capabilities, objectives, and available actions. Their interactions are analysed using attack graphs, temporal and strategic logics, and model-checking techniques. This approach allows the verification of security properties, such as the preservation of confidentiality and integrity, as well as the synthesis of defensive strategies against known attack scenarios.

A central challenge of the project concerns the scalability of formal verification when applied to realistic cybersecurity scenarios. To address this issue, VITAMIN-C investigates symbolic and abstract model-checking techniques, together with a modular architecture supporting the integration of different verification engines.

Within this context, the R&D engineer will contribute to the design, implementation, and evaluation of formal verification techniques for VITAMIN-C. The work will focus on formal modelling of cybersecurity scenarios, strategic model checking, development and optimisation of verification algorithms, and their integration into the existing platform. The engineer will also participate in experimental evaluations using cybersecurity benchmarks and industrial use cases, contributing to the development of a practical verification tool.

Your main responsibilities will include :

• Carry out R&D work in formal methods and cybersecurity verification

• Contribute to the research profile of Télécom Paris and Institut Mines-Télécom