About us
Espace utilisateur
INSTN offers more than 40 diplomas from operator level to post-graduate degree level. 30% of our students are international students.
Professionnal development
Professionnal development
Find a training course
INSTN delivers off-the-self or tailor-made training courses to support the operational excellence of your talents.
Human capital solutions
At INSTN, we are committed to providing our partners with the best human capital solutions to develop and deliver safe & sustainable projects.
Home   /   Thesis   /   Proof of functional equivalence of binary codes in the context of embedded program hardening

Proof of functional equivalence of binary codes in the context of embedded program hardening

Computer science and software Cyber security : hardware and sofware Engineering sciences Technological challenges


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
(). 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


Département Ingénierie Logiciels et Systèmes (LIST)
Laboratoire pour la Sûreté du Logiciel
Université Grenoble Alpes
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down