Preuve d'équivalence fonctionnelle de programmes binaires pour la cyber-sécurité // Proof of Functional Equivalence of Binary Codes in the Context of Programs Hardening.

cf. summary in english.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

This Ph.D. thesis takes place in the general context of cyber-security
in embedded systems. The research background of this thesis is tied to
the automatic application of counter-measures against so-called physical
attacks: observation attacks (side-channel
attacks\autocite{MangardPoweranalysisattacks2007}) and perturbation
attacks (fault-injection
attacks\autocite{BreierAutomatedMethodsCryptographic2019}).


The goal of this thesis is to bring new formal guarantees about the
functional correctness of the secured programs, i.e., that
non-functional changes (application of counter-measures) do not alter
the functional behaviour of the original program.

The work will be structured around the two following research tools:
1. BINSEC\autocite{CEAListBINSEC2023}, an open-source platform for
automatic reasoning on safety and security properties at the binary
level (e.g., \autocite{DanielBinsecRelEfficient2020});
2. COGITO a compiler toolchain based on LLVM for automated application
of software counter-measures against physical attacks (e.g.,
\autocite{Maskara2020,MorelCodepolymorphismmeets2021}).

We seek to formally demonstrate that an optimized and hardened binary
program is functionnally equivalent to the original, non-hardened one.
To do so, we aim to develop a sound and exhaustive symbolic reasoning
supported by and integrated in the BINSEC platform. The work will
consider COGITO counter-measures of incremental complexity wrt.the
research objectives.

You will be hosted at the CEA in Saclay or Grenoble, in a
multidisciplinary environment including experts in embedded software,
cyber-security, hardware design, and machine learning. Stays at the
DILS at the CEA in Saclay will be planned throughout the three years of
the thesis to collaborate with experts and developers of BINSEC.

The position is fully funded.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2024
WEB : https://binsec.github.io/

Autres financements

Université Grenoble Alpes

217 MSTII - Mathématiques, Sciences et technologies de l'information, Informatique

program analysis, formal methods, symbolic execution.
program analysis, formal methods, symbolic execution.