Génération d'implémentations de protocoles modulaires H/F
Stage Grenoble (Isère) Développement informatique
Description de l'offre
Détail de l'offre
Informations générales
Entité de rattachement
Le Commissariat à l'énergie atomique et aux énergies alternatives (CEA) est un organisme public de recherche.Acteur majeur de la recherche, du développement et de l'innovation, le CEA intervient dans le cadre de ses quatre missions :
. la défense et la sécurité
. l'énergie nucléaire (fission et fusion)
. la recherche technologique pour l'industrie
. la recherche fondamentale (sciences de la matière et sciences de la vie).
Avec ses 16000 salariés -techniciens, ingénieurs, chercheurs, et personnel en soutien à la recherche- le CEA participe à de nombreux projets de collaboration aux côtés de ses partenaires académiques et industriels.
Référence
2019-10582Description de l'unité
Le Leti, institut de recherche technologique de Cea Tech, a pour mission d'innover et de transférer les innovations à l'industrie. Son cœur de métier réside dans les technologies de la microélectronique, de miniaturisation des composants, d'intégration système, et d'architecture de circuits intégrés, à la base de l'internet des objets, de l'intelligence artificielle, de la réalité augmentée, de la santé connectée. Le Leti façonne des solutions différenciantes, sécurisées et fiables visant à augmenter la compétitivité de ses partenaires industriels par l'innovation technologique. L'institut est localisé à Grenoble avec deux bureaux aux USA et au Japon, et compte 1800 chercheurs.
Description du poste
Domaine
Sécurité contre la malveillance
Contrat
Stage
Intitulé de l'offre
Génération d'implémentations de protocoles modulaires H/F
Sujet de stage
Génération d'implémentations de protocoles modulaires
Durée du contrat (en mois)
6
Description de l'offre
Les protocoles cryptographiques sont omniprésents dans les réseaux. Ils servent à apporter de la sécurité aux échanges. On en retrouve dans tous les types de réseaux, qu’ils soient sur internet, en rapport avec l’IoT, filaires ou sans fil. Dans l’ambition de les rendre accessibles à des application IoT, des implémentations légères et fiables sont nécessaires. Pour y parvenir, une possibilité réside dans l’utilisation des méthodes formelles pour exprimer, vérifier les propriétés de sécurité. Une difficulté consiste à faire le lien entre les spécifications prouvées et le code qui s’exécute.
L’objectif de ce stage est de fournir une preuve de concept permettant de générer une implémentation de protocole communication à partir de spécifications. Ces spécifications seront écrites dans un langage pouvant faire l’objet de vérifications formelles de sécurité [1], afin de garantir la sécurité du protocole implémenté. Cependant, garantir que l’implémentation est fidèle aux spécifications est une problématique importante de la sécurité des protocoles cryptographique. Cette génération de code devra permettre de changer et/ou intégrer facilement des primitives cryptographiques (ex : RSA, Courbes elliptiques (BEC, …), Trivium) et l’architecture matérielle (ex : x86, ARM, optimisation liées au hardware) [2, 3] afin qu’une brique protocolaire puisse être modulaire.
Références
[1] S. Mödersheim. Algebraic Properties in Alice and Bob Notation. In Proceedings of Ares’09, pages 433–440. IEEE Xplore, 2009. Extended version: Technical Report RZ3709, IBM Zurich Research Lab, 2008
[2] NISTIR 8105, Report on Post-Quantum Cryptography, NIST 2016.
[3] Henry, Jasmine. "What is Crypto-Agility?". Cryptomathic. Retrieved 26 November 2018.
Moyens / Méthodes / Logiciels
Linux, C, Python
Profil recherché
Profil du candidat
Niveau : Bac + 5, Ingénieur ou Master
Prérequis : Cryptographie, compilation et langages de programmation