skip to main content
research-article

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

Published: 14 January 2015 Publication History

Abstract

Mechanism design is the study of algorithm design where the inputs to the algorithm are controlled by strategic agents, who must be incentivized to faithfully report them. Unlike typical programmatic properties, it is not sufficient for algorithms to merely satisfy the property, incentive properties are only useful if the strategic agents also believe this fact.
Verification is an attractive way to convince agents that the incentive properties actually hold, but mechanism design poses several unique challenges: interesting properties can be sophisticated relational properties of probabilistic computations involving expected values, and mechanisms may rely on other probabilistic properties, like differential privacy, to achieve their goals.
We introduce a relational refinement type system, called HOARe2, for verifying mechanism design and differential privacy. We show that HOARe2 is sound w.r.t. a denotational semantics, and correctly models (epsilon,delta)-differential privacy; moreover, we show that it subsumes DFuzz, an existing linear dependent type system for differential privacy. Finally, we develop an SMT-based implementation of HOARe2 and use it to verify challenging examples of mechanism design, including auctions and aggregative games, and new proposed examples from differential privacy.

Supplementary Material

MPG File (p55-sidebyside.mpg)

References

[1]
L. Augustsson. Cayenne -- a language with dependent types. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Baltimore, Maryland, pages 239--250, 1998. URL http://link.springer.com/chapter/10.1007%2F10704973_6.
[2]
M.-F. Balcan, A. Blum, J. D. Hartline, and Y. Mansour. Reducing mechanism design to algorithm design via machine learning. Journal of Computer and System Sciences, 74 (8): 1245--1270, 2008. URL http://www.cs.cmu.edu/ ninamf/papers/ml_md_bbhm.pdf.
[3]
G. Barthe, B. Köpf, F. Olmedo, and S. Zanella-Béguelin. Probabilistic relational reasoning for differential privacy. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, Pennsylvania, pages 97--110, 2012. URL http://certicrypt.gforge.inria.fr/2012.POPL.pdf.
[4]
G. Barthe, C. Fournet, B. Grégoire, P.-Y. Strub, N. Swamy, and S. Zanella-Béguelin. Probabilistic relational verification for cryptographic implementations. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 193--206, 2014. URL http://research.microsoft.com/en-us/um/people/nswamy/papers/rfstar.pdf.
[5]
J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In IEEE Computer Security Foundations Symposium, Pittsburgh, Pennsylvania, 2008. URL http://prosecco.gforge.inria.fr/personal/karthik/pubs/refinement-types-for-secure-implementations-proceedings-csf08.pdf.
[6]
N. Benton. Simple relational correctness proofs for static analyses and program transformations. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Venice, Italy, pages 14--25, 2004. URL http://research.microsoft.com/en-us/um/people/nick/correctnessfull.pdf.
[7]
A. Blum, C. Dwork, F. McSherry, and K. Nissim. Practical privacy: the SuLQ framework. In ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS), Baltimore, Maryland, pages 128--138, 2005. URL http://research.microsoft.com/pubs/64351/bdmn.pdf.
[8]
J. Bornholt, T. Mytkowicz, and K. S. McKinley. Uncertain$łanglet\rangle: A first-order type for uncertain data. In Asian Symposium on Programming Languages and Systems (APLAS), Salt Lake City, Utah, 2014. URL http://research.microsoft.com/pubs/208236/asplos077-bornholtA.pdf.
[9]
E. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23 (5): 552--593, 2013. URL http://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf.
[10]
C. Casinghino, V. Sjöberg, and S. Weirich. Combining proofs and programs in a dependently typed langauge. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, 2014. URL http://www.seas.upenn.edu/ ccasin/papers/combining-TR.pdf.
[11]
T.-H. H. Chan, E. Shi, and D. Song. Private and continual release of statistics. ACM Transactions on Information and System Security, 14 (3): 26, 2011. URL http://eprint.iacr.org/2010/076.pdf.
[12]
S. Chawla, N. Immorlica, and B. Lucier. On the limits of black-box reductions in mechanism design. In ACM SIGACT Symposium on Theory of Computing (STOC), New York, New York, 2012. URL http://arxiv.org/abs/1109.2067.
[13]
R. Cummings, M. Kearns, A. Roth, and Z. S. Wu. Privacy and truthful equilibrium selection for aggregative games. Technical report, 2014. URL http://arxiv.org/abs/1407.7740.
[14]
R. Davies and F. Pfenning. Intersection types and computational effects. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Montréal, Québec, pages 198--208, 2000. URL http://www.cs.cmu.edu/ fp/papers/icfp00.pdf.
[15]
S. Dobzinski and S. Dughmi. On the power of randomization in algorithmic mechanism design. In IEEE Symposium on Foundations of Computer Science (FOCS), Atlanta, Georgia, pages 505--514. URL http://arxiv.org/abs/0904.4193.
[16]
S. Dughmi and T. Roughgarden. Black-box randomized reductions in algorithmic mechanism design. SIAM Journal on Computing, 43 (1): 312--336, 2014. URL http://theory.stanford.edu/ tim/papers/blackbox.pdf.
[17]
J. Dunfield and F. Pfenning. Tridirectional typechecking. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Venice, Italy, pages 281--292. URL http://www.cs.cmu.edu/ joshuad/papers/tridirectional-typechecking/Dunfield04_tridirectional.pdf.
[18]
C. Dwork. Differential privacy. In International Colloquium on Automata, Languages and Programming (ICALP), Venice, Italy, pages 1--12, 2006. URL http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.83.7534&rep=rep1&type=pdf.
[19]
C. Dwork. Differential privacy: A survey of results. In Theory and Applications of Models of Computation (TAMC), Xi'an, China, volume 4978 of LNCS, pages 1--19. Springer Berlin Heidelberg, 2008. URL http://research.microsoft.com/apps/pubs/default.aspx?id=74339.
[20]
C. Dwork, F. McSherry, K. Nissim, and A. Smith. Calibrating noise to sensitivity in private data analysis. In IACR Theory of Cryptography Conference (TCC), New York, New York, pages 265--284, 2006. URL http://dx.doi.org/10.1007/11681878_14.
[21]
Y. Fang, S. Chaudhuri, and M. Vardi. Computer-aided mechanism design, 2014. Poster at POPL'14.
[22]
R. B. Findler and M. Felleisen. Contracts for higher-order functions. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Pittsburgh, Pennsylvania, pages 48--59, 2002. URL http://www.eecs.northwestern.edu/ robby/pubs/papers/ho-contracts-techreport.pdf.
[23]
T. Freeman and F. Pfenning. Refinement types for ML. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, pages 268--277, 1991. URL https://www.cs.cmu.edu/ fp/papers/pldi91.pdf.
[24]
M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce. Linear dependent types for differential privacy. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 357--370, 2013. URL http://dl.acm.org/citation.cfm?id=2429113.
[25]
M. Gaboardi, E. J. Gallego Arias, J. Hsu, A. Roth, and Z. S. Wu. Dual query: Practical private query release for high dimensional data. In International Conference on Machine Learning (ICML), Beijing, China, 2014. URL http://arxiv.org/abs/1402.1526.
[26]
M. Giry. A categorical approach to probability theory. Categorical Aspects of Topology and Analysis, pages 68--85, 1982.
[27]
A. V. Goldberg, J. D. Hartline, A. R. Karlin, M. Saks, and A. Wright. Competitive auctions. Games and Economic Behavior, 55 (2), 2006. URL http://www.ime.usp.br/ yw/papers/games/goldberg2008-competitive-auctions.pdf.
[28]
N. D. Goodman. The principles and practice of probabilistic programming. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 399--402, 2013. URL https://web.stanford.edu/ ngoodman/papers/POPL2013-abstract.pdf.
[29]
A. D. Gordon, T. A. Henzinger, A. V. Nori, and S. K. Rajamani. Probabilistic programming. In International Conference on Software Engineering (ICSE), Hyderabad, India, pages 167--181, 2014. URL http://research.microsoft.com/pubs/208585/fose-icse2014.pdf.
[30]
M. Greenberg, B. C. Pierce, and S. Weirich. Contracts made manifest. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Madrid, Spain, pages 353--364, 2010. URL http://www.cis.upenn.edu/ bcpierce/papers/contracts-popl.pdf.
[31]
J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, pages 93--104, 2006. URL http://galois.com/wp-content/uploads/2014/07/pub_AT_SAGEHybridChecking.pdf.
[32]
J. D. Hartline and B. Lucier. Bayesian algorithmic mechanism design. In ACM SIGACT Symposium on Theory of Computing (STOC), Cambridge, Massachusetts, pages 301--310, 2010. URL http://arxiv.org/abs/0909.4756.
[33]
M. Hicks, G. Bierman, N. Guts, D. Leijen, and N. Swamy. Polymonadic programming. In Workshop on the Mathematical Foundations of Programming Semantics (MFPS), Ithaca, New York, 2014. URL http://arxiv.org/abs/1406.2060.
[34]
ng-Chieh Shan(2009)}Kiselyov:2009O. Kiselyov and Chung-Chieh Shan. Embedded probabilistic programming. In DSL, pages 360--384, 2009.
[35]
A. Lapets, A. Levin, and D. Parkes. A Typed Truthful Language for One-dimensional Truthful Mechanism Design. Technical Report BUCS-TR-2008--026, 2008. URL http://cs-people.bu.edu/lapets/resource/typed-ec-mech.pdf.
[36]
Bride(2005)}epigramC. McBride. Epigram: Practical programming with dependent types. In Advanced Functional Programming, pages 130--170. Springer, 2005. URL http://cs.ru.nl/ freek/courses/tt-2010/tvftl/epigram-notes.pdf.
[37]
009)}mcsherry.pinq09F. McSherry. Privacy integrated queries. In ACM SIGMOD International Conference on Management of Data (SIGMOD), Providence, Rhode Island, 2009. URL http://research.microsoft.com/pubs/80218/sigmod115-mcsherry.pdf.
[38]
F. McSherry and K. Talwar. Mechanism design via differential privacy. In IEEE Symposium on Foundations of Computer Science (FOCS), Providence, Rhode Island, pages 94--103, 2007. URL http://doi.ieeecomputersociety.org/10.1109/FOCS.2007.41.
[39]
P. Milgrom and I. Segal. Deferred-acceptance auctions and radio spectrum reallocation. In ACM SIGecom Conference on Economics and Computation (EC), Palo Alto, California, pages 185--186, 2014. URL http://web.stanford.edu/ isegal/heuristic.pdf.
[40]
m and Nisan(2008)}mu2008truthfulA. Mu'Alem and N. Nisan. Truthful approximation mechanisms for restricted combinatorial auctions. Games and Economic Behavior, 64 (2): 612--631, 2008. URL http://authors.library.caltech.edu/13158/1/MUAgeb08preprint.pdf.
[41]
N. Nisan and A. Ronen. Algorithmic mechanism design. In ACM SIGACT Symposium on Theory of Computing (STOC), Atlanta, Georgia, pages 129--140, 1999. URL http://www.cs.yale.edu/homes/jf/nisan-ronen.pdf.
[42]
N. Nisan, T. Roughgarden, E. Tardos, and V. V. Vazirani. Algorithmic game theory. Cambridge University Press, 2007.
[43]
C.-H. L. Ong and S. J. Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Austin, Texas, volume 46, pages 587--598, 2011. URL https://www.cs.ox.ac.uk/files/3721/main.pdf.
[44]
M. M. Pai and A. Roth. Privacy and mechanism design. ACM SIGecom Exchanges, 12 (1): 8--29, 2013. URL http://www.cis.upenn.edu/ aaroth/Papers/PrivacyMDSurvey.pdf.
[45]
S. Park, F. Pfenning, and S. Thrun. A probabilistic language based upon sampling functions. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Long Beach, California, pages 171--182, 2005. URL https://www.cs.cmu.edu/ fp/papers/popl05.pdf.
[46]
B. C. Pierce. Differential privacy in the programming languages community, 2012. Invited tutorial at DIMACS Workshop on Recent Work on Differential Privacy across Computer Science.
[47]
N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Portland, Oregon, pages 154--165, 2002. URL http://www.cs.tufts.edu/ nr/pubs/pmonad.pdf.
[48]
J. Reed and B. C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Baltimore, Maryland, 2010. URL http://dl.acm.org/citation.cfm?id=1863568.
[49]
P. M. Rondon, M. Kawaguci, and R. Jhala. Liquid types. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Tucson, Arizona, pages 159--169, 2008. URL http://goto.ucsd.edu/ rjhala/papers/liquid_types.pdf.
[50]
I. Roy, S. Setty, A. Kilzer, V. Shmatikov, and E. Witchel. Airavat: Security and privacy for MapReduce. In USENIX Symposium on Networked Systems Design and Implementation (NDSI), San Jose, California, 2010. URL http://dl.acm.org/citation.cfm?id=1855731.
[51]
N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Tokyo, Japan, 2011. URL http://research.microsoft.com/pubs/150012/icfp-camera-ready.pdf.
[52]
Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. Peyton Jones. Refinement Types for Haskell. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Gothenburg, Sweden, 2014. URL http://goto.ucsd.edu/ nvazou/refinement_types_for_haskell.pdf.
[53]
. Vytiniotis, S. Peyton Jones, K. Claessen, and D. Rosén. Halo: Haskell to logic through denotational semantics. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy, 2013. URL http://research.microsoft.com/en-us/people/dimitris/hcc-popl.pdf.
[54]
P. Wadler and R. B. Findler. Well-typed programs can't be blamed. In European Symposium on Programming (ESOP), York, England, pages 1--16, 2009. URL http://homepages.inf.ed.ac.uk/wadler/papers/blame/blame.pdf.
[55]
H. Xi and F. Pfenning. Dependent types in practical programming. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, pages 214--227, 1999. URL http://www.cs.cmu.edu/ fp/papers/popl99.pdf.

