EBSIS Summer School
on Distributed Event Based Systems
and Related Topics 2017

July 10—14, 2017 – Timmendorfer Strand, Germany

★ Lecture Abstract

Verifying Differential Privacy in Concurrent Systems

Catuscia Palamidessi (Inria)

Differential Privacy (DP) is one of the most successful approaches to prevent disclosure of private information in statistical databases. It provides a formal privacy guarantee, ensuring that sensitive information relative to individuals cannot be easily inferred by disclosing answers to aggregate queries. If two databases are adjacent, i.e. differ only for the value of an individual's data, then the query should not allow to tell them apart by more than a certain factor. This induces a bound also on the distinguishability of two generic databases, which is determined by their distance on the Hamming graph of the adjacency relation. Recently, we have proposed a generalized version of DP that can be applied to arbitrary metric domains, by expressing the indistinguishability requirement in terms of a bound on the given distance.

In this talk, we consider the problem of verifying that two probabilistic concurrent processes that differ for the value of a secret satisfy (generalized) DP, i.e., they give raise to observable traces whose distance does not exceed the required bound. To this purpose, we consider an extension of the Bisimulation Metrics based on the Kantorovich distance. However, the standard Kantorovich lifting is additive, while DP is multiplicative. We therefore explore a generalized notion of Kantorovich lifting, suitable for arbitrary metric domains, and therefore also for the generalized DP. We show that the standard results extend smoothly to the generalized case, and that a bound on the generalized bisimulation distance is also a bound for the distance on traces, which guarantees the soundness of the method for proving DP. Finally, we explore a Hennessy-Milner-like logical characterization of our bisimulation distance, and we show how it can be used for reasoning about DP.

Speaker Bio

Catuscia Palamidessi is Director of Research at INRIA Saclay, where she leads the team COMETE. She got her PhD from the University of Pisa in 1988. She held Full Professor positions at the University of Genova, Italy (1994-1997) and at the Pennsylvania State University, USA (1998-2002). Catuscia Palamidessi's research interests include Privacy, Secure Information Flow, and Concurrency. Her past achievements include the proof of expressiveness gaps between various concurrent calculi, and the development of a probabilistic version of the asynchronous pi-calculus. More recently, she has contributed to establish the foundations of probabilistic secure information flow, she has proposed an extension of differential privacy, and geo-indistinguishability, an approach to location privacy.