Position de doctorat - Spéculer sur la sécurité 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-0559

DOMAINE DE RECHERCHE

Cybersécurité: matériel et logiciels

ABSTRAIT

Nous considérons le contexte général de l'analyse automatisée de la sécurité au niveau du code. Alors que les attaques standard telles que le détournement de flux de contrôle tirent parti des failles de programmation (généralement, des vérifications liées manquantes), les attaques micro-architecturales récentes tirent parti de comportements subtils aux niveaux micro-architecturaux, généralement des comportements spéculatifs introduits dans les architectures modernes pour plus d'efficacité, en afin de contourner les protections et de fuir des données sensibles. Ces vulnérabilités sont extrêmement difficiles à trouver par un expert humain, car elles nécessitent de raisonner à un niveau très bas, sur un nombre exponentiel de comportements spéculatifs autrement cachés, et sur des propriétés de sécurité complexes (fuites et interférences de données, plutôt que mémoire standard les corruptions). L'objectif de ce travail de doctorat est de comprendre comment les méthodes automatisées de vérification symbolique et de recherche de bogues (en particulier mais sans s'y limiter, l'exécution symbolique) peuvent être efficacement portées au cas d'attaques micro-architecturales spéculatives, dans le but ultime de sécuriser les primitives de sécurité essentielles. dans les bibliothèques cryptographiques et les noyaux OS. Cet objectif général pose des défis en termes de sémantique des comportements spéculatifs, de sémantique des propriétés de sécurité et d'évolutivité des techniques de vérification. Ces techniques seront mises en œuvre dans le cadre d'analyse de code au niveau binaire BINSEC et leurs avantages seront évalués par une évaluation expérimentale rigoureuse.