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.

About this position

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:

• BINSEC\autocite{CEAListBINSEC2023}, an open-source platform for

automatic reasoning on safety and security properties at the binary

level (e.g., \autocite{DanielBinsecRelEfficient2020});

• 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/

Funding category:

Autres financements