Coupled Relational Symbolic Execution for Differential Privacy

TL;DR

This paper introduces a symbolic execution-based method that combines relational reasoning and probabilistic coupling to verify and identify violations of differential privacy in programs.

Contribution

It presents a novel approach that integrates relational reasoning and probabilistic coupling within symbolic execution to improve verification of differential privacy.

Findings

Successfully verifies differential privacy in complex programs.

Identifies privacy violations effectively using the proposed method.

Enhances the reliability of privacy-preserving program analysis.

Abstract

Differential privacy is a de facto standard in data privacy with applications in the private and public sectors. Most of the techniques that achieve differential privacy are based on a judicious use of randomness. However, reasoning about randomized programs is difficult and error prone. For this reason, several techniques have been recently proposed to support designer in proving programs differentially private or in finding violations to it. In this work we propose a technique based on symbolic execution for reasoning about differential privacy. Symbolic execution is a classic technique used for testing, counterexample generation and to prove absence of bugs. Here we use symbolic execution to support these tasks specifically for differential privacy. To achieve this goal, we leverage two ideas that have been already proven useful in formal reasoning about differential privacy: relational reasoning and probabilistic coupling. Our technique integrates these two ideas and shows how such a combination can be used to both verify and find violations to differential privacy.