[Master] Proved-Secure Compilation for RISC-V Processor


Advisors: David Monniaux and Bruno Ferres


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.

Attached documents

Internship Proposal

24 October 2023
info document : PDF
137.9 KiB

Contact | Site Map | Site powered by SPIP 4.2.8 + AHUNTSIC [CC License]

info visites 3864012