research-article

Linear dependent types for differential privacy

Authors:

Marco Gaboardi,

Andreas Haeberlen,

Benjamin C. PierceAuthors Info & Claims

POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 357 - 370

https://doi.org/10.1145/2429069.2429113

Published: 23 January 2013 Publication History

Abstract

Differential privacy offers a way to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the query's result. Proving that a given query has this property involves establishing a bound on the query's sensitivity---how much its result can change when a single record is added or removed.

A variety of tools have been developed for certifying that a given query differentially private. In one approach, Reed and Pierce [34] proposed a functional programming language, Fuzz, for writing differentially private queries. Fuzz uses linear types to track sensitivity and a probability monad to express randomized computation; it guarantees that any program with a certain type is differentially private. Fuzz can successfully verify many useful queries. However, it fails when the sensitivity analysis depends on values that are not known statically.

We present DFuzz, an extension of Fuzz with a combination of linear indexed types and lightweight dependent types. This combination allows a richer sensitivity analysis that is able to certify a larger class of queries as differentially private, including ones whose sensitivity depends on runtime information. As in Fuzz, the differential privacy guarantee follows directly from the soundness theorem of the type system. We demonstrate the enhanced expressivity of DFuzz by certifying differential privacy for a broad class of iterative algorithms that could not be typed previously.

Supplementary Material

JPG File (r2d2_talk4.jpg)

Download
17.90 KB

MP4 File (r2d2_talk4.mp4)

Download
185.29 MB

References

[1]

M. S. Alvim, M. E. Andres, K. Chatzikokolakis, and C. Palamidessi. On the relation between Differential Privacy and Quantitative Information Flow. In Proc. ICALP, 2011.

Digital Library

[2]

G. Barthe and B. Köpf. Information-theoretic Bounds for Differentially Private Mechanisms. In Proc. CSF, 2011.

Digital Library

[3]

G. Barthe, B. Kopf, F. Olmedo, and S. Zanella Beguelin. Probabilistic relational reasoning for differential privacy. In Proc. POPL, 2012.

Digital Library

[4]

A. Blum, C. Dwork, F. McSherry, and K. Nissim. Practical privacy: the SuLQ framework. In Proc. PODS, 2005.

Digital Library

[5]

K. Chaudhuri, C. Monteleoni, and A. D. Sarwate. Differentially private empirical risk minimization. J. Mach. Learn. Res., 12:1069--1109, July 2011.

Digital Library

[6]

S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. NavidPour. Proving programs robust. In Proc. FSE, 2011.

Digital Library

[7]

C. Chen and H. Xi. Combining programming with theorem proving. In Proc. ICFP, pages 66--77, 2005.

Digital Library

[8]

U. Dal Lago and M. Gaboardi. Linear dependent types and relative completeness. In IEEE LICS '11, pages 133--142, 2011.

Digital Library

[9]

U. Dal Lago and M. Hofmann. Bounded linear logic, revisited. In TLCA, volume 5608 of LNCS, pages 80--94. Springer, 2009.

Digital Library

[10]

N. Dalvi, C. Ré, and D. Suciu. Probabilistic databases: diamonds in the dirt. Commun. ACM, 52(7):86--94, 2009.

Digital Library

[11]

L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. TACAS, 2008.

Digital Library

[12]

C. Dwork. Differential privacy. In Proc. ICALP, 2006.

Digital Library

[13]

C. Dwork, F. McSherry, K. Nissim, and A. Smith. Calibrating noise to sensitivity in private data analysis. In Proc. TCC, 2006.

Digital Library

[14]

M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce. Linear dependent types for differential privacy (extended version). http://privacy.cis.upenn.edu/papers/dfuzz-long.pdf.

[15]

J. Girard. Linear logic. Theor. Comp. Sci., 50(1):1--102, 1987.

Digital Library

[16]

J. Girard, A. Scedrov, and P. Scott. Bounded linear logic. Theoretical Computer Science, 97(1):1--66, 1992.

