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

research-article

Proving differential privacy with shadow execution

Authors:

Danfeng ZhangAuthors Info & Claims

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 655 - 669

https://doi.org/10.1145/3314221.3314619

Published: 08 June 2019 Publication History

Abstract

Recent work on formal verification of differential privacy shows a trend toward usability and expressiveness -- generating a correctness proof of sophisticated algorithm while minimizing the annotation burden on programmers. Sometimes, combining those two requires substantial changes to program logics: one recent paper is able to verify Report Noisy Max automatically, but it involves a complex verification system using customized program logics and verifiers.

In this paper, we propose a new proof technique, called shadow execution, and embed it into a language called ShadowDP. ShadowDP uses shadow execution to generate proofs of differential privacy with very few programmer annotations and without relying on customized logics and verifiers. In addition to verifying Report Noisy Max, we show that it can verify a new variant of Sparse Vector that reports the gap between some noisy query answers and the noisy threshold. Moreover, ShadowDP reduces the complexity of verification: for all of the algorithms we have evaluated, type checking and verification in total takes at most 3 seconds, while prior work takes minutes on the same algorithms.

Supplementary Material

WEBM File (p655-wang.webm)

Download
80.82 MB

References

[1]

John M. Abowd. 2018. The U.S. Census Bureau Adopts Differential Privacy. In Proceedings of the 24th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD '18). ACM, New York, NY, USA, 2867-2867.

Digital Library

[2]

Aws Albarghouthi and Justin Hsu. 2017. Synthesizing Coupling Proofs of Differential Privacy. Proceedings of ACM Programming Languages 2, POPL, Article 58 (Dec. 2017), 30 pages.

Digital Library

[3]

