Abstract
Differential privacy enables sensitive data to be analyzed in a privacy-preserving manner. In this paper, we focus on the online setting where each analyst is assigned a privacy budget and queries the data interactively. However, existing differentially private data analytics systems such as PINQ process each query independently, which may cause an unnecessary waste of the privacy budget. Motivated by this, we present a satisfiability modulo theories (SMT)-based query tracking approach to reduce the privacy budget usage. In brief, our approach automatically locates past queries that access disjoint parts of the dataset with respect to the current query to save the privacy cost using the SMT solving techniques. To improve efficiency, we further propose an optimization based on explicitly specified column ranges to facilitate the search process. We have implemented a prototype of our approach with Z3, and conducted several sets of experiments. The results show our approach can save a considerable amount of the privacy budget and each query can be tracked efficiently within milliseconds.
Similar content being viewed by others
References
Dwork C. Differential privacy. In: Proceedings of the 33rd International Colloquium on Automata, Languages and Programming. 2006, 1–12
McSherry F D. Privacy integrated queries: an extensible platform for privacy-preserving data analysis. Communications of the ACM, 2009, 53: 19–30
Silberschatz A, Korth H F, Sudarshan S. Database System Concepts. Vol 4. New York: McGraw-Hill, 1997
McSherry F, Talwar K. Mechanism design via differential privacy. In: Proceedings of the 48th Annual IEEE Symposium on Foundations of Computer Science. 2007, 94–103
De Moura L, Bjørner N. Z3: an efficient SMT solver. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2008, 337–340
Lichman M. UCI machine learning repository. Irvine, CA: University of California. 2013
Barnett M, Chang B Y E, DeLine R, Jacobs B, Leino K R M. Boogie: a modular reusable verifier for object-oriented programs. In: Proceedings of International Conference on Formal Methods for Components and Objects. 2006, 364–387
Kroening D, Tautschnig M. CBMC-C bounded model checker. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2014, 389–391
Godefroid P, Levin M Y, Molnar D A. Automated whitebox fuzz testing. In: Proceedings of Network and Distributed System Security Symposium. 2008, 151–166
Cadar C, Godefroid P, Khurshid S, Păsăreanu C S, Sen K, Tillmann N, Visser W. Symbolic execution for software testing in practice: preliminary assessment. In: Proceedings of the 33rd International Conference on Software Engineering. 2011, 1066–1071
Cimatti A, Griggio A, Schaafsma B J, Sebastiani R. The NathSAT5SMT solver. In: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2013, 93–107
Dutertre B. Yices 2.2. In: Proceedings of International Conference on Computer Aided Verification. 2014, 737–744
Xiao X,Wang G, Gehrke J. Differential privacy via wavelet transforms. IEEE Transactions on Knowledge and Data Engineering, 2011, 23(8): 1200–1214
Hay M, Rastogi V, Miklau G, Suciu D. Boosting the accuracy of differentially private histograms through consistency. Proceedings of the VLDB Endowment, 2010, 3(1–2): 1021–1032
Xu J, Zhang Z J, Xiao X K, Yang Y, Yu G. Differentially private histogram publication. In: Proceedings of IEEE International Conference on Data Engineering. 2012, 32–43
Chen R, Mohammed N, Fung B C M, Desai B C, Xiong L. Publishing set-valued data via differential privacy. Proceedings of the VLDB Endowment, 2011, 4(11): 1087–1098
Zhang J, Cormode G, Procopiuc C M, Srivastava D, Xiao X K. Privbayes: private data release via Bayesian networks. In: Proceedings of ACM SIGMOD International Conference on Management of Data. 2014, 1423–1434
Xiao X K, Bender G, Hay M, Gehrke J. iReduct: differential privacy with reduced relative errors. In: Proceedings of ACM SIGMOD International Conference on Management of Data. 2011, 229–240
Li C, Hay M, Rastogi V, Miklau G, McGregor A. Optimizing linear counting queries under differential privacy. In: Proceedings of the 29th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems. 2010, 123–134
Li C, Miklau G. An adaptive mechanism for accurate query answering under differential privacy. Proceedings of the VLDB Endowment, 2012, 5(6): 514–525
Yuan G Z, Zhang Z J, Winslett M, Xiao X K, Yang Y, Hao Z F. Lowrank mechanism: optimizing batch queries under differential privacy. Proceedings of the VLDB Endowment, 2012, 5(11): 1352–1363
Peng S F, Yang Y, Zhang Z J, Winslett M, Yu Y. Query optimization for differentially private data management systems. In: Proceedings of the 29th IEEE International Conference on Data Engineering. 2013, 1093–1104
Agrawal R, Bayardo R, Faloutsos C, Kiernan J, Rantzau R, Srikant R. Auditing compliance with a hippocratic database. In: Proceedings of the 30th International Conference on Very Large Data Bases. 2004, 516–527
Kaushik R, Ramamurthy R. Efficient auditing for complex SQL queries. In: Proceedings of ACM SIGMOD International Conference on Management of Data. 2011, 697–708
Miklau G, Suciu D. A formal analysis of information disclosure in data exchange. In: Proceedings of ACM SIGMOD International Conference on Management of Data. 2004, 575–586
Motwani R, Nabar S U, Thomas D. Auditing SQL queries. In: Proceedings of the 24th IEEE International Conference on Data Engineering. 2008, 287–296
Acknowledgements
This work was supported in part by the National Program on Key Basic Research Project (973 Program) (2010CB328003), the National Natural Science Foundation of China (Grant Nos. 61672310, 61272001, 60903030, 91218302), and the National Key Technologies R&D Program of China (SQ2012BAJY4052).
Author information
Authors and Affiliations
Corresponding author
Additional information
Chen Luo received his BS degree from Tongji University, China in 2013 and his Master’s degree from Tsinghua University, China in 2016. He is currently a PhD student in University of California Irvine, USA. His research interests include formal methods and database systems.
Fei He received his BS degree from the National University of Defense Technology, China in 2002, and the PhD degree from Tsinghua University, China in 2008. He is currently an associate professor in the School of Software at Tsinghua University, China. His research interests include satisfiability, model checking, compositional reasoning, and their applications to embedded systems.
Electronic supplementary material
Rights and permissions
About this article
Cite this article
Luo, C., He, F. SMT-based query tracking for differentially private data analytics systems. Front. Comput. Sci. 12, 1192–1207 (2018). https://doi.org/10.1007/s11704-016-6049-6
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11704-016-6049-6