SMT-based query tracking for differentially private data analytics systems

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.

Keywords

differential privacy / privacy budget / satisfiability modulo theory

References

[1] Dwork C. Differential privacy. In: Proceedings of the 33rd International Colloquium on Automata, Languages and Programming. 2006, 1–12

[2] McSherry F D. Privacy integrated queries: an extensible platform for privacy-preserving data analysis. Communications of the ACM, 2009, 53: 19–30

[3] Silberschatz A, Korth H F, Sudarshan S. Database System Concepts. Vol 4. New York: McGraw-Hill, 1997

[4] 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

[5] 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

[6] Lichman M. UCI machine learning repository. Irvine, CA: University of California. 2013

[7] 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

[8] 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

[9] Godefroid P, Levin M Y, Molnar D A. Automated whitebox fuzz testing. In: Proceedings of Network and Distributed System Security Symposium. 2008, 151–166

[10] 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

[11] Cimatti A, Griggio A, Schaafsma B J, Sebastiani R. The NathSAT5 SMT solver. In: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2013, 93–107

[12] Dutertre B. Yices 2.2. In: Proceedings of International Conference on Computer Aided Verification. 2014, 737–744

[13] Xiao X, Wang G, Gehrke J. Differential privacy via wavelet transforms. IEEE Transactions on Knowledge and Data Engineering, 2011, 23(8): 1200–1214

[14] 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

[15] 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

[16] 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

[17] 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

[18] 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

[19] 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

[20] Li C, Miklau G. An adaptive mechanism for accurate query answering under differential privacy. Proceedings of the VLDB Endowment, 2012, 5(6): 514–525

[21] 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

[22] 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

[23] 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

[24] Kaushik R, Ramamurthy R. Efficient auditing for complex SQL queries. In: Proceedings of ACM SIGMOD International Conference on Management of Data. 2011, 697–708

[25] 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

[26] Motwani R, Nabar S U, Thomas D. Auditing SQL queries. In: Proceedings of the 24th IEEE International Conference on Data Engineering. 2008, 287–296

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature