Approximate Span Liftings

TL;DR

This paper introduces approximate span-liftings, a new mathematical framework for reasoning about relaxed forms of differential privacy, enabling compositional analysis of privacy guarantees for complex algorithms.

Contribution

It develops approximate span-liftings as a novel extension of relational liftings to handle various divergences and continuous distributions, and applies this to a new program logic for privacy proofs.

Findings

Framework for reasoning about RDP, zCDP, and truncated CDP

Extension of relational liftings to continuous distributions

A program logic for verifying privacy relaxations

Abstract

We develop new abstractions for reasoning about relaxations of differential privacy: R\'enyi differential privacy, zero-concentrated differential privacy, and truncated concentrated differential privacy, which express different bounds on statistical divergences between two output probability distributions. In order to reason about such properties compositionally, we introduce approximate span-lifting, a novel construction extending the approximate relational lifting approaches previously developed for standard differential privacy to a more general class of divergences, and also to continuous distributions. As an application, we develop a program logic based on approximate span-liftings capable of proving relaxations of differential privacy and other statistical divergence properties.