DUET: An Expressive Higher-Order Language and Linear Type System for Statically Enforcing Differential Privacy
DUET: An Expressive Higher-Order Language and Linear Type System for Statically Enforcing Differential Privacy
复制标题
DOI：
10.1145/3360598
复制
发表时间：
2019-10-01
影响因子：
1.8
通讯作者：
Song, Dawn
中科院分区：
文献类型：
--
作者：
Near, Joseph P.;Darais, David;Song, Dawn
在过去的十年中，差异隐私已经成为保护个人隐私的黄金标准。然而，验证特定程序提供差异隐私通常仍然是由该领域的专家完成的手动任务。已经提出了通过类型系统设计完全自动化差分隐私证明的基于数据的技术，但是这些结果落后于差分隐私算法的进展，在可以自动验证的程序中留下了明显的差距，同时也提供了最先进的隐私边界。我们提出DUET，一种表达性更高的高阶语言，用于自动验证通用高阶程序的差分隐私的线性型系统和工具。除了通用编程，DUET还支持编码机器学习算法，如随机梯度下降，以及常见的辅助数据分析任务，如裁剪，归一化和超参数调整-其中每一个都特别具有挑战性，在静态验证的差分隐私框架中编码。我们提出了DUET语言和线性类型系统的核心设计，并为类型良好的程序提供完整的关于隐私的密钥证明。然后，我们将展示如何扩展DUET，以支持现实的机器学习应用程序和最近的差异隐私的变种，从而提高了许多实际的差异隐私算法的准确性。最后，我们在DUET中实现了几种差异化的私有机器学习算法，这些算法以前从未被基于语言的工具自动验证过，我们提出的实验结果证明了DUET语言设计在训练机器学习模型的准确性方面的好处。
During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by an expert in the field. Language-based techniques have been proposed for fully automating proofs of differential privacy via type system design, however these results have lagged behind advances 172 in differentially-private algorithms, leaving a noticeable gap in programs which can be automatically verified while also providing state-of-the-art bounds on privacy.We propose DUET, an expressive higher-order language, linear type system and tool for automatically verifying differential privacy of general-purpose higher-order programs. In addition to general purpose programming, DUET supports encoding machine learning algorithms such as stochastic gradient descent, as well as common auxiliary data analysis tasks such as clipping, normalization and hyperparameter tuning-each of which are particularly challenging to encode in a statically verified differential privacy framework.We present a core design of the DUET language and linear type system, and complete key proofs about privacy for well-typed programs. We then show how to extend DUET to support realistic machine learning applications and recent variants of differential privacy which result in improved accuracy for many practical differentially private algorithms. Finally, we implement several differentially private machine learning algorithms in DUET which have never before been automatically verified by a language-based tool, and we present experimental results which demonstrate the benefits of DUET'S language design in terms of accuracy of trained machine learning models.