Your browser doesn't support the features required by impress.js, so you are presented with a simplified version of this presentation.

For the best experience please use the latest Chrome, Safari or Firefox browser.

Formalizing Differential Privacy

Please give a careful analysis of the sparse vector technique, comparing your formalization with the differential privacy book and the previous formalizations in [A1,A2].

Overview

  • Differential Privacy and SVT
  • Preliminaries
  • Implementations and Proofs
  • Comparison and Contribution

Background

  • Differential Privacy
    • Adjacent inputs yield bound outputs
  • Sparse Vector Technique
    • Goal: Release an interesting subset of a set of queries.

Preliminaries

  • Adjacency: One sensitive queries
  • Delta: We disregard it

Implementations and Proofs

Above Threshold (Dwork and Roth)

Above Threshold (Barthe et al.)

Between Thresholds (Barthe et al.)

โคน

Contribution and Comparison

From monolith to composition

Release Condition
Numeric
Outer Composition

Logical Proofs

EasyCrypt Implementation

  • Proof verification
  • Let's have a look

Use a spacebar or arrow keys to navigate