Verification of differential private computationss

May 31, 2016 12:00 AM

Who: Gilles Barthe (IMDEA)\
When: 13:30, May 31 \
Where: room EDIT 8103\
Title: {{ page.title }}

Differential privacy is a statistical notion of privacy which achieves compelling trade-offs between input privacy and accuracy (of outputs). Differential privacy is also an attractive target for verification: despite their apparent simplicity, recently proposed algorithms have intricate privacy and accuracy proofs. We present two program logics for reasoning about privacy and accuracy properties of probabilistic computations. The accuracy logic captures reasoning about the union bound, a simple but effective tool from probablility theory, whereas the privacy logic captures fine-grained reasoning about probabilistic couplings, a powerful tool for studying Markov chains. We illustrate the strengths of our program logics with novel and elegant proofs of challenging examples from differential privacy.

Previous Talks

{: .t60 } {% include list-posts tag=‘csstalk’%}