ALTERNANCE - Preuve formelle d'un logiciel embarqué de sécurité F/H

QUI SOMMES-NOUS ?

Thales propose des systèmes d'information et de communication sécurisés et interopérables pour les forces armées, les forces de sécurité et les opérateurs d'importance vitale. Ces activités, qui regroupent radiocommunications, réseaux, systèmes de protection, systèmes d'information critiques et cybersécurité, répondent aux besoins de marchés où l'utilisation des nouvelles technologies numériques est déterminante. Thales intervient tout au long de la chaîne de valeur, des équipements aux systèmes en passant par le soutien logistique et les services associés.

Le site de Gennevilliers est le cœur des activités de conception, et de développement et de soutien des produits et solutions de radiocommunications des Armées, des systèmes de réseaux d'infrastructures résilients et de communications par satellite, et ainsi que des solutions de cybersécurité.

QUI ETES-VOUS ?

Vous êtes issus d'une formation ingénieur BAC+4 à dominante logicielle et vous recherchez une alternance pour 2 ans ?

Compétences souhaitées :

• Développement C
• Raisonnement mathématique
• Anglais scientifique
• Connaissance en méthodes formelles
• Connaissance en cyber-sécurité

Vous savez faire preuve de Curiosité, d'enthousiasme et de ténacité ?

Alors ce poste est fait pour vous !

CE QUE NOUS POUVONS ACCOMPLIR ENSEMBLE :

Le service CyberProtection Solutions Engineering du Thales SIX réalise l'ingénierie pour sécuriser les grands systèmes de défense nationaux et internationaux.

L'objectif de l'alternance est de développer un logiciel embarqué de sécurité qui puisse réussir une évaluation Critères Communs EAL7.

Un logiciel embarqué de sécurité est un logiciel qui s'exécute sur un composant électronique et qui assure des fonctions de sécurité pour le composant, parmi lesquelles l'injection sécurisée de données dans le composant, le stockage sécurisé de ces données, le déploiement sécurisé de ces données sur une interface, la gestion du cycle de vie du composant ou encore la gestion d'un journal de sécurité.

Pour réussir une évaluation EAL7, le développeur doit fournir à l'évaluateur un certain nombre d'éléments, dont :

- la cible de sécurité (un document qui définit le problème de sécurité et en déduit des exigences de sécurité portant sur le logiciel),

- les documents de conception du logiciel,

- le code source du logiciel,

- la preuve formelle que le logiciel satisfait ses exigences de sécurité.

L'alternant devra donc produire tous les éléments requis. Il développera le logiciel en C et fera la preuve en Coq.

L'encadrant connaît bien les Critères Communs, C et Coq. L'alternant pourra donc acquérir les compétences nécessaires pour travailler dans le domaine très prometteur des méthodes formelles appliquées à la sécurité des logiciels embarqués.

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