Certified compilation: security and optimization

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.

We propose several internship topics around certified compilation (to be discussed according to the interests of the students), through modifications to CompCert (we have strong expertise on that) or designing a independent tool.

  • Optimizing compilation (loop nests, SIMD, scheduling…)
  • Integration of security measures at compile time

Some of these themes may lead to a CIFRE PhD with STMicroelectronics. It is also possible to pursue a PhD funded by the scholarships handed out competitively by the graduate school.

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

info visites 1693556