Pause
Lecture
Moteur de recherche d'offres d'emploi CEA

Méthodes formelles pour l'analyse de code


Détail de l'offre

Informations générales

Entité de rattachement

Le Commissariat à l'énergie atomique et aux énergies alternatives (CEA) est un organisme public de recherche.

Acteur majeur de la recherche, du développement et de l'innovation, le CEA intervient dans le cadre de ses quatre missions :
. la défense et la sécurité
. l'énergie nucléaire (fission et fusion)
. la recherche technologique pour l'industrie
. la recherche fondamentale (sciences de la matière et sciences de la vie).

Avec ses 16000 salariés -techniciens, ingénieurs, chercheurs, et personnel en soutien à la recherche- le CEA participe à de nombreux projets de collaboration aux côtés de ses partenaires académiques et industriels.  

Référence

2021-19267  

Description du poste

Domaine

Mathématiques, information  scientifique, logiciel

Contrat

Stage

Intitulé de l'offre

Méthodes formelles pour l'analyse de code

Sujet de stage

Conception d'une chaine d'outils d'analyse statique pour la détection de vulnérabilités lors d'une évaluation sécuritaire

Durée du contrat (en mois)

5

Description de l'offre

L'évaluation sécuritaire de logiciel embarqué comprend une revue de code réalisée par un évaluateur assisté d'outils d'analyse statique pouvant être configurés pour l'aider à vérifier des exigences de sécurité.

La méthodologie d'analyse de code consiste à extraire une portion de code suffisante pour la vérification formelle d'une propriété, d'essayer de la prouver automatiquement, et dans le cas où la preuve n'aboutit pas, de chercher des chemins qui réfutent cette propriété.

Les vulnérabilités détectées peuvent être causées par des données malformées (attaque logicielle) combinées à des injections de faute (attaque matérielle).

Une chaîne d'outils a été développée pour automatiser les différentes étapes de l'analyse :

  • analyse statique avec Frama-C Eva et des greffons développés en interne pour l'extraction de code, l'injection de fautes, et la vérification des propriétés,
  • exécution symbolique et dynamique (DSE) avec Lazart/KLEE pour la recherche de conditions de chemins réfutant une propriété avec des données malformées et des injections de faute en mode multi-faute et multi-modèle.

Une présentation de la chaîne d'analyse accompagnée d'expérimentations sur plusieurs bases de code réalistes a été faite à la conférence PROOF 2021 :
http://www.proofs-workshop.org/2021/papers/paper2.pdf

Les objectifs du stage sont :

  1. étendre la chaîne d’analyse existante avec de nouveaux modèles de faute,
  2. donner un meilleur retour à l’utilisateur sur les chemins analysés,
  3. définir des propriétés de plus haut niveau portant sur l’ensemble d’une base de code.

Moyens / Méthodes / Logiciels

Plateforme Frama-C (APIs, RTE, Slicing/PDG, Eva, MetACSL, E-ACSL), Lazart/KLEE

Profil du candidat

Ingénieur informatique fin d'études

Prérequis :

  • connaissance des techniques d'analyse formelle de code et des techniques d'attaque sur le code (vulnérabilités et exploits)
  • pratique du langage OCaml

Localisation du poste

Site

Grenoble

Localisation du poste

France, Auvergne-Rhône-Alpes, Isère (38)

Ville

Grenoble

Critères candidat

Diplôme préparé

Bac+5 - Diplôme École d'ingénieurs

Formation recommandée

Informatique, méthodes formelles appliquées à la cybersécurité