论文标题
与差异隐私的耦合关系符号执行
Coupled Relational Symbolic Execution for Differential Privacy
论文作者
论文摘要
差异隐私是私人和公共部门的应用程序的事实上的数据隐私标准。获得差异隐私的大多数技术都是基于明智地使用随机性的。但是，关于随机程序的推理很困难且容易出错。因此，最近提出了几种技术来支持设计师以私密的方式证明程序或发现违规行为。在这项工作中，我们提出了一种基于符号执行的技术，以推理差异隐私。符号执行是一种经典技术，用于测试，反例生成和证明没有错误。在这里，我们使用符号执行来专门为差异隐私提供支持。为了实现这一目标，我们利用已经被证明对差异隐私的正式推理有用的两个想法：关系推理和概率耦合。我们的技术整合了这两个想法，并展示了如何使用这种组合来验证和发现侵犯差异隐私的行为。
Differential privacy is a de facto standard in data privacy with applications in the private and public sectors. Most of the techniques that achieve differential privacy are based on a judicious use of randomness. However, reasoning about randomized programs is difficult and error prone. For this reason, several techniques have been recently proposed to support designer in proving programs differentially private or in finding violations to it. In this work we propose a technique based on symbolic execution for reasoning about differential privacy. Symbolic execution is a classic technique used for testing, counterexample generation and to prove absence of bugs. Here we use symbolic execution to support these tasks specifically for differential privacy. To achieve this goal, we leverage two ideas that have been already proven useful in formal reasoning about differential privacy: relational reasoning and probabilistic coupling. Our technique integrates these two ideas and shows how such a combination can be used to both verify and find violations to differential privacy.
