Description
Date depot: 6 avril 2023
Titre: Formal leakage-free analysis and modelling of microarchitectural sources of leakage
Directrice de thèse:
Emmanuelle ENCRENAZ (LIP6)
Encadrant :
Quentin MEUNIER (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Systèmes et architectures intégrés matériel-logiciel
Resumé: Physical attacks named side channel attacks (SCA) consist in measuring physical quantities of a computing system (power consumption, electromagnetic radiations) during the execution of a cryptographic algorithm, and using them in order to retrieve the encryption key [1, 2]. These attacks target more specifically embedded devices, such as payment cards, for which the encryption key must not be known to the user.
SCA have grown in popularity since the early 2000s. To limit their impact, two main hardening techniques have appeared: hiding [3] and masking [4]. The latter consists in breaking down the secret into several parts (shares) using masks (variables following a uniform random distribution between several executions), so that only the recomposition of the different shares makes it possible to deduce information on the original secret. The algorithm must be modified to apply an independent treatment to each of the shares.
Various works have studied how to automate the security proofs of such masking schemes [6, 7, 8, 9]: the goal of resulting tools is, from a description of the program, to verify for all the expressions manipulated by the program that their distributions are statistically independent of the secrets (typically the encryption key). Such security proofs are based on a leakage model (e.g value-based leakage model) that abstracts the real leakage. Moreover they are often applied on a high level representation of a masked program that is too far from the compiled code running on a given hardware target. To guarantee the absence of leakage when running a masked code, it is necessary to perform a leakage-free analysis on the assembly code (or binary) of the program with a sufficiently precise model of the processor [5], typically taking into account its micro-architecture and its sources of leakage.
Recently, the framework Armistice [10] has shown the relevance of modelling the processor micro-architecture for the formal verification of masked program, using the Arm Cortex-M3 core as an example. One objective of the thesis will be to extend this work by proposing a modelling methodology starting from an RTL description. Another important part will concern the design or extension of a formal leakage-free analysis, or on how to combine a formal analysis with simulated power traces. The thesis will also include an experimental part in order to validate the different proposals (model and security analysis).
The work of this thesis will be related to the ANR IDROMEL project that has started in 2021. The objectives of this project are to analyze the micro-architectural sources of leakage and to propose different methods and tools to strengthen the software and hardware security of embedded systems against SCA. The consortium brings together Arm France, CEA, IRISA, LAAS and LIP6. The PhD candidate will interact with all partners, in particular with Arm France.