Advisors: David Monniaux and Bruno Ferres
Context
Fault injections (using laser beams, EM injection, or even purely software attacks) are a real threat against all embedded systems. Even though counter-measures exist (either hardware, software, or hybrid) for those faults, it is difficult to add them in the compilation flow of programs. Moreover, the effectiveness of those counter-measures in the generated code is a difficult question, particularly when multiple counter-measures can be composed to harden the code against several fault models.
Internship Goal
In this context, we investigate the potential of adding security features in the context of verified compilation (within the CompCert compiler, a compiler where the behavior of the machine code is proved correct with respect to the semantics of the source code). This internship is an great opportunity for students interested in formal methods and compilation to discover how those fields may be applied to improve the security of programs. For further information, please take a look at the attached document. If you are interested in this internship, do not hesitate to contact the advisors.
