Marco Gaboardi
Andreas Haeberlen
Arjun Narayan
Benjamin C. Pierce
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.
Supplemental Material
- 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. Google Scholar
Digital Library
- G. Barthe and B. Köpf. Information-theoretic Bounds for Differentially Private Mechanisms. In Proc. CSF, 2011. Google ScholarDigital Library
- G. Barthe, B. Kopf, F. Olmedo, and S. Zanella Beguelin. Probabilistic relational reasoning for differential privacy. In Proc. POPL, 2012. Google ScholarDigital Library
- A. Blum, C. Dwork, F. McSherry, and K. Nissim. Practical privacy: the SuLQ framework. In Proc. PODS, 2005. Google ScholarDigital Library
- K. Chaudhuri, C. Monteleoni, and A. D. Sarwate. Differentially private empirical risk minimization. J. Mach. Learn. Res., 12:1069--1109, July 2011. Google ScholarDigital Library
- S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. NavidPour. Proving programs robust. In Proc. FSE, 2011. Google ScholarDigital Library
- C. Chen and H. Xi. Combining programming with theorem proving. In Proc. ICFP, pages 66--77, 2005. Google ScholarDigital Library
- U. Dal Lago and M. Gaboardi. Linear dependent types and relative completeness. In IEEE LICS '11, pages 133--142, 2011. Google ScholarDigital Library
- U. Dal Lago and M. Hofmann. Bounded linear logic, revisited. In TLCA, volume 5608 of LNCS, pages 80--94. Springer, 2009. Google ScholarDigital Library
- N. Dalvi, C. Ré, and D. Suciu. Probabilistic databases: diamonds in the dirt. Commun. ACM, 52(7):86--94, 2009. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. TACAS, 2008. Google ScholarDigital Library
- C. Dwork. Differential privacy. In Proc. ICALP, 2006. Google ScholarDigital Library
- C. Dwork, F. McSherry, K. Nissim, and A. Smith. Calibrating noise to sensitivity in private data analysis. In Proc. TCC, 2006. Google ScholarDigital Library
- 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.Google Scholar
- J. Girard. Linear logic. Theor. Comp. Sci., 50(1):1--102, 1987. Google ScholarDigital Library
- J. Girard, A. Scedrov, and P. Scott. Bounded linear logic. Theoretical Computer Science, 97(1):1--66, 1992. Google ScholarDigital Library
- T. J. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Proc. PODS, 2007. Google ScholarDigital Library
- A. Gupta, K. Ligett, F. McSherry, A. Roth, and K. Talwar. Differentially private combinatorial optimization. In Proc. SODA, 2010. Google ScholarDigital Library
- A. Gupta, A. Roth, and J. Ullman. Iterative constructions and private data release. In Proc. TCC, 2012. Google ScholarDigital Library
- A. Haeberlen, B. C. Pierce, and A. Narayan. Differential privacy under fire. In Proc. USENIX Security, 2011. Google ScholarDigital Library
- S. Hayashi. Singleton, union and intersection types for program extraction. In Proc. TACS, volume 526 of LNCS, pages 701--730. Springer Berlin / Heidelberg, 1991. Google ScholarDigital Library
- S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, and A. Smith. What can we learn privately? In Proc. FOCS, Oct. 2008. Google ScholarDigital Library
- N. R. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially substructural types. In Proc. ICFP, 2012. Google ScholarDigital Library
- N. Li, T. Li, and S. Venkatasubramanian. t-closeness: Privacy beyond k-anonymity and l-diversity. In Proc. ICDE, 2007.Google ScholarCross Ref
- A. Machanavajjhala, D. Kifer, J. Abowd, J. Gehrke, and L. Vilhuber. Privacy: Theory meets practice on the map. In Proc. ICDE, 2008. Google ScholarDigital Library
- F. McSherry. Privacy integrated queries: an extensible platform for privacy-preserving data analysis. In Proc. SIGMOD, 2009. Google ScholarDigital Library
- F. McSherry and R. Mahajan. Differentially-private network trace analysis. In Proc. SIGCOMM, 2010. Google ScholarDigital Library
- F. McSherry and K. Talwar. Mechanism design via differential privacy. In Proc. FOCS, 2007. Google ScholarDigital Library
- P. Mohan, A. Thakurta, E. Shi, D. Song, and D. Culler. GUPT: privacy preserving data analysis made easy. In Proc. SIGMOD, 2012. Google ScholarDigital Library
- A. Narayanan and V. Shmatikov. Robust de-anonymization of large sparse datasets. In Proc. IEEE S&P, 2008. Google ScholarDigital Library
- 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.Google Scholar
- N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In Proc. POPL, 2002. Google ScholarDigital Library
- 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.Google Scholar
- J. Reed and B. C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy. In Proc. ICFP, Sept. 2010. Google ScholarDigital Library
- A. Roth and T. Roughgarden. The median mechanism: Interactive and efficient privacy with multiple queries. In Proc. STOC, 2010.Google Scholar
- I. Roy, S. T. V. Setty, A. Kilzer, V. Shmatikov, and E.Witchel. Airavat: security and privacy for MapReduce. In Proc. NSDI, 2010. Google ScholarDigital Library
- D. Walker. Advanced Topics in Types and Programming Languages, chapter Substructural Type Systems. The MIT Press, 2005.Google Scholar
- H. Xi and F. Pfenning. Dependent types in practical programming. In Proc. POPL, 1999. Google ScholarDigital Library
- L. Xu. Modular reasoning about differential privacy in a probabilistic process calculus. Manuscript, 2012.Google Scholar
- 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. Google ScholarDigital Library
Index Terms
- Linear dependent types for differential privacy
Recommendations
Distance makes the types grow stronger: a calculus for differential privacy
ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programmingWe 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 '13Differential 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