Digital Library

[17]

T. J. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Proc. PODS, 2007.

Digital Library

[18]

A. Gupta, K. Ligett, F. McSherry, A. Roth, and K. Talwar. Differentially private combinatorial optimization. In Proc. SODA, 2010.

Digital Library

[19]

A. Gupta, A. Roth, and J. Ullman. Iterative constructions and private data release. In Proc. TCC, 2012.

Digital Library

[20]

A. Haeberlen, B. C. Pierce, and A. Narayan. Differential privacy under fire. In Proc. USENIX Security, 2011.

Digital Library

[21]

S. Hayashi. Singleton, union and intersection types for program extraction. In Proc. TACS, volume 526 of LNCS, pages 701--730. Springer Berlin / Heidelberg, 1991.

Digital Library

[22]

S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, and A. Smith. What can we learn privately? In Proc. FOCS, Oct. 2008.

Digital Library

[23]

N. R. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially substructural types. In Proc. ICFP, 2012.

Digital Library

[24]

N. Li, T. Li, and S. Venkatasubramanian. t-closeness: Privacy beyond k-anonymity and l-diversity. In Proc. ICDE, 2007.

[25]

A. Machanavajjhala, D. Kifer, J. Abowd, J. Gehrke, and L. Vilhuber. Privacy: Theory meets practice on the map. In Proc. ICDE, 2008.

Digital Library

[26]

F. McSherry. Privacy integrated queries: an extensible platform for privacy-preserving data analysis. In Proc. SIGMOD, 2009.

Digital Library

[27]

F. McSherry and R. Mahajan. Differentially-private network trace analysis. In Proc. SIGCOMM, 2010.

Digital Library

[28]

F. McSherry and K. Talwar. Mechanism design via differential privacy. In Proc. FOCS, 2007.

Digital Library

[29]

P. Mohan, A. Thakurta, E. Shi, D. Song, and D. Culler. GUPT: privacy preserving data analysis made easy. In Proc. SIGMOD, 2012.

Digital Library

[30]

A. Narayanan and V. Shmatikov. Robust de-anonymization of large sparse datasets. In Proc. IEEE S&P, 2008.

Digital Library

[31]

C. Palamidessi and M. Stronati. Differential privacy for relational algebra: Improving the sensitivity bounds via constraint systems. In Proc. QAPLS, volume 85 of EPTCS, pages 92--105, 2012.

[32]

N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In Proc. POPL, 2002.

Digital Library

[33]

J. Reed, M. Gaboardi, and B. C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy (extended version). http://privacy.cis.upenn.edu/papers/fuzz-long.pdf.

[34]

J. Reed and B. C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy. In Proc. ICFP, Sept. 2010.

Digital Library

[35]

A. Roth and T. Roughgarden. The median mechanism: Interactive and efficient privacy with multiple queries. In Proc. STOC, 2010.

[36]

I. Roy, S. T. V. Setty, A. Kilzer, V. Shmatikov, and E.Witchel. Airavat: security and privacy for MapReduce. In Proc. NSDI, 2010.

Digital Library

[37]

D. Walker. Advanced Topics in Types and Programming Languages, chapter Substructural Type Systems. The MIT Press, 2005.

[38]

H. Xi and F. Pfenning. Dependent types in practical programming. In Proc. POPL, 1999.

Digital Library

[39]

L. Xu. Modular reasoning about differential privacy in a probabilistic process calculus. Manuscript, 2012.

[40]

B. A. Yorgey, S.Weirich, J. Cretin, S. Peyton Jones, D. Vytiniotis, and J. P. M. es. Giving Haskell a promotion. In Proc. TLDI, 2012.

Digital Library

Cited By

Kellison AHsu J(2024)Numerical Fuzz: A Type System for Rounding Error AnalysisProceedings of the ACM on Programming Languages10.1145/36564568:PLDI(1954-1978)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656456
Toro MOlmedo FTanter É(2024)Gradual Differentially Private ProgrammingCommunications of the ACM10.1145/365332867:8(49-53)Online publication date: 18-Jul-2024
https://dl.acm.org/doi/10.1145/3653328
Oakley LHoltzen SOprea A(2024)Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00048(449-463)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00048
Show More Cited By

