Soutenance de doctorat de Dorian Bourgeoisat : Garantir l’exécution à temps constant : l’interface matériel et logiciel
Télécom Paris, 19 place Marguerite Perey F-91120 Palaiseau [y aller], amphi 5
Jury
- Clémentine Maurice, Chargée de Recherches, CNRS – CRIStAL (Rapporteure)
- Guillaume Hiet, Professeur, CentraleSupélec – SUSHI (Rapporteur)
- Emmanuelle Encrenaz-Tiphene, Professeure, Sorbonne Université – LIP6 (Examinatice)
- Laure Petrucci, Professeure, CNRS – LIPN (Examinatice)
- Florian Brandner, Maître de conférences, Télécom Paris – ACES (Directeur de thèse)
- Ulrich Kühne, Maître de conférences, Télécom Paris – SSH (Co-encadrant de thèse)
Résumé
Les canaux auxiliaires temporels permettent à un attaquant de récupérer des données secrètes en mesurant les temps d’exécution. La programmation à temps constant a été utilisée pour se prémunir contre de telles attaques, mais les attaques microarchitecturales modernes, comme Spectre, ont montré que cette discipline était insuffisante. Pour prouver l’absence de fuites potentielles, les contrats matériel/logiciel ont été proposés. Ces contrats définissent formellement les contraintes imposées au logiciel pour un matériel donné. Cependant, ils ne tiennent pas compte de l’influence d’un autre composant clé de la sécurité des plateformes d’exécution : l’OS.
Nous commençons par construire un modèle matériel intégrant plusieurs fonctionnalités connues pour être sources de fuites temporelles, ainsi que la capacité de représenter les opérations de l’OS. Ce modèle est complété par un modèle d’attaquant basé sur les fils d’exécution, correspondant à des attaques concrètes connues, utilisé pour formuler une propriété de non-interférence.
Nous évaluons ensuite l’impact de différentes implémentations des opérations de l’OS, que nous appelons politiques, sur le résultat de multiples scénarios d’attaque, puis nous analysons et reproduisons nos observations sur FreeBSD. Sur la base de ces résultats, nous proposons d’étendre les contrats matériel/logiciel afin d’inclure le comportement de l’OS.
Enfin, nous proposons une méthode pour prouver nos contrats étendus en nous appuyant sur le modèle et une preuve par induction. Nous appliquons cette méthode à différents contrats et politiques.