Tue 25 Jun 2019 10:20 - 10:40 at 224AB - Type Systems II Chair(s): Jeffrey S. Foster

Recent work on formal verification of differential privacy shows a trend toward usability and expressiveness – generating a correctness proof of sophisticated algorithm while minimizing the annotation burden on programmers. Sometimes, combining those two requires substantial changes to program logics: one recent paper is able to verify Report Noisy Max automatically, but it involves a complex verification system using customized program logics and verifiers.

In this paper, we propose a new proof technique, called shadow execution, and embed it into a language called ShadowDP. ShadowDP uses shadow execution to generate proofs of differential privacy with very few programmer annotations and without relying on customized logics and verifiers. In addition to verifying Report Noisy Max, we show that it can verify a new variant of Sparse Vector that reports the gap between some noisy query answers and the noisy threshold. Moreover, ShadowDP reduces the complexity of verification: for all of the algorithms we have evaluated, type checking and verification in total takes at most 3 seconds, while prior work takes minutes on the same algorithms.

Conference Day
Tue 25 Jun

Displayed time zone: Tijuana, Baja California change

10:00 - 11:00
Type Systems IIPLDI Research Papers at 224AB
Chair(s): Jeffrey S. FosterTufts University
10:00
20m
Talk
ILC: A Calculus for Composable, Computational Cryptography
PLDI Research Papers
Kevin Liao, Matthew HammerNone, Andrew MillerUniversity of Illinois at Urbana-Champaign, USA
10:20
20m
Talk
Proving Differential Privacy with Shadow Execution
PLDI Research Papers
Yuxin Wang, Zeyu DingPennsylvania State University, USA, Guanhong WangPennsylvania State University, USA, Daniel KiferDept. of Computer Science and Engineering, Penn State University, Danfeng ZhangPennsylvania State University
Media Attached
10:40
20m
Talk
Data-Trace Types for Distributed Stream Processing Systems
PLDI Research Papers
Konstantinos MamourasUniversity of Pennsylvania, Caleb StanfordUniversity of Pennsylvania, Rajeev AlurUniversity of Pennsylvania, Zachary G. IvesUniversity of Pennsylvania, Val TannenUniversity of Pennsylvania, USA
Media Attached