Stage Bac +5 – Modélisation d’une architecture de sécurité et preuves formelles (H/F)

Stage Par Thales
  • Architecture
  • Gennevilliers
  • A négocier

Description

Stage Bac +5 – Modélisation d’une architecture de sécurité et preuves formelles (H/F)

QUI SOMMES-NOUS ?

Rejoignez Thales, leader mondial des technologies de sûreté et de sécurité pour les marchés de l'Aérospatial, du Transport, de la Défense et de la Sécurité . Fort de 62 000 collaborateurs dans 56 pays , le Groupe bénéficie d'une implantation internationale qui lui permet d'agir au plus près de ses clients, partout dans le monde .

Les 14 000 collaborateurs de l' activité Systèmes d'information et de communication sécurisés développent des systèmes de communications militaires et de numérisation de l'espace de bataille , des systèmes de sécurité urbaine , de protection des États et des infrastructures critiques , ainsi que des solutions de cybersécurité .

Le site de Gennevilliers est le cœur des activités de conception, de développement et de soutien des produits et solutions de radiocommunications des armées, des réseaux d'infrastructures résilients et de communications par satellite , ainsi que des solutions de cybersécurité .
La Direction de la Sécurité des Technologies de l'Information recherche un/une Stage Bac +5 – Modélisation d'une architecture de sécurité et preuves formelles (H/F)

Basé(e) à Gennevilliers.


QUI ETES-VOUS ?

Etudiant de dernière année en école d'ingénieur ou équivalent ?
Vous avez une connaissance théorique des méthodes formelles ?
Vous connaissez un langage formel (ex : B, Coc, Isabel, HOL) ?
Vous connaissez un langage de programmation (C, C++, Python) ?

CE QUE NOUS POUVONS ACCOMPLIR ENSEMBLE :

L'objectif de ce stage est de réaliser à partir d'une architecture de sécurité réalisant un ensemble de propriétés de sécurité, une modélisation de cette architecture et d'étudier les outils et méthodes permettant d'établir un ensemble de preuves formelles entre ces propriétés et une implémentation.

L'architecture modélisée s'appuie sur des propriétés de contrôle d'accès et de contrôle de flux dont la logique et les modèles doivent être étudiés et raffinés notamment en termes d'automates et de modèle de données.

L'objectif de la modélisation est donc de définir formellement les propriétés de sécurité attendues sur le système et de démontrer que l'architecture retenue et modélisée possède ces propriétés.

Ainsi, dans un premier temps, l'architecture sera analysée afin d'en définir les modèles : modèles de données et de contrôle associés Le choix des outils et des langages formels appropriés pour ce type de problème feront partie de l'analyse : le langage retenu doit permettre d'exprimer des propriétés de sécurité mais aussi de décrire les modèles de données et de contrôle précédemment mentionnés.

Dans un second temps, le stage proposera la définition et la mise en œuvre de stratégies de preuves sur les modèles afin de démontrer la préservation des propriétés de sécurité attendues. L'objectif de cette phase est d'utiliser des outils de preuve automatique ou du model-checking dans le but d'avoir une approche systématique.

Missions :
• Prendre connaissance du système étudié : Architecture logicielle et matérielle et modèle de référence des échanges entre les traitements cloisonnés.
• Etudier et analyser les outils et les langages permettant l'expression des modèles de contrôle et de données.
• Formalisation de propriétés de sécurité.
• Analyse et mise en œuvre d'une preuve de conformité entre l'implémentation et les modèles.

La perspective de rejoindre un Groupe innovant vous motive ? Alors rejoignez-nous en postulant à cette offre .

Vous souhaitez en savoir plus sur les activités Systèmes d'information et de communication sécurisés ? Cliquez ici et ici .

Découvrir la Page Entreprise

Ils ont travaillé ici