[Master] Compilation prouvée sécurisée vers processeur RISC-V

  Sommaire  

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.


Documents joints

Internship Proposal

24 octobre 2023
info document : PDF
137.9 kio

Contact | Plan du site | Site réalisé avec SPIP 4.2.8 + AHUNTSIC [CC License]

info visites 3863823