Vous êtes ici

Soutenance de thèse de Thomas Letan, CIDRE, le jeudi 25 octobre à 14h, au 30 rue des Favorites, à Paris

Bonjour,

Vous êtes cordialement invités à la soutenance de thèse de Thomas Letan, CIDRE, le 25 octobre à 14h, au 30 rue des Favorites, à Paris (dans les locaux de la formation continue (l’Exed) de CentraleSupélec).

Sujet de la thèse : Specifying and Verifying Hardware-based Security Enforcement Mechanisms

Résumé :

Dans ces travaux de thèse, nous nous intéressons à une classe de stratégies d'application de politiques de sécurité que nous appelons
HSE, pour Hardware-based Security Enforcement. Dans le cadre d'un mécanisme HSE, un ou plusieurs composants logiciels de confiance
contraignent l'exécution du reste de la pile logicielle avec le concours de la plate-forme matérielle sous-jacente afin d'assurer le respect
d'une certaine politique de sécurité. Par exemple, un système d'exploitation s'appuie classiquement sur la MMU pour isoler les
applications.

Pour qu'un mécanisme HSE contraigne effectivement l'exécution de logiciels arbitraires, il est nécessaire que la plate-forme matérielle
et les composants logiciels de confiance l'implémentent correctement. Ces dernières années, plusieurs vulnérabilités ont mis à défaut des
implémentations de mécanismes HSE. Nous concentrons ici nos efforts sur celles qui sont le résultat d'erreurs dans les spécifications
matérielles et non dans une implémentation donnée. Plus précisément, nous nous intéressons aux cas particulier de l'usage légitime, par un
attaquant, d'une fonctionnalité d'un composant matériel pour contourner les protections offertes par un second.

Notre but est d'explorer des approches basées sur l'usage de méthodes formelles pour spécifier et vérifier des mécanismes HSE. Nous pensons
que de telles approches seraient bénéfiques tant aux concepteurs de plate-formes matérielles qu'aux développeurs de composants logiciels. La
spécification de mécanismes HSE peut en effet servir de point de départ pour la vérification des spécifications matérielles concernées, dans
l'espoir de prévenir des attaques profitant de la composition d'un grand nombre de composants matériels. Elles peuvent ensuite être fournies aux
développeurs logiciels, sous la forme d'une liste de pré-requis que leurs produits doivent respecter s'ils désirent l'application d'une
politique de sécurité clairement identifiée.

Abstract :
 
In this thesis, we consider a class of security enforcement mechanisms we called Hardware-based Security Enforcement (HSE). In such mechanisms,
some trusted software components rely on the underlying hardware architecture to constrain the execution of untrusted software components
with respect to targeted security policies. For instance, an operating system which configures page tables to isolate userland applications implements a HSE mechanism.

For a HSE mechanism to correctly enforce a targeted security policy, it requires both hardware and trusted software components to play their parts. During the past decades, several vulnerability disclosures have defeated HSE mechanisms. We focus on the vulnerabilities that are the result of errors at the specification level, rather than implementation errors. In some critical vulnerabilities, the attacker makes a legitimate use of one hardware component to circumvent the HSE mechanism provided by another one. For instance, cache poisoning attacks leverage inconsistencies between cache and DRAM’s access control mechanisms. We
call this class of attacks, where an attacker leverages inconsistencies in hardware specifications, compositional attacks.

Our goal is to explore approaches to specify and verify HSE mechanisms using formal methods that would benefit both hardware designers and software developers. Firstly, a formal specification of HSE mechanisms can be leveraged as a foundation for a systematic approach to verify hardware specifications, in the hope of uncovering potential compositional attacks ahead of time. Secondly, it provides unambiguous specifications to software developers, in the form of a list of requirements.

Orateur: 
Thomas Letan
Date: 
Jeudi, 25. octobre 2018 - 14:00 - 18:30
Lieu: 
30 rue des Favorites à Paris
Type soutenance: 
Composition du Jury: 

ENCRENAZ-TIPHÈNE Emmanuelle, Maître de conférence à Sorbonne Université

BARTHE Gilles, Professor à IMDEA Software Institute (rapporteur)

PIERRE Laurence, Professeur des Universités, Université Grenoble Alpes (rapporteur)

MÉ Ludovic, Professeur, Inria Rennes (directeur de thèse)

CHIFFLIER Pierre, Chef de laboratoire ANSSI (encadrant)

HIET Guillaume, Professeur adjoint à CentraleSupélec (encadrant)