Reliable and Privacy-Aware Software Systems via Bisimulation Metrics – REPAS

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.