The French National Research Agency Projects for science

Voir cette page en français

ANR funded project

(DS0703) 2016
Projet REPAS

Reliable and Privacy-Aware Software Systems via Bisimulation Metrics

Software systems are everywhere: they support most of the human activities and are becoming the backbone of our society. They form a more and more distributed and interconnected structure, where information is exchanged, stored and processed at an ever-increasing rate. Naturally, it is extremely important to ensure their reliability, namely their correctness with respect to the expected behavior, and their security, namely the absence of leaks of sensitive or private information. In this context, probabilistic aspects become crucial: On one hand, due to the distributed nature of these systems, computation and communication involve factors that are unpredictable or too complicated to analyse deterministically. On the other hand, the leakage of information depends on the probabilistic knowl edge of the adversary and is best formalized in terms of probabilistic correlation between secret and public information. Traditional bisimulation techniques, that have successfully been employed to prove correctness (equivalence of the implementation w.r.t. a specification) and non-interference (absence of information leaks), become inadequate in this probabilistic scenario, because unable to capture the quantitative dimension: a system whose behavior is probabilistically close to a specification can be acceptable, and is definitely better than a system which always behaves incorrectly. Furthermore, it is usually impossible to guarantee absolute absence of leaks in practice. For instance, a password- checking program leaks information about the password even when denying access to an attacker that enters a wrong sequence of characters, since the adversary now knows that the password is a different sequence. It is therefore fundamental to be able to express leakage in quantitative terms so to ensure that the information obtained by the adversary, if not zero, is at least very small.
In this project, we aim at investigating quantitative notions and tools for proving program correctness and protecting privacy. In particular, we will focus on bisimulation metrics, which are the natural extension of bisimulation on quantitative systems. As a key application, we will develop a mechanism to protect the privacy of users when their location traces are collected.


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

ANR grant: 336 393 euros
Beginning and duration: octobre 2016 - 48 mois


ANR Programme: (DS0703) 2016

Project ID: ANR-16-CE25-0011

Project coordinator:
Madame Catuscia Palamidessi (Inria - Centre de recherche Saclay - Ile-de-France - Equipe projet COMETE)


Back to the previous page


The project coordinator is the author of this abstract and is therefore responsible for the content of the summary. The ANR disclaims all responsibility in connection with its content.