Stage : vérification formelle de traitement de chaînes de caractères et application à l’obfuscation logicielle - Thales Research & Technology (H/F)

Stage Par Thales
  • Palaiseau
  • A négocier

Description

Stage : vérification formelle de traitement de chaînes de caractères et application à l’obfuscation logicielle - Thales Research & Technology (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 .
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 est le centre de recherche du Groupe.

Grâce aux nombreux partenariats avec le monde académique et un réseau international d'entreprises innovantes, nos équipes de recherche développent des technologies de rupture au service des unités opérationnelles du Groupe.

Le stage s'exécutera au sein du Laboratoire Systèmes embarqués critiques (LSEC).

Nous recherchons un/une stagiaire sur le sujet de la «vérification formelle de traitement de chaînes de caractères et de son application à l'obfuscation logicielle», basé(e) à Palaiseau.


QUI ETES-VOUS ?



Vous préparez un bac +5 à l'université ou en école d'ingénieur, avec une spécialité dans le domaine du logiciel, des méthodes formelles ou des mathématiques, vous maîtrisez Ada, Parser et les bases en méthodes formelles.

Des connaissances en SPARK 2014, Méthodes formelles (SAT/SMT solver), Obfuscation logicielle et Why3 seraient un plus significatif.

De plus, vous êtes à l'aise en anglais.

CE QUE NOUS POUVONS ACCOMPLIR ENSEMBLE :



THALES conçoit et développe des systèmes temps-réel de plus en complexe et critique. De ce fait, la difficulté de vérification de ces systèmes n'est que croissante. En conséquence, les coûts associés à la vérification par tests constituent une part majeure du coût de développement d'un système.

Une piste envisagée pour réduire ces coûts est la vérification formelle de code. La vérification formelle de code est une technique mathématique permettant de prouver (et non plus tester) que le code répond à sa spécification. Autrefois, cette vérification était une activité très manuelle du fait de la faiblesse des outils de preuve (appelés prouveurs).

Aujourd'hui, beaucoup de ces vérifications sont devenues automatiques au fil des progrès de ces prouveurs. Cependant, des points durs subsistent dans la vérification automatique.

L'un d'eux est la preuve de fonction travaillant sur des chaînes de caractères.

L'objectif de ce stage est d'évaluer les possibilités des outils de preuves automatiques sur les chaînes de caractères au travers d'une étude de cas sur l'obfuscation de code.

EN NOUS REJOIGNANT, VOUS VOUS VERREZ CONFIER LES MISSIONS SUIVANTES :


Dans le cadre de ce stage, nous allons nous intéresser à concevoir et développer un obfuscateur de code à des fins de vérification formelle sur les chaînes de caractères.

· Etat de l'art sur les techniques d'obfuscation automatique de code
· Identifier et proposer un outil d'obfuscation et sa spécification
· Concevoir et spécifier formellement la solution logicielle
· Conduire des activités de vérification formelle de la solution logicielle
· Expérimenter la solution sur des études de cas logicielles Thales

A l'issue de votre stage, vous aurez acquis des connaissances significatives en modélisation et vérification de contrats formelle, et des connaissances sur l'état de l'art des logiciels d'obfuscation.

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 de Thales ? Cliquez ici .

Découvrir la Page Entreprise

Ils ont travaillé ici