IARCS Verification Seminar Series



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

Speaker: Mahesh Viswanathan    (bio) (bio)


Mahesh Viswanathan is a faculty member at the University of Illinois at Urbana-Champaign. His research interests are in the core areas of logic, automata theory, and algorithm design, with applications to the algorithmic verification of systems. Most recently, his research has been focussed on the dynamic analysis of multi-threaded programs, model checking of cyberphysical systems and stochastic systems, and formal analysis of stochastic security protocols and differential privacy.


When: Tuesday, 04 October 2022 at 1900 hrs (IST)   Slides  Video  

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.

This is joint work with Rohit Chadha and Prasad Sistla.