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

id="offer-description" class="ecl-u-type-heading-2 ecl-u-mt-none ecl-u-mb-l">Offer Description 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 ph