Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Tue 20 Aug 2019 10:52 - 11:15 at Aurora Borealis - Program Analysis & Synthesis Chair(s): Daniel Winograd-Cort

Curators of sensitive datasets sometimes need to know whether queries against the data are {\em differentially private}. Two sorts of logics have been proposed for checking this property: (1) {\em type systems} and other static analyses, which fully automate straightforward reasoning with concepts like program sensitivity'' andprivacy loss,'' and (2) full-blown program logics such as apRHL (an approximate, probabilistic, relational Hoare logic), which support more flexible reasoning about subtle privacy-preserving algorithmic techniques but offer only minimal automation.

We propose a {\em three-level logic} for differential privacy in an imperative setting and present a prototype implementation called Fuzzi. Fuzzi’s lowest level is a general-purpose logic; its middle level is apRHL; and its top level is a novel {\em sensitivity logic} adapted from the linear-logic-inspired type system of Fuzz, a differentially private functional language. The key novelty is a high degree of integration between the sensitivity logic and the two lower-level logics: the judgments and proofs of the sensitivity logic can be easily translated into apRHL; conversely, privacy properties of key algorithmic building blocks can be proved manually in apRHL and the base logic, then packaged up as typing rules that can be applied by a checker for the sensitivity logic to automatically construct privacy proofs for composite programs of arbitrary size.

We demonstrate Fuzzi’s utility by implementing four different private machine-learning algorithms and showing that Fuzzi’s checker is able to derive tight sensitivity bounds.

Conference Day
Tue 20 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00
Program Analysis & SynthesisResearch Papers at Aurora Borealis
Chair(s): Daniel Winograd-CortTarget Corp
10:30
22m
Talk
Relational Cost Analysis for Functional-Imperative Programs
Research Papers
Weihao QuUniversity at Buffalo, SUNY, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems
10:52
22m
Talk
Fuzzi: A Three-Level Logic for Differential Privacy
Research Papers
Hengchu ZhangUniversity of Pennsylvania, Edo RothUniversity of Pennsylvania, Andreas HaeberlenUniversity of Pennsylvania, USA, Benjamin C. PierceUniversity of Pennsylvania, Aaron RothUniversity of Pennsylvania, USA
11:15
22m
Talk
Synthesizing Differentially Private Programs
Research Papers
Calvin SmithUniversity of Wisconsin - Madison, Aws AlbarghouthiUniversity of Wisconsin-Madison
11:37
22m
Talk
Synthesizing Symmetric Lenses
Research Papers
Anders MiltnerPrinceton University, Solomon MainaUniversity of Pennsylvania, Kathleen FisherTufts University, USA, Benjamin C. PierceUniversity of Pennsylvania, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania
Pre-print