On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs

TL;DR

This paper presents a linear-time decision procedure for verifying differential privacy in automata models that handle unbounded real-valued query sequences, advancing the understanding of privacy guarantees for complex algorithms.

Contribution

It introduces an automata model for differential privacy mechanisms with unbounded inputs and provides the first decidability results for such algorithms.

Findings

Decidability of differential privacy for automata with unbounded real inputs in linear time.

Identification of a necessary and sufficient graph condition for privacy verification.

First known results on decidability for algorithms with unbounded real-valued query answers.

Abstract

We introduce an automata model for describing interesting classes of differential privacy mechanisms/algorithms that include known mechanisms from the literature. These automata can model algorithms whose inputs can be an unbounded sequence of real-valued query answers. We consider the problem of checking whether there exists a constant $d$ such that the algorithm described by these automata are $d\epsilon$-differentially private for all positive values of the privacy budget parameter $\epsilon$. We show that this problem can be decided in time linear in the automaton's size by identifying a necessary and sufficient condition on the underlying graph of the automaton. This paper's results are the first decidability results known for algorithms with an unbounded number of query answers taking values from the set of reals.