On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs
This provides the first decidability results for verifying differential privacy in algorithms with an unbounded number of real-valued query answers, addressing a key challenge in privacy-preserving data analysis.
The paper tackles the problem of verifying differential privacy for algorithms with unbounded real-valued inputs by introducing an automata model and showing that checking for a constant d such that the algorithm is dε-differentially private can be decided in linear time relative to the automaton's size.
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ε$-differentially private for all positive values of the privacy budget parameter $ε$. 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.