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.

Tue 20 Aug

icfp-2019-papers
10:30 - 12:00: Research Papers - Program Analysis & Synthesis at Aurora Borealis
Chair(s): Daniel Winograd-CortTarget Corp
icfp-2019-papers10:30 - 10:52
Talk
Weihao QuUniversity at Buffalo, SUNY, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems
icfp-2019-papers10:52 - 11:15
Talk
Hengchu ZhangUniversity of Pennsylvania, Edo RothUniversity of Pennsylvania, Andreas HaeberlenUniversity of Pennsylvania, USA, Benjamin C. PierceUniversity of Pennsylvania, Aaron RothUniversity of Pennsylvania, USA
icfp-2019-papers11:15 - 11:37
Talk
Calvin SmithUniversity of Wisconsin - Madison, Aws AlbarghouthiUniversity of Wisconsin-Madison
icfp-2019-papers11:37 - 12:00
Talk
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