Verifying Pufferfish Privacy in Hidden Markov Models
summary
Proposes encoding discrete privacy mechanisms as hidden Markov models and reduces Pufferfish verification to SMT solving, proving the decision problem NP-hard. Implements the algorithm in the tool FAIER and reports concrete failures: naive discretization of Laplace to truncated geometric breaks guarantees (example: only log4 privacy in a family scenario), and discrete Above Threshold gives no privacy, with SMT-produced counterexamples and a combined testing+verification workflow to tighten epsilon bounds.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:00Privacy
- 1:48Differential Privacy
- 3:28Privacy Limits
- 4:08Example
- 5:05Pufferfish Privacy
- 7:27Main Contributions
- 8:25Running Example
- 9:45Markov Chain Model
- 11:10Hidden Markov Models
- 12:52State Distributions
- 18:18Observation Sequence Omega
- 20:49Evaluation
- 21:44Results
- 23:52Conclusion
related talks
39mPufferfish Privacy Mechanisms for Correlated Data
43mPufferfish Privacy Mechanisms for Correlated Data
58mFormal Methods and Proofs of Privacy Properties, Part I
01h 02mFormal Methods and Proofs of Privacy Properties, Part III
56mFormal Methods and Proofs of Privacy Properties, Part II
48mFormal Modelling of Information-flow Control Systems: Some Lessons Learned
16mBalancing Privacy: Leveraging Privacy Budgets for Privacy-Enhancing Technologies
38mDemystifying Privacy Preserving Computing