*-Liftings for Differential Privacy

Authors Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub

Thumbnail PDF


  • Filesize: 0.56 MB
  • 12 pages

Document Identifiers

Author Details

Gilles Barthe
Thomas Espitau
Justin Hsu
Tetsuya Sato
Pierre-Yves Strub

Cite AsGet BibTex

Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub. *-Liftings for Differential Privacy. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 102:1-102:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. There are two styles of definitions for this construction. Earlier definitions require the existence of one or more witness distributions, while a recent definition by Sato uses universal quantification over all sets of samples. These notions have different strengths and weaknesses: the universal version is more general than the existential ones, but the existential versions enjoy more precise composition principles. We propose a novel, existential version of approximate lifting, called *-lifting, and show that it is equivalent to Sato's construction for discrete probability measures. Our work unifies all known notions of approximate lifting, giving cleaner properties, more general constructions, and more precise composition theorems for both styles of lifting, enabling richer proofs of differential privacy. We also clarify the relation between existing definitions of approximate lifting, and generalize our constructions to approximate liftings based on f-divergences.
  • Differential Privacy
  • Probabilistic Couplings
  • Formal Verification


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Ron Aharoni, Eli Berger, Agelos Georgakopoulos, Amitai Perlstein, and Philipp Sprüssel. The max-flow min-cut theorem for countable networks. J. Comb. Theory, Ser. B, 101(1):1-17, 2011. URL: http://dx.doi.org/10.1016/j.jctb.2010.08.002.
  2. Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Advanced probabilistic couplings for differential privacy. In ACM SIGSAC Conference on Computer and Communications Security (CCS), Vienna, Austria, 2016. URL: https://arxiv.org/abs/1606.07143.
  3. Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proving differential privacy via probabilistic couplings. In IEEE Symposium on Logic in Computer Science (LICS), New York, New York, 2016. URL: http://arxiv.org/abs/1601.05047.
  4. Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce. Programming language techniques for differential privacy. SIGLOG News, 3(1):34-53, 2016. URL: http://dx.doi.org/10.1145/2893582.2893591.
  5. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin. Probabilistic relational reasoning for differential privacy. ACM Transactions on Programming Languages and Systems, 35(3):9, 2013. URL: http://software.imdea.org/~bkoepf/papers/toplas13.pdf.
  6. Gilles Barthe and Federico Olmedo. Beyond differential privacy: Composition theorems and relational logic for f-divergences between probabilistic programs. In International Colloquium on Automata, Languages and Programming (ICALP), Riga, Latvia, volume 7966 of Lecture Notes in Computer Science, pages 49-60. Springer-Verlag, 2013. URL: http://certicrypt.gforge.inria.fr/2013.ICALP.pdf.
  7. Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith. Calibrating noise to sensitivity in private data analysis. In IACR Theory of Cryptography Conference (TCC), New York, New York, pages 265-284, 2006. URL: http://dx.doi.org/10.1007/11681878_14.
  8. Cynthia Dwork, Guy N. Rothblum, and Salil Vadhan. Boosting and differential privacy. In IEEE Symposium on Foundations of Computer Science (FOCS), Las Vegas, Nevada, pages 51-60, 2010. URL: http://research.microsoft.com/pubs/155170/dworkrv10.pdf.
  9. Torgny Lindvall. Lectures on the coupling method. Courier Corporation, 2002. Google Scholar
  10. Federico Olmedo. Approximate Relational Reasoning for Probabilistic Programs. PhD thesis, Universidad Politécnica de Madrid, 2014. URL: http://software.imdea.org/~federico/thesis.pdf.
  11. Tetsuya Sato. Approximate relational Hoare logic for continuous random samplings. In Conference on the Mathematical Foundations of Programming Semantics (MFPS), Pittsburgh, Pennsylvania, volume 325 of Electronic Notes in Theoretical Computer Science, pages 277-298. Elsevier, 2016. URL: https://arxiv.org/abs/1603.01445.
  12. Volker Strassen. The existence of probability measures with given marginals. The Annals of Mathematical Statistics, pages 423-439, 1965. URL: http://projecteuclid.org/euclid.aoms/1177700153.
  13. Hermann Thorisson. Coupling, Stationarity, and Regeneration. Springer-Verlag, 2000. Google Scholar
  14. Cédric Villani. Optimal transport: old and new. Springer-Verlag, 2008. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail