Duet: An Expressive Higher-Order Language and Linear Type System for Statically Enforcing Differential Privacy
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 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.
Wed 23 Oct Times are displayed in time zone: Beirut change
14:00 - 15:30 | |||
14:00 22mTalk | Duet: An Expressive Higher-Order Language and Linear Type System for Statically Enforcing Differential Privacy OOPSLA Joseph P. NearUniversity of Vermont, David DaraisUniversity of Vermont, Chike AbuahUniversity of Vermont, Tim StevensUniversity of Vermont, Pranav GaddamaduguUniversity of California, Berkeley, Lun WangUniversity of California, Berkeley, Neel SomaniUniversity of California, Berkeley, Mu ZhangUniversity of Utah, Nikhil SharmaUniversity of California, Berkeley, Alex ShanUniversity of California, Berkeley, Dawn SongUniversity of California, Berkeley DOI | ||
14:22 22mTalk | Improving Bug Detection via Context-Based Code Representation Learning and Attention-Based Neural Networks OOPSLA Yi LiNew Jersey Institute of Technology, USA, Shaohua WangNew Jersey Institute of Technology, USA, Tien N. NguyenUniversity of Texas at Dallas, Son NguyenThe University of Texas at Dallas DOI | ||
14:45 22mTalk | Probabilistic Verification of Fairness Properties via Concentration OOPSLA Osbert BastaniUniversity of Pennsylvania, Xin ZhangMassachusetts Institute of Technology, Armando Solar-LezamaMassachusetts Institute of Technology DOI | ||
15:07 22mTalk | Generating Precise Error Specifications for C: A Zero Shot Learning Approach OOPSLA Baijun WuUniversity of Louisiana at Lafayette, John Peter CamporaUniversity of Louisiana at Lafayette, He YiUniversity of Louisiana at Lafayette, Alexander SchlechtUniversity of Louisiana at Lafayette, Sheng ChenUniversity of Louisiana at Lafayette DOI |