Featherweight PINQ

TL;DR

Featherweight PINQ is a formal model that captures the core principles of PINQ, ensuring that any program using its API guarantees differential privacy, thus simplifying the design of privacy-preserving data analyses.

Contribution

This work introduces a formal, simplified model of PINQ, proving that all programs interacting with it are differentially private, enhancing understanding and correctness guarantees.

Findings

Featherweight PINQ accurately models PINQ's core features.

All programs using featherweight PINQ's API are differentially private.

The model provides a foundation for verifying privacy guarantees in data analysis systems.

Abstract

Differentially private mechanisms enjoy a variety of composition properties. Leveraging these, McSherry introduced PINQ (SIGMOD 2009), a system empowering non-experts to construct new differentially private analyses. PINQ is an LINQ-like API which provides automatic privacy guarantees for all programs which use it to mediate sensitive data manipulation. In this work we introduce featherweight PINQ, a formal model capturing the essence of PINQ. We prove that any program interacting with featherweight PINQ's API is differentially private.