DS0703 -

Des systèmes logiciels fiables et conscients des données privées, via les métriques de bisimulation – REPAS

Résumé de soumission

Les systèmes logiciels sont omniprésents : ils assistent la plupart des activités humaines, et deviennent progressivement l'épine dorsale de nos sociétés. Ils se combinent pour former une structure de plus en plus distribuée et interconnectée, où l'information est échangée, stockée et traitée à une vitesse toujours plus grande. Il est évidemment extrêmement important d'assurer leur fiabilité, c'est-à-dire leur adéquation au comportement attendu d'eux, ainsi que leur sécurité : un programme ne doit pas induire de fuite d'informations sensibles ou confidentielles. Dans ces circonstances, les aspects probabilistes deviennent prépondérants. D'une part, le caractère distribué de ces systèmes fait que calculs et communications dépendent de facteurs non prédictibles, ou trop complexes pour être analysés de façon déterministe. D’autre part, les fuites d’information sont de nature incertaine et correspondent à des corrélations probabilistes entre secrets et informations publiques. Les techniques usuelles de bisimulation, qui ont fait leurs preuves pour démontrer la correction de systèmes (c'est-à-dire le respect d'une spécification par une implémentation) et leur non-interférence (c'est-à-dire l'absence de fuite d'information), ne sont pas adaptées à ce cadre probabiliste car incapables de capturer la dimension quantitative de ces systèmes. Un système peut être acceptable lorsque son comportement est proche, en probabilité, de sa spécification ; et est certainement préférable à un système dont le comportement est toujours incorrect. De plus, il est en pratique impossible d'affirmer avec certitude l'absence de fuites : par exemple, un programme vérifiant un mot de passe révèle de l'information sur celui-ci ne serait-ce qu'en rejetant une suite de caractères erronée, puisqu'il indique ainsi à un adversaire que le mot de passe est différent de cette suite, information qu'il ne possédait peut-être pas encore. Il est donc fondamental de pouvoir quantifier la fuite de données, afin de s’assurer que l'information acquise par l'adversaire, à défaut d'être nulle, reste négligeable. Ce projet vise à développer des notions et des outils quantitatifs adaptés à la preuve de correction de programmes, ainsi qu'à la protection de confidentialité. En particulier, nous nous intéresserons à une extension naturelle de la bisimulation dans un cadre quantitatif : les métriques de bisimulation. Notre application principale sera de développer un mécanisme permettant de protéger la confidentialité d'utilisateurs lorsque leurs positions géographiques sont collectées.

Coordination du projet

Catuscia PALAMIDESSI (Inria - Centre de recherche Saclay - Ile-de-France - Equipe projet COMETE)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

ENS Ecole Normale Supérieure
Inria Saclay - Ile-de-France - équipe COMETE Inria - Centre de recherche Saclay - Ile-de-France - Equipe projet COMETE
LIP - CNRS Laboratoire de l'Informatique du Parallèlisme

Aide de l'ANR 336 392 euros
Début et durée du projet scientifique : septembre 2016 - 48 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter