Model Checking Differentially Private Properties

Differential privacy is a framework for designing and analyzing privacy measures, which has become a gold standard in data privacy¹. In this tool, the branching time temporal logic dpCTL is developed for specifying differential privacy. Several differentially private mechanisms are formalized as Markov chains or Markov decision processes. Using formal models, subtle privacy conditions are specified by dpCTL. In order to verify privacy properties automatically, model checking problems are investigated. We implement a model checking algorithm for Markov chains and for MDPs, it’s shown to be undecidable. For more information about the tool and the logic dpCTL, please refer to this paper².

Introduction to the tool

Our tool is built as a plugin of the model checker ePMC, and now is publicly available on GitHub at this repository. It now supports input files consisting of models and properties (both in the standard prism format). For more information on how to use the tool, please refer to this page How to use the tool.

Future work

We have now studied the verification problem of pufferfish privacy³, a more generalized definition which consumes differential privacy. A formalization of the problem models the privacy mechanisms as hidden Markov models and the privacy is checked by computing and comparing the observations distribution from initial pair of information states. We study the complexity of the problem and gives an algorithm which applies SMT solver to solve the verification problem. We also implement the algorithm as a tool FAIER, the pufferFish privAcy verifIER. The tool is to be published soon, though, you can first have a look at this paper⁴.

Contacts

Please refer to the contact page for details on how to contact us.

References