QUI SOMMES-NOUS ?

Situé sur le campus de l’École polytechnique, au cœur du pôle scientifique et technologique d’envergure mondiale de Paris-Saclay, le site de Palaiseau regroupe les activités de Thales Research & Technology (TRT), le centre de recherche du Groupe, et de ThereSIS (THALES European REsearch center for Security & Information Systems) au service des activités mondiales du Groupe. Grâce à une politique de partenariat proactive avec le monde académique et un réseau international d’entreprises innovantes, nos équipes de recherche de TRT développent des technologies de rupture et celles de ThereSIS sont dédiées à la sécurisation des systèmes d’information, à l’ingénierie des systèmes complexes et aux technologies innovantes de la transformation numérique afin d’obtenir rapidement des résultats répondant à des demandes opérationnelles concrètes.

Dans ce cadre nous recherchons un :

STAGE - Ingénieur  Vérification formelle de modules critiques (F/H)Basé à Palaiseau (91)

QUI ETES-VOUS ?

• Etudiant en école d’ingénieur ou de formation équivalente, vous préparez un Master 1 ou 2 avec une spécialisation en informatique ?
• Vous recherchez un stage de fin d’étude pour une durée de 6 mois ?
• Votre formation vous a permis d’acquérir des compétences dans les domaines suivants :

• Logique et génie logiciel
• Langage de programmation
• Connaissances du langage C
• Connaissances en systèmes d’exploitation

• Vous portez un intérêt à la vérification formelle, la logique et aux raisonnements mathématiques ?
• Savoir appliquer les outils de preuve et analyser les programmes serait un plus ?
• Vous faites preuve de curiosité au quotidien c’est la raison pour laquelle vous souhaitez effectuer votre stage en recherche ?
• Enfin vous souhaitez évoluer dans un milieu international et de ce fait parler couramment anglais (Niveau B2-C1 attendu) ?

Vous vous reconnaissez ? Alors découvrez vite vos futures missions. :)

CE QUE NOUS POUVONS ACCOMPLIR ENSEMBLE :

Le Groupe de Recherche Systèmes et Techniques de l’Information (STI) de Thales Recherche et Technologie (TRT-France à Palaiseau) se compose de plusieurs laboratoires dont un est spécialisé dans la conception des systèmes temps-réel embarqué critiques (LSEC).

THALES conçoit et développe des systèmes temps-réel de plus en plus complexes et critiques.

De ce fait, la difficulté de validation et de vérification de ces systèmes est croissante.

Lors de la validation des logiciels faisant partie de ces systèmes, on cherche généralement à atteindre un niveau d’assurance élevée, ce qui peut être fait par la vérification formelle.

Dans certains domaines critiques, la vérification formelle est imposée par des normes de certification. Un élément clef pour la sécurité de ces systèmes est le système d’exploitation (OS). 

Parmi les différentes techniques de vérification, l’analyse statique (notamment, l’analyse de valeur) permet de démontrer formellement l’absence d’erreurs à l’exécution (telles que les accès invalides à la mémoire, des divisions par zéro, des dépassements arithmétiques, etc.).

La vérification déductive (ou preuve de programme) reste l’une des techniques les plus rigoureuses permettant de démontrer formellement qu’un programme respecte sa spécification. Les avancées récentes des outils de vérification (notamment, la plate-forme Frama-C et ses greffons Eva, WP et MetAcsl) permettent aujourd’hui de spécifier un large spectre de propriétés de sûreté de la mémoire (e.g. absence d’accès mémoire invalides) et de sécurité (intégrité, confidentialité) et de les vérifier automatiquement.

Nous nous intéresserons particulièrement aux bibliothèques ou utilitaires système, par exemple, relatifs à la cryptographie ou au contrôle d’accès (libc, libgrypt, OpenSSL, sudo, etc.).

Votre stage vise à identifier un ensemble de propriétés mémoire et à les vérifier à l’aide des outils de vérification formelle. On utilisera la plateforme Frama-C développée par le CEA List, ses analyseurs EVA et WP, et son langage de spécification ACSL.

Dans un premier temps, nous allons étudier des propriétés de sûreté mémoire, qui ne nécessitent qu’un nombre limité d’annotations manuelles. Ensuite, nous allons considérer des propriétés de plus haut niveau (notamment, d’isolation) qui pourront être spécifiées à l’aide de MetAcsl, un nouveau greffon de Frama-C, et ensuite prouvées par le greffon WP. 

Votre stage vous permettra d’acquérir des compétences et une expérience en vérification des logiciels critiques système fréquemment utilisés, qui sont très recherchées par les entreprises.

Selon votre profil, votre stage pourra avoir une orientation professionnelle ou de recherche.

Dans ce contexte, vos missions principales seront les suivantes :

• Vous apprendrez et approfondirez vos connaissances en spécification et vérification formelle des programmes C.
• Vous appliquerez l’analyse de valeurs pour montrer l’absence d’erreur à l’exécution dans les modules ciblés
• Vous écrierez des spécifications formelles des propriétés de sécurité avec MetAcsl.
• Vous appliquerez les outils de preuve et analyserez leurs résultats
• Vous adapterez les spécifications pour finaliser la preuve

Votre travail se déroulera en étroite collaboration avec vos encadrants pour vous guider et vous permettre d’acquérir ou d’approfondir vos connaissances dans le domaine.

Tous nos stages sont conventionnés et soumis à une gratification dont le montant est déterminé selon votre niveau d’études.

Innovation, passion, ambition : rejoignez Thales et créez le monde de demain, dès aujourd’hui.