Cited By

View all
  • (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
  • (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
  • (2023)Group and Attack: Auditing Differential PrivacyProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3616607(1905-1918)Online publication date: 15-Nov-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
  • Editor:
  • Andy Gill
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    January 2015
    716 pages
    ISBN:9781450333009
    DOI:10.1145/2676726
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 the author(s) 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: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. probabilistic programming
  2. program logics

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)29
  • Downloads (Last 6 weeks)3
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (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
  • (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
  • (2023)Group and Attack: Auditing Differential PrivacyProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3616607(1905-1918)Online publication date: 15-Nov-2023
  • (2019)Type-based complexity analysis of probabilistic functional programsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470193(1-13)Online publication date: 24-Jun-2019
  • (2019)Probabilistic relational reasoning via metricsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470192(1-19)Online publication date: 24-Jun-2019
  • (2019)Approximate span liftingsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470166(1-14)Online publication date: 24-Jun-2019
  • (2019)Encrypted Databases for Differential PrivacyProceedings on Privacy Enhancing Technologies10.2478/popets-2019-00422019:3(170-190)Online publication date: 12-Jul-2019
  • (2019)Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic ProofsJournal of Automated Reasoning10.1007/s10817-019-09530-2Online publication date: 31-Jul-2019
  • (2018)Model Checking Differentially Private PropertiesProgramming Languages and Systems10.1007/978-3-030-02768-1_21(394-414)Online publication date: 22-Oct-2018
  • (2017)Automating Induction for Solving Horn ClausesComputer Aided Verification10.1007/978-3-319-63390-9_30(571-591)Online publication date: 13-Jul-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media