Home > Careers

Careers

Internships / Stages

We view internships as a recruitment channel, and prefer graduate students who can be integrated into our team at the end of their internship.

Les stages, d’une durée de 6 mois, s’adressent à des étudiants de Master 2 ou de fin d’études d’ingénieur.

Les stages sont pour Trusted Labs un canal de recrutement ; nous favorisons donc les étudiants en fin d’études susceptibles d’intégrer notre équipe à l’issue du stage. Les spécialités que nous recherchons en priorité incluent :

Pour postuler, les candidats stagiaires sont invités à envoyer leur CV et une lettre de motivation et à préciser la référence du ou des stage(s) visé(s).

STG-2013-TLA-001 Vérification formelle d’implémentations cryptographiques

STG-2013-TLA-002 Vérification formelle de contre-mesures dans un circuit sécurisé

STG-2013-TLA-001 Vérification formelle d’implémentations cryptographiques

Contexte

Les composants cryptographiques (i.e. les primitives et les protocoles) assurent la sécurité de nombreux systèmes informatiques. Des dispositifs mobiles aux systèmes client/serveur, la sécurité repose en grande partie sur la correction de leur noyau cryptographique. Cependant, l’implémentation de ces composants est susceptible d’être erronée non seulement à cause de la complexité de leur spécification mais aussi en raison de nombreuses optimisations. Tandis que de nombreux travaux sont concentrés sur la sécurité de la spécification, la correction de leur implémentation reste un défi à relever. En effet, la plupart des outils formels génériques ne sont pas adaptés à ce domaine spécifique. Plusieurs études ont montré qu’une erreur mineure d’implémentation peut s’avérer dangereuse car elle ouvre le chemin aux nouvelles attaques sur le composant afin de compromettre la sécurité du système.

Travail à réaliser

Dans ce stage nous nous intéressons à la spécification formelle d’une implémentation cryptographique et à la vérification de sa correction fonctionnelle. Le travail consiste à définir l’approche technique, à la mettre en œuvre dans un outil. Ce stage pourra aboutir à une thèse de doctorat.

Compétences requises

Compétences acquises en fin de stage

Lieu : Ce stage se déroulera sur notre site de Versailles (78000)

Durée : 6 mois

STG-2013-TLA-002 Vérification formelle de contre-mesures dans un circuit sécurisé

Contexte

Les circuits sécurisés (par ex. smart card IC) sont le composant matériel des dispositifs sécuritaires comme les cartes à puce, le dongle USB ou encore la carte microSD, etc. Pendant leur utilisation, ces matériels sont soumis aux nombreuses attaques physiques comme la perturbation, les canaux auxiliaires ou l’injection de faute. Face à ces attaques, un circuit sécurisé implémente souvent des contre-mesures plus ou moins sophistiquées mais dans la plupart des cas incomplètes.

Jusqu’à récemment la seule méthode pour valider ces contre-mesures consistait à soumettre le circuit à une série d’attaques dans un laboratoire. Ces tests permettent d’identifier les vulnérabilités du circuit et donc, d’évaluer l’efficacité de ses contre-mesures en fonction de la réalisabilité de chaque attaque (i.e. the attack potential). Cette méthode est indispensable mais est loin d’être exhaustive à cause notamment du coût très élevé du montage des attaques.

Travail à réaliser

Ce stage consiste à modéliser les contre-mesures implémentées dans un circuit sécurisé et prouver leur efficacité dans un modèle de faute définie. La modélisation pourra s’appuyer sur nos travaux existants dans l’assistant de preuve Coq ou bien reposer sur les autres techniques formelles comme celles décrites.

Ce stage pourra aboutir à une thèse de doctorat (par contrat CIFRE).

Compétences requises

Compétences acquises en fin de stage

Lieu : Ce stage se déroulera sur notre site de Versailles (78000)

Durée : 6 mois

Careers