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: the formal correctness of CompCert states that if the compiler succeeds to produce an executable, then the observable behaviors of the executable are also observable on 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.
Security of embedded systems like smart-cards, secured dongles and IoTs relies on the robustness of devices against physical fault attacks (such as laser or electromagnetic attacks). Current certification schemes (e.g., Common Criteria) require protection mechanisms against multi-fault injection attacks. Typically, these protections often consist in Counter-Measures (CM): monitors which perform redundant computations in order to detect/prevent some attacks.
Some of these CMs are "manually" written in the source code by developers. For example, the process of counting the number of trials for typing some pin-code is duplicated in order to make successful hardware attacks on this number more complex. However, because such CM perform redundant computations on execution without attacks, optimizing compilers may remove them.
A solution of has been experimented within LLVM compiler. It consists in introducing observations of the program state that are intrinsic to the correct execution of security protections, along with means to specify and preserve observations across the compilation flow. Such observations complement the input/output semantics-preservation contract of compilers. In practice, they are given as annotations of the source code.
From these works, the internship will study how to use the formal notion of observable events of CompCert, in order to ensure that CMs are not removed by the compiler (as a consequence of its formal correctness).
This wide topic is also the subject of a future PhD thesis proposed as an extension to the internship.
