Coupled relational symbolic execution for differential privacy

DOI10.1007/978-3-030-72019-3_8zbMATH Open1473.68072arXiv2007.12987OpenAlexW3150939926MaRDI QIDQ2233459FDOQ2233459

Authors: Gian Pietro Farina, Stephen Chong, Marco Gaboardi 

Publication date: 18 October 2021

Abstract: 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. 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 leverage two ideas that have been already proven useful in formal reasoning about differential privacy: relational reasoning and probabilistic coupling. Our technique integrates these two ideas and shows how such a combination can be used to both verify and find violations to differential privacy.

Full work available at URL: https://arxiv.org/abs/2007.12987

Recommendations

• Differential privacy for symbolic systems with application to Markov chains
• scientific article; zbMATH DE number 7333242
• Probabilistic relational reasoning for differential privacy
• Symbolic algorithmic verification of intransitive generalized noninterference
• Formal verification of differential privacy for interactive systems (extended abstract)
• Probabilistic relational verification for cryptographic implementations
• Relational \(\star\)-liftings for differential privacy
• scientific article; zbMATH DE number 1929965

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Privacy of data (68P27)

Cites Work

• LightDP: towards automating differential privacy proofs
• Randomized response: a survey technique for eliminating evasive answer bias
• Theory of Cryptography
• Information flow inference for ML
• Linear dependent types for differential privacy
• Probabilistic relational reasoning for differential privacy
• Distance makes the types grow stronger: a calculus for differential privacy
• Formal verification of differential privacy for interactive systems (extended abstract)
• Proving differential privacy via probabilistic couplings
• Coupled relational symbolic execution for differential privacy
• Deciding differential privacy for programs with finite inputs and outputs
• Model checking differentially private properties

Cited In (5)

• Proving differential privacy via probabilistic couplings
• Sound symbolic execution via abstract interpretation and its application to security
• Probabilistic relational reasoning for differential privacy
• Verifying Pufferfish privacy in hidden Markov models
• Coupled relational symbolic execution for differential privacy

This page was built for publication: Coupled relational symbolic execution for differential privacy

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233459)