Verifying Pufferfish Privacy in Hidden Markov ModelsRemote
Pufferfish is a Bayesian privacy framework for designing and analyzing privacy mechanisms. It refines differential privacy, the current gold standard in data privacy, by allowing explicit prior knowledge in privacy analysis. In practice, privacy mechanisms often need be modified or adjusted to specific applications. Their privacy risks have to be re-evaluated for different circumstances. Privacy proofs can thus be complicated and prone to errors. Such tedious tasks are burdensome to average data curators. In this paper, we propose an automatic verification technique for Pufferfish privacy. We use hidden Markov models to specify and analyze discrete mechanisms in Pufferfish privacy. We show that the Pufferfish verification problem in hidden Markov models is NP-hard. Using Satisfiability Modulo Theories solvers, we propose an algorithm to verify privacy requirements. We implement our algorithm in a prototypical tool called FAIER, and analyze several classic privacy mechanisms in Pufferfish privacy. Surprisingly, our analysis show that naive discretization of well-established privacy mechanisms often fails, witnessed by counterexamples generated by FAIER. In discrete Above Threshold, we show that it results in absolutely no privacy. Finally, we compare our approach with state-of-the-art tools for differential privacy, and show that our verification technique can be efficiently combined with these tools for the purpose of certifying counterexamples and finding a more precise lower bound for the privacy budget $epsilon$.
Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 14:30 | Privacy and SecurityVMCAI at Salon I Chair(s): Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences | ||
13:30 30mPaper | Verifying Pufferfish Privacy in Hidden Markov ModelsRemote VMCAI Depeng Liu Institute of Software, Chinese Academy of Sciences, Bow-Yaw Wang Academia Sinica, Lijun Zhang Institute of Software, Chinese Academy of Sciences | ||
14:00 30mPaper | Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACERemote VMCAI Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Jorge A. Navas Certora, inc., Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys, Arie Gurfinkel University of Waterloo |