Advisors: David Monniaux, Sylvain Boulmé
CompCert is a compiler for the C programming language for the assembly languages of several processor architectures. In contrast to compilers such as Visual C++, gcc, or LLVM, its compilation phases are proved mathematically correct, and thus the compiled program always matches the source program. Other compilers may contain bugs that in some cases result in incorrect code being generated. The possibility of compilation bug cannot be tolerated in certain applications with high safety requirements, and then costly solutions such as disabling all optimizations are used to get assembly code that is close to the source. In contrast, CompCert, despite not optimizing as well as gcc -O3 or clang -O3, allows using optimizations safely.
Adding security features (protections against buffer overflow, control-flow integrity checks, etc.) during compilation, as opposed to adding them at the source level, is very tempting: those features will be added consistently, and won’t risk being removed by an optimizing compiler.
In a certified compilation framework, in addition to proving that the security features won’t disturb the normal execution of the program, one could even try proving that they block certain attacks (which entails building a formal model of an attacker).
This is a CIFRE PhD with STMicroelectronics.
(It is also possible to pursue such a PhD funded by the scholarships handed out competitively by the graduate school.)
