AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
While it is invaluable to formally verify correct differentially-private algorithms, we believe that it is important to detect incorrect algorithms and provide counterexamples for them, due to the subtleties involved in algorithm development

Detecting Violations of Differential Privacy.

ACM Conference on Computer and Communications Security, pp.475-489, (2018)

Cited by: 73|Views480
EI

Abstract

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 their claimed privacy. In this paper, we consider the problem of producing counterexamples...More

Code:

Data:

Introduction
  • Differential privacy has become a de facto standard for extracting information from a dataset while protecting the confidentiality of individuals whose data are collected
  • Implemented correctly, it guarantees that any individual’s record has very little influence on the output of the algorithm.
  • There are two main approaches to tackling this prevalence of bugs: programming platforms and verification
  • Programming platforms, such as PINQ [29], Airavat [37], and GUPT [32] provide a small set of primitive operations that can be used as building blocks of algorithms for differential privacy.
  • The authors write D1 ∼ D2 to mean that D1 is adjacent to D2
Highlights
  • Differential privacy has become a de facto standard for extracting information from a dataset while protecting the confidentiality of individuals whose data are collected
  • It treats programs as semi-black-boxes and uses statistical tests to detect violations of differential privacy. We evaluate our counterexample generator on a variety of sophisticated differentially private algorithms and their common incorrect variations
  • While it is invaluable to formally verify correct differentially-private algorithms, we believe that it is important to detect incorrect algorithms and provide counterexamples for them, due to the subtleties involved in algorithm development
  • We proposed a novel semi-black-box method of evaluating differentially private algorithms, and providing counterexamples for those incorrect ones
  • We show that within a few seconds, our tool correctly rejects incorrect algorithms and provides counterexamples for them
  • This will require additional extensions such as a more refined use of program analysis techniques that reason about what happens when a program is run on adjacent databases
Methods
  • The authors implemented the counterexample detection framework with all components, including hypothesis test, event selector and input generator.
  • The tool takes in an algorithm implementation and the desired privacy bound ε0, and generates counterexamples if the algorithm does not satisfy ε0-differential privacy.
  • 5.1 Noisy Max. Report Noisy Max reports which one among a list of counting queries has the largest value.
  • The correct versions have been proven to satisfy ε0-differential privacy [19] no matter how long the input list is.
  • A naive proof would show that it satisfies (ε0 · |Q |/2)-differential privacy, but a clever proof shows that it satisfies ε0-differential privacy
Conclusion
  • CONCLUSIONS AND FUTURE

    WORK

    While it is invaluable to formally verify correct differentially-private algorithms, the authors believe that it is important to detect incorrect algorithms and provide counterexamples for them, due to the subtleties involved in algorithm development.
  • The authors proposed a novel semi-black-box method of evaluating differentially private algorithms, and providing counterexamples for those incorrect ones.
  • Future work includes extensions that detect violations of differential privacy even if those violations occur with extremely small probabilities.
  • This will require additional extensions such as a more refined use of program analysis techniques that reason about what happens when a program is run on adjacent databases.
  • Additional extensions include counterexample generation for other variants of differential privacy, such as approximate differential privacy, zCDP, and renyi-differential privacy
Tables
  • Table1: Database categories and samples
  • Table2: Counterexamples detected for incorrect privacy mechanisms
  • Table3: Time spent on running tool for different algorithms
Download tables as Excel
Related work
  • Differential privacy. The term differential privacy covers a family of privacy definitions that include pure ε-differential privacy (the topic of this paper) [17] and its relaxations: approximate (ε, δ )differential privacy [16], concentrated differential privacy [8, 20], and Renyi differential privacy [31]. The pure and approximate versions have received the most attention from algorithm designers (e.g., see the book [19]). However, due to the lack of availability of easy-to-use debugging and verification tools, a considerable fraction of published algorithms are incorrect. In this paper, we focus on algorithms for which there is a public record of an error (e.g., variants of the sparse vector method [12, 28]) or where a seemingly small change to an algorithm breaks an important component of the algorithm (e.g., variants of the noisy max algorithm [5, 19] and the histogram algorithm [14]).

    Programming platforms and verification tools. Several dynamic tools [21, 29, 37, 39, 40] exist for enforcing differential privacy. Those tools track the privacy budget consumption at runtime, and terminates a program when the intended privacy budget is exhausted. On the other hand, static methods exist for verifying that a program obeys differential privacy during any execution, based on relational program logic [1,2,3,4,5,6,7] and relational type system [24, 35, 41]. We note that those methods are largely orthogonal to this paper: their goal is to verify a correct program or to terminate an incorrect one, while our goal is to detect an incorrect program and generate counterexamples for it. The counterexamples provide valuable guidance for fixing incorrect algorithms for algorithm designers. Moreover, we believe our tool fills in the currently missing piece in the development of differentially private algorithms: with our tool, immature designs can first be tested for counterexamples, before being fed into those dynamic and static tools.