Gilles Barthe, George Danezis, Benjamin Gregoire, Cesar Kunz, and Santiago Zanella-Beguelin. 2013. Verified Computational Differential Privacy with Applications to Smart Metering. In Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium (CSF '13). IEEE Computer Society, Washington, DC, USA, 287-301.

Digital Library

[4]

Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. 2004. Secure Information Flow by Self-Composition. In Proceedings of the 17th IEEE Workshop on Computer Security Foundations (CSFW '04). IEEE Computer Society, Washington, DC, USA, 100-.

Digital Library

[5]

Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. Advanced Probabilistic Couplings for Differential Privacy. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS '16). ACM, New York, NY, USA, 55-67.

Digital Library

[6]

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub. 2014. Proving Differential Privacy in Hoare Logic. In Proceedings of the 2014 IEEE 27th Computer Security Foundations Symposium (CSF '14). IEEE Computer Society, Washington, DC, USA, 411-424.

Digital Library

[7]

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 2015. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15). ACM, New York, NY, USA, 55-68.

Digital Library

[8]

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. Proving Differential Privacy via Probabilistic Couplings. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '16). ACM, New York, NY, USA, 749-758.

Digital Library

[9]

Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. 2012. Probabilistic Relational Reasoning for Differential Privacy. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '12). ACM, New York, NY, USA, 97-110.

Digital Library

[10]

Gilles Barthe and Federico Olmedo. 2013. Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences Between Probabilistic Programs. In Proceedings of the 40th International Conference on Automata, Languages, and Programming - Volume Part II (ICALP'13). Springer-Verlag, Berlin, Heidelberg, 49-60.

Digital Library

[11]

Dirk Beyer and M. Erkan Keremoglu. 2011. CPACHECKER: A Tool for Configurable Software Verification. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11). Springer-Verlag, Berlin, Heidelberg, 184-190.

Digital Library

[12]

Benjamin Bichsel, Timon Gehr, Dana Drachsler-Cohen, Petar Tsankov, and Martin Vechev. 2018. DP-Finder: Finding Differential Privacy Violations by Sampling and Optimization. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS '18). ACM, New York, NY, USA, 508-524.

Digital Library

[13]

Mark Bun and Thomas Steinke. 2016. Concentrated Differential Privacy: Simplifications, Extensions, and Lower Bounds. In Proceedings, Part I, of the 14th International Conference on Theory of Cryptography - Volume 9985. Springer-Verlag New York, Inc., New York, NY, USA, 635-658.

Digital Library

[14]

Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. 2012. SMTInterpol: An Interpolating SMT Solver. In Proceedings of the 19th International Conference on Model Checking Software (SPIN'12). Springer-Verlag, Berlin, Heidelberg, 248-254.

Digital Library

[15]

Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. 2013. The MathSAT5 SMT Solver. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13). Springer-Verlag, Berlin, Heidelberg, 93-107.

Digital Library

[16]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08/ETAPS'08). Springer-Verlag, Berlin, Heidelberg, 337-340.

Digital Library

[17]

Zeyu Ding, Yuxin Wang, Guanhong Wang, Danfeng Zhang, and Daniel Kifer. 2018. Detecting Violations of Differential Privacy. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS '18). ACM, New York, NY, USA, 475-489.

Digital Library

[18]

Cynthia Dwork, Krishnaram Kenthapadi, Frank McSherry, Ilya Mironov, and Moni Naor. 2006. Our Data, Ourselves: Privacy via Distributed Noise Generation. In Proceedings of the 24th Annual International Conference on The Theory and Applications of Cryptographic Techniques (EUROCRYPT'06). Springer-Verlag, Berlin, Heidelberg, 486-503.

Digital Library

[19]

Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith. 2006. Calibrating Noise to Sensitivity in Private Data Analysis. In Theory of Cryptography, Shai Halevi and Tal Rabin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 265-284.

Digital Library

[20]

Cynthia Dwork, Aaron Roth, et al. 2014. The algorithmic foundations of differential privacy. Theoretical Computer Science 9, 3-4 (2014), 211-407.

Digital Library

[21]

Hamid Ebadi, David Sands, and Gerardo Schneider. 2015. Differential Privacy: Now It's Getting Personal. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15). ACM, New York, NY, USA, 69-81.

Digital Library

[22]

Úlfar Erlingsson, Vasyl Pihur, and Aleksandra Korolova. 2014. RAPPOR: Randomized Aggregatable Privacy-Preserving Ordinal Response. In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security (CCS '14). ACM, New York, NY, USA, 1054-1067.

Digital Library

[23]

Gian Pietro Farina, Stephen Chong, and Marco Gaboardi. 2017. Relational Symbolic Execution. arXiv e-prints, Article arXiv:1711.08349 (Nov 2017).

[24]

Anna C. Gilbert and Audra McMillan. 2018. Property Testing For Differential Privacy. 2018 56th Annual Allerton Conference on Communication, Control, and Computing (Allerton) (2018), 249-258.

[25]

Moritz Hardt, Katrina Ligett, and Frank McSherry. 2012. A Simple and Practical Algorithm for Differentially Private Data Release. In Proceedings of the 25th International Conference on Neural Information Processing Systems - Volume 2 (NIPS'12). Curran Associates Inc., USA, 2339-2347.

Digital Library

[26]

Sebastian Hunt and David Sands. 2006. On Flow-sensitive Security Types. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '06). ACM, New York, NY, USA, 79-90.

Digital Library

[27]

Noah Johnson, Joseph P Near, and Dawn Song. 2018. Towards practical differential privacy for SQL queries. Proceedings of the VLDB Endowment 11, 5 (2018), 526-539.

Digital Library

[28]

Dexter Kozen. 1981. Semantics of probabilistic programs. J. Comput. System Sci. 22, 3 (1981), 328-350.

[29]

Min Lyu, Dong Su, and Ninghui Li. 2017. Understanding the sparse vector technique for differential privacy. Proceedings of the VLDB Endowment 10, 6 (2017), 637-648.

Digital Library

[30]

Frank McSherry and Kunal Talwar. 2007. Mechanism Design via Differential Privacy. In Proceedings of the 48th Annual IEEE Symposium on Foundations of Computer Science (FOCS '07). IEEE Computer Society, Washington, DC, USA, 94-103.

Digital Library

[31]

Frank D. McSherry. 2009. Privacy Integrated Queries: An Extensible Platform for Privacy-preserving Data Analysis. In Proceedings of the 2009 ACM SIGMOD International Conference on Management of Data (SIGMOD '09). ACM, New York, NY, USA, 19-30.

Digital Library

[32]

I. Mironov. 2017. Rényi Differential Privacy. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 263-275.

[33]

Prashanth Mohan, Abhradeep Thakurta, Elaine Shi, Dawn Song, and David Culler. 2012. GUPT: Privacy Preserving Data Analysis Made Easy. In Proceedings of the 2012 ACM SIGMOD International Conference on Management of Data (SIGMOD '12). ACM, New York, NY, USA, 349-360.

Digital Library

[34]

Kobbi Nissim, Thomas Steinke, Alexandra Wood, Micah Altman, Aaron Bembenek, Mark Bun, Marco Gaboardi, David R O'Brien, and Salil Vadhan. 2017. Differential privacy: A primer for a non-technical audience. In Privacy Law Scholars Conf.

[35]

Indrajit Roy, Srinath T. V. Setty, Ann Kilzer, Vitaly Shmatikov, and Emmett Witchel. 2010. Airavat: Security and Privacy for MapReduce. In Proceedings of the 7th USENIX Conference on Networked Systems Design and Implementation (NSDI'10). USENIX Association, Berkeley, CA, USA, 20-20.

Digital Library

[36]

Andrei Sabelfeld and Andrew C Myers. 2003. Language-based information-flow security. IEEE Journal on selected areas in communications 21, 1 (2003), 5-19.

Digital Library

[37]

Apple Differential Privacy Team. 2017. Learning with Privacy at Scale. Apple Machine Learning Journal 1, 8 (2017).

[38]

Tachio Terauchi and Alex Aiken. 2005. Secure information flow as a safety problem. In International Static Analysis Symposium. Springer, 352-367.

Digital Library

[39]

Michael Carl Tschantz, Dilsun Kaynar, and Anupam Datta. 2011. Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract). Electronic Notes in Theoretical Computer Science 276 (Sept. 2011), 61-79.

Digital Library

[40]

Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, and Danfeng Zhang. 2019. Proving Differential Privacy with Shadow Execution. arXiv e-prints, Article arXiv:1903.12254 (Mar 2019).

[41]

Lili Xu, Konstantinos Chatzikokolakis, and Huimin Lin. 2014. Metrics for Differential Privacy in Concurrent Systems. In Formal Techniques for Distributed Objects, Components, and Systems, Erika Ábrahám and Catuscia Palamidessi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 199-215.

[42]

Danfeng Zhang and Daniel Kifer. 2017. LightDP: Towards Automating Differential Privacy Proofs. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, New York, NY, USA, 888-901.

Digital Library

[43]

Dan Zhang, Ryan McKenna, Ios Kotsogiannis, Michael Hay, Ashwin Machanavajjhala, and Gerome Miklau. 2018. EKTELO: A Framework for Defining Differentially-Private Computations. In Proceedings of the 2018 International Conference on Management of Data (SIGMOD '18). ACM, New York, NY, USA, 115-130.

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
Zhang YLiang XDu RTian J(2024)DP-Discriminator: A Differential Privacy Evaluation Tool Based on GANProceedings of the 21st ACM International Conference on Computing Frontiers10.1145/3649153.3649211(285-293)Online publication date: 7-May-2024
https://dl.acm.org/doi/10.1145/3649153.3649211
Lu YMagdon-Ismail MWei YZikas V(2024)Eureka: A General Framework for Black-box Differential Privacy Estimators2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00166(913-931)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00166
Show More Cited By

Index Terms

Proving differential privacy with shadow execution
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

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 ...
CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security

We propose CheckDP, an automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample generators have failed. ...
Detecting Violations of Differential Privacy
CCS '18: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security

The widespread acceptance of differential privacy has led to the publication of many sophisticated algorithms for protecting privacy. However, due to the subtle nature of this privacy definition, many such algorithms have bugs that make them violate ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2019

1162 pages

ISBN:9781450367127

DOI:10.1145/3314221

General Chair:
Kathryn S. McKinley
Google, USA
,
Program Chair:
Kathleen Fisher
Tufts University, USA

Copyright © 2019 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 June 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '19

Sponsor:

SIGPLAN

PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 22 - 26, 2019

AZ, Phoenix, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
410
Total Downloads

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

Reflects downloads up to 11 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
Zhang YLiang XDu RTian J(2024)DP-Discriminator: A Differential Privacy Evaluation Tool Based on GANProceedings of the 21st ACM International Conference on Computing Frontiers10.1145/3649153.3649211(285-293)Online publication date: 7-May-2024
https://dl.acm.org/doi/10.1145/3649153.3649211
Lu YMagdon-Ismail MWei YZikas V(2024)Eureka: A General Framework for Black-box Differential Privacy Estimators2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00166(913-931)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00166
Kutta TAskin ÖDunsche M(2024)Lower Bounds for Rényi Differential Privacy in a Black-Box Setting2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00134(951-971)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00134
Künnemann RPatrignani MCecchetti E(2024)Computationally Bounded Robust Compilation and Universally Composable Security2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00024(265-278)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00024
Toro MDarais DAbuah CNear JÁrquez DOlmedo FTanter É(2023)Contextual Linear Types for Differential PrivacyACM Transactions on Programming Languages and Systems10.1145/358920745:2(1-69)Online publication date: 17-May-2023
https://dl.acm.org/doi/10.1145/3589207
Chadha RSistla AViswanathan MBhusal BMeng WJensen CCremers CKirda E(2023)Deciding Differential Privacy of Online Algorithms with Multiple VariablesProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623170(1761-1775)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623170
Abuah CDarais DNear J(2022)Solo: a lightweight static analysis for differential privacyProceedings of the ACM on Programming Languages10.1145/35633136:OOPSLA2(699-728)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563313
Askin ÖKutta TDette H(2022)Statistical Quantification of Differential Privacy: A Local Approach2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833689(402-421)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833689
Ding ZWang YXiao YWang GZhang DKifer D(2022)Free gap estimates from the exponential mechanism, sparse vector, noisy max and related algorithmsThe VLDB Journal — The International Journal on Very Large Data Bases10.1007/s00778-022-00728-232:1(23-48)Online publication date: 16-Feb-2022
https://dl.acm.org/doi/10.1007/s00778-022-00728-2
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 Table of Contents