L’Ecole doctorale : Ecole Doctorale de l’Institut Polytechnique de Paris

et le Laboratoire de recherche SAMOVAR – Services répartis, Architectures, Modélisation, Validation, Administration des Réseaux

présentent

l’AVIS DE SOUTENANCE de Madame Subashiny TANIGASSALAME

Autorisée à présenter ses travaux en vue de l’obtention du Doctorat de l’Institut Polytechnique de Paris, préparé à Télécom SudParis en :

Informatique

« Privagic: Utilisation d’environnement d’exécution sécurisé rendu pratique avec typage »

le VENDREDI 5 AVRIL 2024 à 10h30 à

Amphi 2, 19 Pl. Marguerite Perey, 91120 Palaiseau

Membres du jury :

M. Marc SHAPIRO, Directeur de recherche émérite, Sorbonne Université LIP6, FRANCE – Rapporteur
M. Laurent RÉVEILLÈRE, Professeur, Université de Bordeaux, FRANCE – Rapporteur
Mme Sonia BEN MOKHTAR, Directrice de recherche, LIRIS CNRS, FRANCE – Examinateur
M. Stéphane DUCASSE, Directeur de recherche, Inria, FRANCE – Examinateur
M. Gaël THOMAS, Directeur de recherche, Inria Saclay, FRANCE – Directeur de these

« Privagic: Utilisation d’environnement d’exécution sécurisé rendu pratique avec typage »

présenté par Madame Subashiny TANIGASSALAME

Résumé :

Pendant plus de vingt ans, plusieurs outils ont été proposés pour partitionner automatiquement une application entre une zone de mémoire sécurisée et une zone de mémoire non sécurisée. Ces outils analysent le flux de données de l’application afin d’identifier les emplacements mémoire susceptibles de contenir des valeurs sensibles. La plupart de ces outils se comportent de manière incorrecte en présence de pointeurs. Lorsqu’ils sont corrects, ils sont incapables de gérer les threads en raison de la difficulté à suivre les pointeurs dans une application multi-thread. Les outils actuels sont également incapables de diviser une application en plus de deux partitions, en raison de la sur-approximation, qui entraîne le partage erroné d’emplacements mémoire entre les deux partitions. Dans cette thèse, au lieu de partir de l’analyse du flux de données, nous proposons de partir d’une technique plus précise : le typage de langage. Nous introduisons le typage sécurisé, qui consiste à incorporer un identifiant de partition dans le système de types d’un langage. Sur la base du typage sécurisé, nous avons conçu un compilateur indépendant du langage basé sur LLVM. Le compilateur prend en entrée une application enrichie de types sécurisés et génère plusieurs partitions pour Intel SGX. Notre évaluation avec des micro- et macro-applications montre que (i) le typage sécurisé peut gérer les pointeurs, les threads multiples et plus de deux partitions, (ii) l’ajout de types sécurisés dans une application héritée est simple, (iii) le typage sécurisé réduit la base de confiance en informatique et est plus efficace que l’incorporation d’une application complète dans une enclave.

Abstract :

For more than twenty years, several tools have been proposed to automatically partition an application between a secure memory zone and a non-secure memory zone. These tools analyze the data flow of the application in order to identify the memory locations that may contain sensitive values. Most of these tools behave incorrectly in the presence of pointers. When they are correct, they are unable to handle threads because of the difficulty to track pointers in a multi-threaded application. The current tools are also unable to split an application in more than two partitions. This is caused by over-approximation, which leads to memory locations falsely shared between the two partitions. In the thesis, instead of starting from data flow analysis, we propose to start from a more accurate technique: language typing. We introduce secure typing, which consists in embedding a partition identifier in the type system of a language. Based on secure typing, we designed a language-agnostic compiler based on LLVM. The compiler takes a legacy application enriched with secure types as input, and generates multiple partitions for Intel SGX. Our evaluation with micro- and macro-applications show that (i) secure typing can handle pointers, multiple threads and more than two partitions, (ii) adding secure types in a legacy application is easy, (iii) secure typing reduces the trusted computing base, and is more efficient than embedding a full application inside an enclave.