General information
Organisation
The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development and innovation in four main areas :
• defence and security,
• nuclear energy (fission and fusion),
• technological research for industry,
• fundamental research in the physical sciences and life sciences.
Drawing on its widely acknowledged expertise, and thanks to its 16000 technicians, engineers, researchers and staff, the CEA actively participates in collaborative projects with a large number of academic and industrial partners.
The CEA is established in ten centers spread throughout France
Reference
SL-DRT-24-0540
Direction
DRT
Thesis topic details
Category
Technological challenges
Thesis topics
Proof of functional equivalence of binary codes in the context of embedded program hardening
Contract
Thèse
Job description
The general context of this thesis is the cyber-security of embedded
systems. The research background of this thesis is tied to the
automatic application of counter-measures against the so-called physical
attacks, which encompass observation attacks (side-channel attacks) and
perturbation attacks (fault-injection attacks).
The CEA List is working on COGITO, a compiler toolchain based on LLVM
for the automatic application of software counter-measures against
physical attacks. Given a source-level implementation of an unprotected
program, our toolchain produces an optimised binary program including
targeted counter-measures, such that the compiled program is hardened
against a specified threat model. Two key points are today crucial to
trust the compiled programs:
1. the proof of robustness of programs produced by our toolchain,
2. the proof that adding counter-measures does not alter the
functionality of the target programs.
This thesis will target the second point: bringing formal guarantees
about the functional correctness of the secured programs. We will use
sound and exhaustive symbolic reasoning, supported by BINSEC
(<https://binsec.github.io>). BINSEC is an open-source toolset
developed at CEA List to help improve software security at the binary
level. It relies on cutting-edge research in binary code analysis, at
the intersection of formal methods, program analysis, security and
software engineering.
The PhD thesis will be hosted at the CEA in Saclay, within the BINSEC team.
Short-term stays
at CEA Grenoble will be planned throughout the three
years of the thesis to collaborate with experts and developers of
COGITO.
University / doctoral school
Mathématiques, Sciences et Technologies de l’Information, Informatique (MSTII)
Université Grenoble Alpes
Thesis topic location
Site
Saclay
Requester
Position start date
01/10/2024
Person to be contacted by the applicant
RECOULES Frédéric frederic.recoules@cea.fr
CEA
DRT/DILS//LSL
Tutor / Responsible thesis director
COUROUSSE Damien damien.courousse@cea.fr
CEA
DRT/DSCIN/DSCIN/LFIM
Commissariat à l’énergie atomique et aux énergies alternatives
MINATEC Campus | 17 rue des Martyrs | 38054 Grenoble Cedex 9
+33 (0)4 38 78 04 66
En savoir plus