Encadrants : David Monniaux et Bruno Ferres
Contexte
Les attaques en fautes (par faisceau laser, injection électromagnétique, ou même purement logicielle) constituent une menace sévère contre tous les systèmes embarqués. Bien qu’il existe des contre-mesures (matérielles, logicielles, ou hybrides) pour chaque modèle de faute, il est souvent complexe d’ajouter ces contre-mesures dans le flot de compilation des programmes. En outre, la question de l’efficacité de ces contre-mesures dans le code généré se pose, notamment dans des contextes ou plusieurs contre-mesures peuvent être composées pour durcir le code contre plusieurs modèles de fautes.
Objectifs du stage
Dans ce contexte, nous nous intéressons à la possibilité d’ajouter des fonctionnalités de sécurité dans des flots de compilation vérifiée (plus précisément, dans le compilateur CompCert, où le comportement du code machine est prouvé équivalent au comportement du code source). Ce stage est une bonne opportunité pour des étudiant(e)s intéressé(e)s par les méthodes formelles et la compilation de découvrir comment ces domaines peuvent être appliquées pour renforcer la sécurité des programmes. Pour plus d’information, voir le document ci-joint (en anglais). Si vous êtes intéressé(e)s, n’hésitez pas à contacter les encadrants.