Funding
  • We thank anonymous CCS reviewers for their helpful suggestions. This work was partially funded by NSF awards #1228669, #1702760 and #1566411
Reference
  • Aws Albarghouthi and Justin Hsu. 2017. Synthesizing coupling proofs of differential privacy. Proceedings of the ACM on Programming Languages 2, POPL (2017), 58.
    Google ScholarLocate open access versionFindings
  • Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, and Santiago Zanella-Beguelin. 2013. Verified Computational Differential Privacy with Applications to Smart Metering. In 2013 IEEE 26th Computer Security Foundations Symposium. 287–301.
    Google ScholarLocate open access versionFindings
  • 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. 55–67.
    Google ScholarLocate open access versionFindings
  • Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub. 201Proving Differential Privacy in Hoare Logic. In 2014 IEEE 27th Computer Security Foundations Symposium. 411–424.
    Google ScholarLocate open access versionFindings
  • Gilles Barthe, Marco Gaboardi, Benjamin Gregoire, Justin Hsu, and Pierre-Yves Strub. 2016. Proving differential privacy via probabilistic couplings. In IEEE Symposium on Logic in Computer Science (LICS).
    Google ScholarLocate open access versionFindings
  • 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. 97–110.
    Google ScholarLocate open access versionFindings
  • Gilles Barthe and Federico Olmedo. 2013. Beyond differential privacy: Composition theorems and relational logic for f-divergences between probabilistic programs. In ICALP. 49–60.
    Google ScholarLocate open access versionFindings
  • Mark Bun and Thomas Steinke. 2016. Concentrated Differential Privacy: Simplifications, Extensions, and Lower Bounds. In Proceedings of the 14th International Conference on Theory of Cryptography - Volume 9985.
    Google ScholarLocate open access versionFindings
  • Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and
    Google ScholarFindings
  • Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. 2006. EXE: Automatically Generating Inputs of Death. In Conference on Computer and Communications Security (CCS). 322–335.
    Google ScholarLocate open access versionFindings
  • Rui Chen, Qian Xiao, Yu Zhang, and Jianliang Xu. 2015. Differentially private high-dimensional data publication via sampling-based inference. In Proceedings of the 21th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. ACM, 129–138.
    Google ScholarLocate open access versionFindings
  • Yan Chen and Ashwin Machanavajjhala. 2015. On the Privacy Properties of Variants on the Sparse Vector Technique. http://arxiv.org/abs/1508.07306. (2015).
    Findings
  • Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340.
    Google ScholarFindings
  • Cynthia Dwork. 2006. Differential Privacy. In Proceedings of the 33rd International Conference on Automata, Languages and Programming - Volume Part II (ICALP’06). Springer-Verlag, Berlin, Heidelberg, 1–12. https://doi.org/10.1007/11787006_1
    Locate open access versionFindings
  • Cynthia Dwork. 2008. Differential privacy: A survey of results. In International Conference on Theory and Applications of Models of Computation. Springer, 1–19.
    Google ScholarLocate open access versionFindings
  • Cynthia Dwork, Krishnaram Kenthapadi, Frank McSherry, Ilya Mironov, and Moni Naor. 2006. Our Data, Ourselves: Privacy via Distributed Noise Generation. In EUROCRYPT. 486–503.
    Google ScholarLocate open access versionFindings
  • Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith. 2006. Calibrating Noise to Sensitivity in Private Data Analysis.. In TCC.
    Google ScholarFindings
  • Cynthia Dwork, Moni Naor, Omer Reingold, Guy N.Rothblum, and Salil Vadhan. 2009. On the Complexity of Differentially Private Data Release: Efficient Algorithms and Hardness Results. In STOC. 381–390.
    Google ScholarLocate open access versionFindings
  • Cynthia Dwork, Aaron Roth, et al. 2014. The algorithmic foundations of differential privacy. Foundations and Trends® in Theoretical Computer Science 9, 3–4 (2014), 211–407.
    Google ScholarLocate open access versionFindings
  • Cynthia Dwork and Guy N. Rothblum. 2016. Concentrated Differential Privacy. http://arxiv.org/abs/1603.01887. (2016).
    Findings
  • Hamid Ebadi, David Sands, and Gerardo Schneider. 2015. Differential privacy: Now it’s getting personal. In ACM Symposium on Principles of Programming Languages (POPL).
    Google ScholarLocate open access versionFindings
  • Gian Pietro Farina, Stephen Chong, and Marco Gaboardi. 2017. Relational Symbolic Execution. http://arxiv.org/abs/1711.08349. (2017).
    Findings
  • R.A. Fisher. 1935. The design of experiments. 1935. Oliver and Boyd, Edinburgh.
    Google ScholarFindings
  • Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. 2013. Linear Dependent Types for Differential Privacy. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (ACM Symposium on Principles of Programming Languages (POPL)). 357–370.
    Google ScholarLocate open access versionFindings
  • Eric Jones, Travis Oliphant, Pearu Peterson, et al. 2001–. SciPy: Open source scientific tools for Python. (2001–). http://www.scipy.org/[Online; accessed
    Findings
  • James C King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (1976), 385–394.
    Google ScholarLocate open access versionFindings
  • Jaewoo Lee and Christopher W Clifton. 2014. Top-k frequent itemsets via differentially private fp-trees. In Proceedings of the 20th ACM SIGKDD international conference on Knowledge discovery and data mining. ACM, 931–940.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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. 19–30.
    Google ScholarLocate open access versionFindings
  • Dimiter Milushev, Wim Beck, and Dave Clarke. 2012. Noninterference via symbolic execution. In Formal Techniques for Distributed Systems. Springer, 152–168.
    Google ScholarFindings
  • Ilya Mironov. 2017. Rényi Differential Privacy. In 30th IEEE Computer Security Foundations Symposium, CSF.
    Google ScholarLocate open access versionFindings
  • Prashanth Mohan, Abhradeep Thakurta, Elaine Shi, Dawn Song, and David Culler. 2012. GUPT: Privacy Preserving Data Analysis Made Easy. In Proceedings of the ACM SIGMOD International Conference on Management of Data.
    Google ScholarLocate open access versionFindings
  • Suzette Person, Matthew B Dwyer, Sebastian Elbaum, and Corina S Pasareanu. 2008. Differential symbolic execution. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering. ACM, 226–237.
    Google ScholarLocate open access versionFindings
  • Silvio Ranise and Cesare Tinelli. 2006. The smt-lib standard: Version 1.2. Technical Report. Technical report, Department of Computer Science, The University of Iowa, 2006. Available at www. SMT-LIB. org.
    Findings
  • Jason Reed and Benjamin C. Pierce. 2010. Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP ’10). 157–168.
    Google ScholarLocate open access versionFindings
  • A. Roth. 2011. Sparse Vector Technique, Lecture notes for “The Algorithmic Foundations of Data Privacy”. (2011).
    Google ScholarFindings
  • Indrajit Roy, Srinath Setty, Ann Kilzer, Vitaly Shmatikov, and Emmett Witchel. 2010. Airavat: Security and Privacy for MapReduce. In NSDI.
    Google ScholarFindings
  • Ben Stoddard, Yan Chen, and Ashwin Machanavajjhala. 2014. Differentially private algorithms for empirical machine learning. arXiv preprint arXiv:1411.5428 (2014).
    Findings
  • Michael Carl Tschantz, Dilsun Kaynar, and Anupam Datta. 2011. Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract). Electron. Notes Theor. Comput. Sci. 276 (Sept. 2011), 61–79.
    Google ScholarLocate open access versionFindings
  • Lili Xu, Konstantinos Chatzikokolakis, and Huimin Lin. 2014. Metrics for Differential Privacy in Concurrent Systems. 199–215.
    Google ScholarFindings
  • Danfeng Zhang and Daniel Kifer. 2017. LightDP: Towards Automating Differential Privacy Proofs. In ACM Symposium on Principles of Programming Languages (POPL). 888–901.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科