{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:26:56Z","timestamp":1752982016848,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720186"},{"type":"electronic","value":"9783030720193"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Differential privacy is a de facto standard in data privacy with applications in the private and public sectors. Most of the techniques that achieve differential privacy are based on a judicious use of randomness. However, reasoning about randomized programs is difficult and error prone. For this reason, several techniques have been recently proposed to support designer in proving programs differentially private or in finding violations to it.<\/jats:p><jats:p>In this work we propose a technique based on symbolic execution for reasoning about differential privacy. Symbolic execution is a classic technique used for testing, counterexample generation and to prove absence of bugs. Here we use symbolic execution to support these tasks specifically for differential privacy. To achieve this goal, we design a relational symbolic execution technique which supports reasoning about probabilistic coupling, a formal notion that has been shown useful to structure proofs of differential privacy. We show how our technique can be used to both verify and find violations to differential privacy.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_8","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T14:03:10Z","timestamp":1616421790000},"page":"207-233","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Coupled Relational Symbolic Execution for Differential Privacy"],"prefix":"10.1007","author":[{"given":"Gian Pietro","family":"Farina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Chong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Hsu, J.: Synthesizing coupling proofs of differential privacy. Proc. ACM Program. Lang. 2(POPL), 58:1\u201358:30 (Dec 2017)","DOI":"10.1145\/3158146"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., Chadha, R., Jagannath, V., Sistla, A.P., Viswanathan, M.: Deciding differential privacy for programs with finite inputs and outputs. In: LICS \u201920. pp. 141\u2013154. ACM (2020)","DOI":"10.1145\/3373718.3394796"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Proving differential privacy via probabilistic couplings. In: LICS \u201916. pp. 749\u2013758. ACM, New York, NY, USA (2016)","DOI":"10.1145\/2933575.2934554"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., Zanella\u00a0Beguelin, S.: Probabilistic relational reasoning for differential privacy. ACM SIGPLAN Notices 47(1), 97\u2013110 (2012)","DOI":"10.1145\/2103621.2103670"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Bichsel, B., Gehr, T., Drachsler-Cohen, D., Tsankov, P., Vechev, M.: Dp-finder: Finding differential privacy violations by sampling and optimization. In: CCS \u201918. pp. 508\u2013524 (2018)","DOI":"10.1145\/3243734.3243863"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Ding, Z., Wang, Y., Wang, G., Zhang, D., Kifer, D.: Detecting violations of differential privacy. In: CCS 2018. pp. 475\u2013489 (2018)","DOI":"10.1145\/3243734.3243818"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Ding, Z., Wang, Y., Zhang, D., Kifer, D.: Free gap information from the differentially private sparse vector and noisy max mechanisms. Proc. VLDB Endow. 13(3), 293\u2013306 (2019). https:\/\/doi.org\/10.14778\/3368289.3368295, http:\/\/www.vldb.org\/pvldb\/vol13\/p293-ding.pdf","DOI":"10.14778\/3368289.3368295"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Dwork, C., McSherry, F., Nissim, K., Smith, A.D.: Calibrating noise to sensitivity in private data analysis. In: TCC. LNCS, vol.\u00a03876, pp. 265\u2013284. Springer (2006)","DOI":"10.1007\/11681878_14"},{"key":"8_CR9","unstructured":"Farina, G.P.: Coupled Relational Symbolic Execution. Ph.D. thesis, University at Buffalo, SUNY (2020), https:\/\/search.proquest.com\/pqdtglobal\/docview\/2385305218\/"},{"key":"8_CR10","unstructured":"Farina, G.P., Chong, S., Gaboardi, M.: Relational symbolic execution. In: PPDP \u201919. pp. 10:1\u201310:14. ACM, New York, NY, USA (2019)"},{"key":"8_CR11","unstructured":"Farina, G.P., Chong, S., Gaboardi, M.: Coupled relational symbolic execution for differential privacy. CoRR abs\/2007.12987 (2020), https:\/\/arxiv.org\/abs\/2007.12987"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: POPL. pp. 357\u2013370 (2013)","DOI":"10.1145\/2480359.2429113"},{"key":"8_CR13","unstructured":"Haeberlen, A., Pierce, B.C., Narayan, A.: Differential privacy under fire. In: Proceedings of the 20th USENIX Security Symposium (Aug 2011)"},{"key":"8_CR14","unstructured":"Kaplan, H., Mansour, Y., Stemmer, U.: The sparse vector technique, revisited. In: Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems, NeurIPS 2020 (2020), https:\/\/arxiv.org\/abs\/2010.00917, to appear"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Liu, D., Wang, B., Zhang, L.: Model checking differentially private properties. In: APLAS 2018. pp. 394\u2013414 (2018)","DOI":"10.1007\/978-3-030-02768-1_21"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Lyu, M., Su, D., Li, N.: Understanding the sparse vector technique for differential privacy. Proc. VLDB Endow. 10(6), 637\u2013648 (Feb 2017)","DOI":"10.14778\/3055330.3055331"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Mironov, I.: On significance of the least significant bits for differential privacy. In: CCS 2012. pp. 650\u2013661 (2012)","DOI":"10.1145\/2382196.2382264"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Near, J.P., Darais, D., Abuah, C., Stevens, T., Gaddamadugu, P., Wang, L., Somani, N., Zhang, M., Sharma, N., Shan, A., Song, D.: Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy. Proc. ACM Program. Lang. 3(OOPSLA), 172:1\u2013172:30 (2019)","DOI":"10.1145\/3360598"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ml. In: ACM SIGPLAN Notices. vol.\u00a037, pp. 319\u2013330. ACM (2002)","DOI":"10.1145\/565816.503302"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: ICFP 2010. pp. 157\u2013168. ACM (2010)","DOI":"10.1145\/1932681.1863568"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Sato, T., Barthe, G., Gaboardi, M., Hsu, J., Katsumata, S.: Approximate span liftings: Compositional semantics for relaxations of differential privacy. In: LICS 2019. pp. 1\u201314. IEEE (2019)","DOI":"10.1109\/LICS.2019.8785668"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Tschantz, M.C., Kaynar, D.K., Datta, A.: Formal verification of differential privacy for interactive systems (extended abstract). In: MFPS 2011. ENTCS (2011)","DOI":"10.1016\/j.entcs.2011.09.015"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Wang, Y., Ding, Z., Kifer, D., Zhang, D.: Checkdp: An automated and integrated approach for proving differential privacy or finding precise counterexamples. In: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security (2020), to appear","DOI":"10.1145\/3372297.3417282"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Wang, Y., Ding, Z., Wang, G., Kifer, D., Zhang, D.: Proving differential privacy with shadow execution. In: PLDI 2019. pp. 655\u2013669. ACM (2019)","DOI":"10.1145\/3314221.3314619"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Warner, S.L.: Randomized response: A survey technique for eliminating evasive answer bias. Journal of the American Statistical Association 60(309), 63\u201369 (1965)","DOI":"10.1080\/01621459.1965.10480775"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, D., Kifer, D.: Lightdp: towards automating differential privacy proofs. In: POPL 2017. pp. 888\u2013901. ACM (2017)","DOI":"10.1145\/3093333.3009884"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Zhang, H., Roth, E., Haeberlen, A., Pierce, B.C., Roth, A.: Testing differential privacy with dual interpreters. Proc. ACM Program. Lang. (OOPSLA) (2020), to appear","DOI":"10.1145\/3428233"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T03:06:01Z","timestamp":1635131161000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}