Deciding Differential Privacy of Online Algorithms with Multiple Variables

TL;DR

This paper extends automaton models to analyze the differential privacy of online algorithms with multiple variables, providing a PSPACE-complete decision procedure and practical implementation for verifying privacy guarantees.

Contribution

It generalizes DiP automata to handle multiple real-valued variables and characterizes the class of differentially private automata, with a PSPACE-complete decision algorithm.

Findings

PSPACE-complete complexity for privacy verification

Algorithm computes privacy budget factor when private

Implementation demonstrates practical effectiveness

Abstract

We consider the problem of checking the differential privacy of online randomized algorithms that process a stream of inputs and produce outputs corresponding to each input. This paper generalizes an automaton model called DiP automata (See arXiv:2104.14519) to describe such algorithms by allowing multiple real-valued storage variables. A DiP automaton is a parametric automaton whose behavior depends on the privacy budget $\epsilon$. An automaton $A$ will be said to be differentially private if, for some $\mathfrak{D}$, the automaton is $\mathfrak{D}\epsilon$-differentially private for all values of $\epsilon>0$. We identify a precise characterization of the class of all differentially private DiP automata. We show that the problem of determining if a given DiP automaton belongs to this class is PSPACE-complete. Our PSPACE algorithm also computes a value for $\mathfrak{D}$ when the given automaton is differentially private. The algorithm has been implemented, and experiments demonstrating its effectiveness are presented.