
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsCryptography and Data Security · Privacy-Preserving Technologies in Data · Security and Verification in Computing
