隐马尔可夫模型中的河豚隐私
Verifying Pufferfish Privacy in Hidden Markov Models
摘要：
Pufferfish是一个贝叶斯隐私框架，用于设计和分析隐私机制。它改进了差分隐私，目前的黄金标准，在数据隐私，允许明确的先验知识的隐私分析。通过这些隐私框架，在文献中已经开发了许多隐私机制。在实践中，隐私机制往往需要修改或调整，以适应特定的应用。他们的隐私风险必须根据不同的情况重新评估。此外，计算设备仅通过浮点计算来近似连续噪声，这在本质上是离散的。因此，隐私证明可能很复杂，容易出错。这些繁琐的任务对于普通数据管理员来说可能是沉重的负担。在本文中，我们提出了一个自动验证技术的河豚隐私。我们使用隐马尔可夫模型来指定和分析离散河豚隐私机制。我们证明了隐马尔可夫模型中的河豚验证问题是NP难的。利用可满足性模理论求解器，我们提出了一个算法来分析隐私需求。我们实现我们的算法在一个原型工具称为FAIER，并提出了几个案例研究。令人惊讶的是，我们的案例研究表明，成熟的隐私机制的天真离散化往往会失败，FAIER生成的反例证明了这一点。在离散的\emph{Above Threshold}，我们表明，它的结果在绝对没有隐私。最后，我们比较我们的方法与基于测试的方法在几个案例研究，并表明，我们的验证技术可以与基于测试的方法相结合的目的（i）有效地证明反例和（ii）获得更好的下限的隐私预算$ε$。
英文摘要：
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. Through these privacy frameworks, a number of privacy mechanisms have been developed in literature. In practice, privacy mechanisms often need be modified or adjusted to specific applications. Their privacy risks have to be re-evaluated for different circumstances. Moreover, computing devices only approximate continuous noises through floating-point computation, which is discrete in nature. Privacy proofs can thus be complicated and prone to errors. Such tedious tasks can be 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 discretized Pufferfish privacy mechanisms. We show that the Pufferfish verification problem in hidden Markov models is NP-hard. Using Satisfiability Modulo Theories solvers, we propose an algorithm to analyze privacy requirements. We implement our algorithm in a prototypical tool called FAIER, and present several case studies. Surprisingly, our case studies show that naïve discretization of well-established privacy mechanisms often fail, witnessed by counterexamples generated by FAIER. In discretized \emph{Above Threshold}, we show that it results in absolutely no privacy. Finally, we compare our approach with testing based approach on several case studies, and show that our verification technique can be combined with testing based approach for the purpose of (i) efficiently certifying counterexamples and (ii) obtaining a better lower bound for the privacy budget $ε$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
