Supervised by: Sylvain Boulmé, Marie-Laure Potet
Contacts:
- Sylvain.Boulme@univ-grenoble-alpes.fr
- Marie-Laure.Potet@univ-grenoble-alpes.fr
Verimag Lab
Keywords: software security protections, compilation, fault injection attacks
Scientific Context
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. More details are provided in the document below. However, because such CM perform redundant computations on execution without attacks, optimizing compilers may remove them.
The purpose of this internship is to study how the formal notion of observable events introduced in the (certified) CompCert compiler may be used to ensure that such CMs are not removed by the optimization steps, as a consequence of its formal correctness.
Moe details are given in the document below.
Not that this topic is also the subject of a future Phd thesis proposed as an extension to the internship.
See also this related topic.
