Marco Gaboardi
University of Pennsylvania, Department of Computer and Information Science
Linear Dependent Types for Differential Privacy
Abstract:
Differential privacy
offers a way to answer queries about sensitive information while offering
strong, provable privacy guarantees. Several tools have been developed
for certifying that a given query is differentially private. In one approach,
Reed and Pierce[31] proposed a functional programming language, Fuzz, for
writing differentially private queries. Fuzz uses linear types to track
sensitivity, as well as a probability monad to express randomized computation;
it guarantees that any program that has a certain type is differentially
private. Fuzz can successfully verify many useful queries. However, it fails
when the analysis depends on values that are not known statically.
We present DFuzz, an extension of Fuzz with a combination of linear indexed
types and lightweight dependent types. This combination allows a richer
sensitivity analysis that is able to analyze a larger class of queries,
including queries whose sensitivity depends on runtime information. As in Fuzz,
the differential privacy guarantees follows directly from the soundness theorem
for the type system. We demonstrate the enhanced expressivity of DFuzz by
certifying differential privacy a broad class of iterative algorithms that
could not be typed previously.
Bio:
Marco
Gaboardi is currently a Marie Curie Fellow at the University of Pennsylvania
and at the Università di Bologna (Italy) in the INRIA Focus team. Previously,
he held postdoc positions at the Università di Bologna and at the Università di
Torino (Italy). He received his Ph.D. in Computer Science from Università di
Torino and Institut national polytechnique de Lorraine (France) in 2007.
His research is centered on the use of logic and type theory in the settings of
implicit computational complexity, differential privacy and computation over
streams.
Poster
Host: Frank Pfenning
Appointments: jennsbl@cs.cmu.edu
Monday, October 29, 2012
2:30 p.m.
Gates
& Hillman Centers - 6115
Principles
of Programming Seminars