在隐马尔可夫模型中验证 Pufferfish 隐私

Pufferfish 是一种用于设计与分析隐私机制的贝叶斯隐私框架。它改进了当前数据隐私的黄金标准——差分隐私，通过在隐私分析中允许显式先验知识。通过这些隐私框架，文献中已提出若干隐私机制。在实践中，隐私机制常需针对特定应用进行修改或调整，其隐私风险须针对不同环境重新评估。此外，计算设备仅能通过浮点计算近似连续噪声，而浮点计算本质上是离散的。因此隐私证明可能复杂且易错。此类繁琐任务对普通数据管理者而言是负担。本文提出一种 Pufferfish 隐私的自动验证技术。我们使用隐马尔可夫模型来规约与分析离散化 Pufferfish 隐私机制。我们证明隐马尔可夫模型中的 Pufferfish 验证问题是 NP 难的。利用可满足性模理论（SMT）求解器，我们提出一种分析隐私需求的算法。我们在名为 FAIER 的原型工具中实现了该算法，并给出了若干案例研究。令人惊讶的是，案例研究表明，对成熟隐私机制的朴素离散化常会失效，FAIER 生成的 counterexamples（反例）证实了这一点。在离散化 \emph{Above Threshold} 中，我们表明其导致绝对无隐私。最后，我们在若干案例上将本方法与基于测试的方法比较，并显示我们的验证技术可与基于测试的方法结合以用于（i）高效认证反例与（ii）获得隐私预算 $\epsilon$ 的更优下界。