LightDP：走向自动化的差分隐私证明
LightDP: Towards Automating Differential Privacy Proofs
摘要：
差分隐私在学术和工业环境中的日益普及和采用导致了用于在保护隐私的同时发布信息的日益复杂的算法的发展。伴随这一现象的是不正确算法的开发和出版的自然上升，从而证明了形式化验证工具的必要性。然而，现有的差分隐私形式化方法面临着一个困境：基于定制逻辑的方法可以验证复杂的算法，但学习曲线陡峭，程序员的注释负担很重，而现有的编程平台缺乏对一些复杂算法的表达能力。在本文中，我们提出了LightDP，一个简单的命令式语言，在表达能力和可用性之间取得了更好的平衡。LightDP的核心是一种新型的关系类型系统，它将关系推理与隐私预算计算分离开来。对于依赖类型，类型系统足够强大，可以验证复杂的算法，而组合定理不适用。此外，LightDP的推理引擎可以推断出大部分的证明细节，甚至可以在多个证明存在的情况下搜索具有最小隐私成本约束的证明。我们表明，LightDP验证复杂的算法，几乎没有手动工作。
英文摘要：
The growing popularity and adoption of differential privacy in academic and industrial settings has resulted in the development of increasingly sophisticated algorithms for releasing information while preserving privacy. Accompanying this phenomenon is the natural rise in the development and publication of incorrect algorithms, thus demonstrating the necessity of formal verification tools. However, existing formal methods for differential privacy face a dilemma: methods based on customized logics can verify sophisticated algorithms but come with a steep learning curve and significant annotation burden on the programmers, while existing programming platforms lack expressive power for some sophisticated algorithms. In this paper, we present LightDP, a simple imperative language that strikes a better balance between expressive power and usability. The core of LightDP is a novel relational type system that separates relational reasoning from privacy budget calculations. With dependent types, the type system is powerful enough to verify sophisticated algorithms where the composition theorem falls short. In addition, the inference engine of LightDP infers most of the proof details, and even searches for the proof with minimal privacy cost bound when multiple proofs exist. We show that LightDP verifies sophisticated algorithms with little manual effort.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
