Chercheur/Chercheuse (Post-Doctoral·e) en Informatique

Date limite de réponse :  16 juillet 2024
Type de recrutement : 
Poste ouvert en CDD
Quotité de travail : 
100%
Niveau d'emploi : 
A - Chercheur
Durée du contrat : 
1 an
Localisation : 
VERIMAG
Place du Torrent 150
38400 Saint-Martin-d'Hères

Présentation de la structure

Verimag est un laboratoire de recherche en informatique, menant principalement des recherches sur les approches permettant d’obtenir des systèmes embarqués fiables, sûrs et sécurisé, comportant 27 chercheurs et enseignants-chercheurs titulaires.

https://www-verimag.imag.fr/


Ce contrat de recherche est financé dans le cadre du projet Arsène du PERP Cybersécurité qui vise à développer des architectures sécurisées pour le numérique embarqué, utilisant notamment des solutions matérielles basées sur des jeux d'instructions RISC-V. Il se déroulera dans le cadre du lot 3 dont un des axes est le développement de compilateurs capables de générer du code sécurisé, à partir d'annotations fournies par le développeur. Dans ce cadre Verimag développera une variante du compilateur formellement vérifié CompCert avec des mécanismes pour sécuriser le code généré.

Vous travaillerez sous l’autorité de M. Bruno Ferres (MCF UGA), Sylvain Boulmé (MCF G-INP) et David Monniaux (DR CNRS).

Missions principales

Travail usuel de recherche en informatique : bibliographie, développement de prototypes, rédaction d’articles, participation à des conférences, etc.

Activités principales

  • Proposer des mécanismes permettant d’insérer des contre-mesures contre les attaques par exécutions transientes
  • Implémenter et prouver leur correction fonctionnelle formellement dans le contexte du compilateur formellement vérifié CompCert
  • Étudier les garanties de sécurité apportées par les contre-mesures ajoutées
  • Proposer une sémantique des exécutions transientes
  • Prouver l’adéquation des contremesures proposées par rapport à cette sémantique
  • Un programme scientifique plus détaillé est présenté ici :
    https://www-verimag.imag.fr/Funded-PhD-PostDoc-Countermeasures.html?lang=


Compétences attendues

  • Connaissance des méthodes formelles et des sémantiques de langages de programmation
  • Connaissance des outils de preuve déductive, notamment de Coq ; du fonctionnement de CompCert ; et/ou des attaques transientes sera fortement appréciée
  • Savoir faire de la modélisation formelle des sémantiques de langages de programmation et de langage d’assemblage (ISA)
  • Connaissance des attaques et des contre-mesures pour s’en protéger
  • Savoir utiliser des assistants de preuve et notamment de Coq
  • Maîtriser l’anglais
  • Savoir rédiger des articles scientifiques et faire des présentations orales des résultats scientifiques
  • Etre capable de discuter de questions scientifiques et techniques et travailler en équipe sur celles-ci
  • Doctorat informatique souhaité

Rémunération

A partir de 3020€ mensuel brut et en fonction de l’expérience.
Publié le  4 juin 2024
Mis à jour le  25 juin 2024