Accueil > Manifestations > Thèses et HDR > Thèses > Ronan-Alexandre Cherruau

Ronan-Alexandre Cherruau

Directeur de thèse

Mario Südholt

Résumé

Grâce à l’informatique en nuage, les services de l’information occupent un rôle prépondérant dans la société moderne (clients pour les courriers électroniques, réseaux sociaux, services de stockage). Un rôle qui exige d’être intransigeant avec la sécurité de l’information puisque ces services génèrent et sauvegardent des
données qui constituent la vie privée numérique des utilisateurs.

Un service du nuage peut employer des techniques de sécurités pour assurer la sécurité de l’information. Ces techniques protègent une donnée personnelle en la rendant inintelligible pour toutes personnes autres que l’utilisateur du service. En contrepartie, certaines fonctionnalités ne peuvent plus être implémentées. Par exemple, la technique du chiffrement symétrique rend les données inintelligibles,
mais empêche le calcul sur ces données.

Cette thèse avance qu’un service du nuage doit *composer* les techniques pour assurer la sécurité de l’information sans perdre de fonctionnalités. Elle se base sur l’étude de la composition de trois techniques qui sont le chiffrement, la fragmentation verticale et les calculs côté client. Cette étude montre que la composition sécurise sans perdre de fonctionnalités, mais complexifie l’écriture du
service. La thèse propose alors un nouveau langage pour l’écriture de services du nuage qui assurent la sécurité des données personnelles par compositions des techniques de sécurité. Ce langage est muni de lois algébriques pour dériver, systématiquement, un service local sans protection vers son équivalent sécurisé du nuage. Le langage est implémenté en Idris et profite de son système de type expressif pour vérifier la composition correcte des techniques de cryptographie. Dans
le même temps, une transformation traduit le langage en ProVerif, un vérificateur de modèle pour l’analyse automatique des propriétés de sécurité sur les protocoles cryptographiques. Cette traduction vérifie alors la sécurité des données personnelles dans le service.

Mots clefs :

Vie privée, confidentialité, informatique en nuage, chiffrement, fragmentation verticale, calculs côté client, langage de programmation, Idris, lois algébriques, vérification automatique, ProVerif.

Abstract :

In the context of cloud computing, information services are ever-present (web-based email client, social networks, file hosting). Such services yield personal data that constitutes the privacy of the client and therefore, should be uncompromising on information privacy.

A cloud service can use security techniques to ensure information privacy. These techniques protect privacy by converting the client’s personal data into unintelligible text. But they can also cause the loss of some functionalities of the service. For instance, a symmetric-key cipher protects privacy by converting readable personal
data into unreadable one. However, this causes the loss of computational functionalities on this data.

This thesis claims that a cloud service has to *compose* security techniques to ensure information privacy without the loss of functionalities. This claim is based on the study of the composition of three techniques : symmetric cipher, vertical data fragmentation and client-side computation. This study shows that the composition makes the service privacy preserving, but makes its formulation overwhelming. In response, the thesis offers a new language for the writing of cloud services that enforces information privacy using the composition of security techniques. This language comes with a set of algebraic laws to systematically transform a local service without protection into its cloud equivalent protected by composition. An
Idris implementation harnesses the Idris expressive type system to ensure the correct composition of security techniques. Furthermore, a transformation translates the language into ProVerif, a model checker for automated reasoning about the security properties found in cryptographic protocols. This translations checks that the service preserves the privacy of its client.

Key words :

Privacy, information privacy, cloud computing, encryption, data fragmentation, client-side computation, programming language, Idris, algebraic laws, automatique vérification, ProVerif.

Composition du jury :

  • Wolfgang De Meuter, Full Professor, Vrije Universiteit Brussel, Rapporteur
  • Ludovic Mé, Professeur, CentraleSupélec, Rapporteur
  • Claude Jard, Professeur, Université de Nantes, Examinateur
  • Yves Roudier, Professeur, Sophia antipolis, Examinateur
  • Anderson Santana de Oliveira, Chercheur, SAP Labs, Examinateur
  • Mario Südholt, Professeur, Mines-Nantes, Directeur de thèse

Dernière modification : jeudi 10 novembre 2016