More Web Proxy on the site http://driver.im/

research-article

Linear dependent types for differential privacy

Authors:

Marco Gaboardi,

Andreas Haeberlen,

Benjamin C. PierceAuthors Info & Claims

ACM SIGPLAN Notices, Volume 48, Issue 1

Pages 357 - 370

https://doi.org/10.1145/2480359.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

Lobo-Vesga ERusso AGaboardi MCortiñas C(2024)Sensitivity by ParametricityProceedings of the ACM on Programming Languages10.1145/36897268:OOPSLA2(415-441)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689726
Liu DWang BFu CZhang L(2023)Model checking differentially private propertiesTheoretical Computer Science10.1016/j.tcs.2022.10.002943(153-170)Online publication date: Jan-2023
https://doi.org/10.1016/j.tcs.2022.10.002
Chadha RSistla AViswanathan MGorla D(2021)On linear time decidability of differential privacy for programs with unbounded inputsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470708(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470708
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

LightDP: towards automating differential privacy proofs
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

The growing popularity and adoption of differential privacy in academic and industrial settings has resulted in the development of increasingly sophisticated algorithms for releasing information while preserving privacy. Accompanying this phenomenon is ...
Linear dependent types for differential privacy
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

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

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

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

150
Total Citations
View Citations
1,001
Total Downloads

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

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lobo-Vesga ERusso AGaboardi MCortiñas C(2024)Sensitivity by ParametricityProceedings of the ACM on Programming Languages10.1145/36897268:OOPSLA2(415-441)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689726
Liu DWang BFu CZhang L(2023)Model checking differentially private propertiesTheoretical Computer Science10.1016/j.tcs.2022.10.002943(153-170)Online publication date: Jan-2023
https://doi.org/10.1016/j.tcs.2022.10.002
Chadha RSistla AViswanathan MGorla D(2021)On linear time decidability of differential privacy for programs with unbounded inputsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470708(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470708
Pistone PGorla D(2021)On generalized metric spaces for the simply typed lambda-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470696(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470696
Lobo-Vesga EJuristo N(2021)Let's not make a fuzz about itProceedings of the 43rd International Conference on Software Engineering: Companion Proceedings10.1109/ICSE-Companion52605.2021.00051(114-116)Online publication date: 25-May-2021
https://dl.acm.org/doi/10.1109/ICSE-Companion52605.2021.00051
Farina GChong SGaboardi M(2021)Coupled Relational Symbolic Execution for Differential PrivacyProgramming Languages and Systems10.1007/978-3-030-72019-3_8(207-233)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_8
Zhang HRoth EHaeberlen APierce BRoth A(2020)Testing differential privacy with dual interpretersProceedings of the ACM on Programming Languages10.1145/34282334:OOPSLA(1-26)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428233
Tao YHe XMachanavajjhala ARoy SMaier DPottinger RDoan ATan WAlawini ANgo H(2020)Computing Local Sensitivities of Counting Queries with JoinsProceedings of the 2020 ACM SIGMOD International Conference on Management of Data10.1145/3318464.3389762(479-494)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3318464.3389762
Johnson NNear JHellerstein JSong D(2020)Chorus: a Programming Framework for Building Scalable Differential Privacy Mechanisms2020 IEEE European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP48549.2020.00041(535-551)Online publication date: Sep-2020
https://doi.org/10.1109/EuroSP48549.2020.00041
Li TJiang JQi JSo CMa JChen XShen TCui HWang YWang P(2020)UPA: An Automated, Accurate and Efficient Differentially Private Big-Data Mining System2020 50th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)10.1109/DSN48063.2020.00064(515-527)Online publication date: Jun-2020
https://doi.org/10.1109/DSN48063.2020.00064
Show More Cited By

View Options

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 Issue’s Table of Contents