En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)
Portail > Offres > Offre UMR7503-VINLAP-002 - Ingénieur d’étude en compilation (H/F)

Ingénieur d’étude en compilation (H/F)


Date Limite Candidature : mercredi 24 juillet 2024 23:59:00 heure de Paris

Assurez-vous que votre profil candidat soit correctement renseigné avant de postuler

Informations générales

Intitulé de l'offre : Ingénieur d’étude en compilation (H/F)
Référence : UMR7503-VINLAP-002
Nombre de Postes : 1
Lieu de travail : VANDOEUVRE LES NANCY
Date de publication : mercredi 3 juillet 2024
Type de contrat : CDD Technique/Administratif
Durée du contrat : 12 mois
Date d'embauche prévue : 2 septembre 2024
Quotité de travail : Temps complet
Rémunération : De 2372,55 € brut à 2497,14 € brut mensuel, ajustable selon expérience
Niveau d'études souhaité : Niveau 6 - (Bac+3 ou 4)
Expérience souhaitée : 1 à 4 années
BAP : Informatique, Statistiques et Calcul scientifique
Emploi type : Ingénieur-e en ingénierie logicielle

Missions

Le langage de programmation Jasmin est conçu pour permettre l’écriture d’implémentations de bas-niveau offrant de fortes garanties telles que la sûreté, la correction ou encore l’absence de fuite d’information sensible par des canaux auxiliaires. Il a été notamment utilisé pour implémenter des primitives cryptographiques particulièrement rapides. Ses liens étroits avec des outils de vérification — automatiques ou interactifs — en font un langage de choix pour des implémentations formellement prouvées.
Le compilateur qui traduit ce langage en assembleur est certifié au moyen de l’assistant à la preuve Coq : les propriétés qui sont établies au niveau du programme source sont préservées et restent valides au niveau du programme assembleur. Ces garanties peuvent être obtenues sans pénaliser les performances, comme le montrent de récentes études de cas.
Outre le compilateur certifié, divers outils permettent la manipulation, l’étude et la vérification de programmes écrits dans le langage de programmation Jasmin. Ces outils sont principalement développés en OCaml et servent d’interface entre le langage Jasmin et ses usagers.

La personne recrutée rejoindra l’équipe de développement de Jasmin. Elle interagira avec les utilisateurs et les autres contributeurs et plus généralement avec l’ensemble des membres du groupe Formosa Crypto. Elle participera à la maintenance et l’amélioration des parties non certifiées et enrichira leur documentation. Elle prendra activement part à la conception et l’implémentation de nouveaux aspects du langage et notamment développera de nouveaux outils de traitement programmes Jasmin.

Activités

- Maintenir les parties non certifiées, en corriger les bugs.
- Améliorer les interfaces du compilateur (parseur et pretty-printeur); refondre l’interpréteur.
- Générer des interfaces de programmes jasmin pour les langages de haut niveau, en particulier Rust.
- Mettre en œuvre le système de modules.
- Réviser l’interface de traduction pour l’assistant de preuve EasyCrypt utilisée pour la vérification semi-automatique de diverses propriétés (sûreté, non-interférence, etc).

Compétences

- Programmation en OCaml
- Communication en langue anglaise, à l’écrit et à l’oral
- Compétences dans le domaine de la compilation

Contexte de travail

La personne recrutée intégrera l’équipe de recherche PESTO dont les thématiques de recherche s’articulent autour des méthodes formelles pour la sécurité. Cette équipe étudie notamment les protocoles et leurs implémentations. Ses bureaux se trouvent au Loria, Laboratoire lorrain de Recherche en Informatique et ses Applications (UMR 7503), à Villers-lès-Nancy.