Index Terms

Linear dependent types for differential privacy
1. Software and its engineering
  1. Software notations and tools
    1. Context specific languages
      1. Specialized application languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Distance makes the types grow stronger: a calculus for differential privacy
ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming

We want assurances that sensitive information will not be disclosed when aggregate data derived from a database is published. Differential privacy offers a strong statistical guarantee that the effect of the presence of any individual in a database will ...
Linear dependent types for differential privacy
POPL '13

Differential privacy offers a way to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the ...
Cayenne—a language with dependent types

Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value, and types of record components (which can be types or values) ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2013

586 pages

ISBN:9781450318327

DOI:10.1145/2429069

General Chair:
Roberto Giacobazzi
Università di Verona, Italy
,
Program Chair:
Radhia Cousot
École normale supérieure CNRS & INRIA, France

ACM SIGPLAN Notices Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '13

Sponsor:

SIGPLAN

POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 23 - 25, 2013

Rome, Italy

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

150
Total Citations
View Citations
995
Total Downloads

Downloads (Last 12 months)59
Downloads (Last 6 weeks)4

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kellison AHsu J(2024)Numerical Fuzz: A Type System for Rounding Error AnalysisProceedings of the ACM on Programming Languages10.1145/36564568:PLDI(1954-1978)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656456
Toro MOlmedo FTanter É(2024)Gradual Differentially Private ProgrammingCommunications of the ACM10.1145/365332867:8(49-53)Online publication date: 18-Jul-2024
https://dl.acm.org/doi/10.1145/3653328
Oakley LHoltzen SOprea A(2024)Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00048(449-463)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00048
Vasilenko EVazou NBarthe G(2024)OBRA: Oracle-Based, Relational, Algorithmic Type VerificationProgramming Languages and Systems10.1007/978-981-97-8943-6_14(283-302)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_14
Bell ZGoldwasser SKim MWatson J(2024)Certifying Private Probabilistic MechanismsAdvances in Cryptology – CRYPTO 202410.1007/978-3-031-68391-6_11(348-386)Online publication date: 18-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-68391-6_11
Colledan ADal Lago U(2024)Circuit Width Estimation via Effect Typing and Linear DependencyProgramming Languages and Systems10.1007/978-3-031-57267-8_1(3-30)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_1
Pillutla KAndrew GKairouz PMcMahan HOprea AOh SOh ANaumann TGloberson ASaenko KHardt MLevine S(2023)Unleashing the power of randomization in auditing differentially private MLProceedings of the 37th International Conference on Neural Information Processing Systems10.5555/3666122.3669012(66201-66238)Online publication date: 10-Dec-2023
https://dl.acm.org/doi/10.5555/3666122.3669012
Pettersson MLjung Ekeroth JRusso A(2023)Calculating Function Sensitivity for Synthetic Data AlgorithmsProceedings of the 35th Symposium on Implementation and Application of Functional Languages10.1145/3652561.3652567(1-12)Online publication date: 29-Aug-2023
https://dl.acm.org/doi/10.1145/3652561.3652567
Haeberlen APhan LMcGuire M(2023)Metaverse as a ServiceProceedings of the 2023 ACM Symposium on Cloud Computing10.1145/3620678.3624662(298-307)Online publication date: 30-Oct-2023
https://dl.acm.org/doi/10.1145/3620678.3624662
Rasifard HGopinath RBackes MNemati HRanise SCarbone RTakabi D(2023)SEAL: Capability-Based Access Control for Data-Analytic ScenariosProceedings of the 28th ACM Symposium on Access Control Models and Technologies10.1145/3589608.3593838(67-78)Online publication date: 24-May-2023
https://dl.acm.org/doi/10.1145/3589608.3593838
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents