POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 17:20 - 17:45 at Auditorium - Security and Privacy Chair(s): Cătălin Hriţcu

The growing populariy 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 comes with a steep learning curve and significant annotation burden on the programmers; while existing type systems lacks expressiveness for some sophisticated algorithms. In this paper, we present AutoPriv, a simple imperative language that strikes a better balance between expressive power and usefulness. The core of AutoPriv 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 AutoPriv infers most of the proof details, and even searches for the proof with minimal privacy cost when multiple proofs exist. We show that AutoPriv verifies sophisticated algorithms with little manual effort.

Fri 20 Jan
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 17:45: POPL - Security and Privacy at Auditorium
Chair(s): Cătălin HriţcuInria Paris
POPL-2017-papers16:30 - 16:55
Nada AminEPFL, Tiark RompfPurdue University
POPL-2017-papers16:55 - 17:20
Mounir AssafStevens Institute of Technology, David NaumannStevens Institute of Technology, Julien SignolesCEA LIST, Éric TotelCentraleSupélec, Frédéric TronelCentraleSupélec
POPL-2017-papers17:20 - 17:45
Danfeng ZhangPennsylvania State University, Daniel KiferDept. of Computer Science and Engineering, Penn State University