Embedded systems are increasingly used in critical infrastructures (e.g., energy production networks) and are therefore prime targets for malicious actors. The use of intrusion detection systems (IDS) that dynamically analyze the system's state is becoming necessary to detect an attack before its impacts become harmful.
The IDS that interest us are based on machine learning anomaly detection methods and allow learning the normal behavior of a system and raising an alert at the slightest deviation. However, the learning of normal behavior by the model is done only once beforehand on a static dataset, even though the embedded systems considered can evolve over time with updates affecting their nominal behavior or the addition of new behaviors deemed legitimate.
The subject of this thesis therefore focuses on studying re-learning mechanisms for anomaly detection models to update the model's knowledge of normal behavior without losing information about its prior knowledge. Other learning paradigms, such as reinforcement learning or federated learning, may also be studied to improve the performance of IDS and enable learning from the behavior of multiple systems.

The Information Technology Security Evaluation Facility (ITSEF) conducts activities in the field of security evaluation of electronic systems, embedded software components, either within the framework of certification schemes, for example the one led by the l’Agence Nationale de la Sécurité des Systèmes d’information (ANSSI), or at the direct request of developers.
In the context of security evaluations conducted by the ITSEF, evaluators are required, among other things, to test the resistance of cryptographic mechanisms embedded on smart cards against physical attacks, such as chip tampering attacks or attacks by observing compromising signals. In an application context (banking, healthcare, identity), these mechanisms are used within cryptographic protocols, such as key exchanges or authentications. When a vulnerability is detected in a product, the evaluator must analyze its impact on the protocol. Currently, this analysis relies on the evaluator's expertise, but the use of formal methods would be advantageous for tracing attack paths or for providing greater assurance that the vulnerability will not be exploited.
Initially, this thesis will focus on studying existing verification tools (e.g., Tamarin [1]) in order to test them on the protocols used in commonly evaluated applications. The thesis will then aim to examine the different ways in which a vulnerability can be expressed within the protocol, and to evaluate the tool's ability to formally analyze its impacts by identifying attack paths. Finally, the PhD student will be required to enhance the tool with new components to address the identified needs.
References
[1] Tamarin : https://github.com/tamarin-prover/tamarin-prover

The security assessment of post-quantum cryptography, from the perspective of physical attacks, has been extensively studied in the literature, particularly with regard to the ML-KEM and ML-DSA standards, which are based on Euclidean lattices. Furthermore, in March 2025, the HQC scheme, based on error-correcting codes, was standardized as an alternative key encapsulation mechanism to ML-KEM. Recently, Soft-Analytical Side-Channel Attacks (SASCA) have been used on a wide variety of algorithms to combine information related to intermediate variables in order to trace back to the secret, providing a form of “correction” to the uncertainty associated with profiled attacks. SASCA is based on probabilistic models called “factor graphs,” to which a “belief propagation” algorithm is applied. In the case of attacks on post-quantum cryptosystems, it is theoretically possible to use the underlying mathematical structure to process the output of a SASCA attack in the form of cryptanalysis. This has been demonstrated, for example, on ML-KEM. The objective of this thesis is to develop a methodology and the necessary tools for cryptanalysis and residual complexity calculation for cryptography based on error-correcting codes. These tools will need to take into account information (“hints”) obtained from a physical attack. A second part of the thesis will be to study the impact that this type of tool can have on the design of countermeasures.