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.

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

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