PhD - Analyse statique évolutive et précise de la mémoire pour les langages de bas niveau

DÉTAILS OPPORTUNITÉ

Récompense totale

0 $

Université étatique

CEA Tech

Région

Europe de l'Ouest

Pays hôte

France

Date limite

31 oct. 2021

Niveau d'études

Doctorat

Type d'opportunité

Doctorat

Spécialités

Informatique et sciences technologiques

Financement d'opportunité

Non financé

Pays éligibles

Cette opportunité est destiné à tous les pays

Région éligible

Toutes les régions

SL-DRT-21-0641

DOMAINE DE RECHERCHE

Intelligence artificielle et intelligence des données

ABSTRAIT

Le but de la thèse est de développer une analyse statique automatisée (basée sur une interprétation abstraite) pour vérifier, dans une grande base de code dans des langages compilés de bas niveau (par exemple C, C ++, assembly, Rust, Fortran), les propriétés de sécurité liées à mémoire, les propriétés des informations de flux lke et l'absence de corruption de la mémoire. Ce problème a de nombreuses applications en cybersécurité, car la plupart des problèmes de cybersécurité liés aux logiciels, et ceux qui ont la plus grande gravité, proviennent d'erreurs de sécurité de la mémoire (par exemple (débordements de mémoire tampon, utilisation après libre, déréférences de pointeur nul, mauvais type de poinçonnage , mauvaise interface entre plusieurs langages, etc.) Les trois principaux problèmes lors de la conception d'une telle analyse statique automatisée sont de maintenir un effort de vérification faible, de gérer des systèmes volumineux et complexes et d'être suffisamment précis pour que l'analyse ne rapporte pas un L'approche privilégiée de cette thèse s'appuiera sur le succès d'une nouvelle méthode utilisant des domaines abstraits paramétrés par des invariants de type, qui a trouvé un juste milieu entre précision (c'est-à-dire peu de fausses alarmes), efficacité (dans les ressources de calcul), et effort requis (de la part de l'utilisateur). Cette méthode a notamment permis de prouver de manière entièrement automatique l'absence d'escalade de privilèges et de corruption de mémoire d'un micro-noyau industriel existant à partir de son code machine, en utilisant seulement 58 lignes d'annotations.De nombreuses questions de recherche demeurent, et nous explorerons comment étendre l'analyseur pour améliorer l'évolutivité (en utilisant l'analyse compositionnelle), comment améliorer son expressivité (pour montrer des propriétés de sécurité complexes comme la non-interférence), comment améliorer la précision sans dégrader l'efficacité, ou comment réduire davantage le nombre d'annotations (en utilisant l'inférence automatique d'invariants de type plus précis).