Advanced Probabilistic Couplings for Differential Privacy
Accuracy-dependent, Advanced Composition, Adaptive Algorithms
Gilles Barthe

Noémie Fong

IMDEA Software Institute
Madrid, Spain

ENS
Paris, France

arXiv:1606.07143v2 [cs.LO] 17 Aug 2016

Benjamin Grégoire
Inria
Sophia-Antipolis, France

†

Justin Hsu

University of Pennsylvania
Philadelphia, USA

ABSTRACT
Differential privacy is a promising formal approach to data privacy,
which provides a quantitative bound on the privacy cost of an algorithm that operates on sensitive information. Several tools have
been developed for the formal verification of differentially private
algorithms, including program logics and type systems. However,
these tools do not capture fundamental techniques that have emerged
in recent years, and cannot be used for reasoning about cutting-edge
differentially private algorithms. Existing techniques fail to handle
three broad classes of algorithms: 1) algorithms where privacy depends on accuracy guarantees, 2) algorithms that are analyzed with
the advanced composition theorem, which shows slower growth in
the privacy cost, 3) algorithms that interactively accept adaptive
inputs.
We address these limitations with a new formalism extending
apRHL [6], a relational program logic that has been used for proving
differential privacy of non-interactive algorithms, and incorporating
aHL [11], a (non-relational) program logic for accuracy properties.
We illustrate our approach through a single running example, which
exemplifies the three classes of algorithms and explores new variants
of the Sparse Vector technique, a well-studied algorithm from the
privacy literature. We implement our logic in EasyCrypt, and formally verify privacy. We also introduce a novel coupling technique
called optimal subset coupling that may be of independent interest.

1.

INTRODUCTION

Differential privacy, a rigorous and quantitative notion of statistical privacy, is one of the most promising formal definitions of
privacy to date. Since its initial formulation by Dwork et al. [19],
differential privacy has attracted substantial attention throughout
∗Partially supported by NSF grants CNS-1237235, CNS-1565365
and by EPSRC grant EP/M022358/1.
†Partially supported by NSF grants #1065060 and #1513694, and
a grant from the Simons Foundation (#360368 to Justin Hsu).
Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. Copyrights for components of this work owned by others than the
author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or
republish, to post on servers or to redistribute to lists, requires prior specific permission
and/or a fee. Request permissions from permissions@acm.org.

CCS’16, October 24 - 28, 2016, Vienna, Austria
c 2016 Copyright held by the owner/author(s). Publication rights licensed to ACM.
ISBN 978-1-4503-4139-4/16/10. . . $15.00
DOI: http://dx.doi.org/10.1145/2976749.2978391

∗

Marco Gaboardi

University at Buffalo, SUNY
Buffalo, USA

Pierre-Yves Strub
IMDEA Software Institute
Madrid, Spain

computer science, including areas like databases, machine learning,
and optimization, and more.
There are several reasons for this success. For one, differential
privacy allows a formal trade-off between privacy and accuracy:
differentially private algorithms come with a privacy guarantee
expressed in terms of two parameters  (expressing the privacy cost)
and δ (expressing the probability of violating the privacy cost). For
both parameters, smaller values offer stronger privacy guarantees.
Another important advantage differential privacy is that it composes well: differentially private algorithms can be easily combined
to build new private algorithms. The differential privacy literature
offers several composition theorems, differing in how the privacy
parameter of the larger algorithm depends on the parameters of the
components. These composition properties can also be used in interactive and adaptive scenarios where an adversary can decide which
algorithm to run depending on the outputs of previous algorithms.
Differential privacy’s clean composition properties also make it
an attractive target for an unusually diverse array of formal verification techniques. By now, there are tools that formally guarantee
differential privacy via relational program logics [2, 6], linear type
systems [25, 29, 42], interactive automata [50, 51], product programs [7], satisfiability modulo theories [28], refinement type systems [9], and more. While these systems formalize privacy through
a wide variety techniques, most of these approaches analyze a composition of private algorithms using the sequential composition
theorem of differential privacy, which guarantees that the resulting
algorithms have parameter  and δ equal to the sum of the parameters
of their components.
Recently, Barthe et al. [10] highlighted a close connection between approximate couplings and differential privacy which enables
formal verification beyond sequential composition. Barthe et al.
[10] work with the relational program logic apRHL [6], extended
with a new composition principle called pointwise privacy. The
idea is to first prove a restricted case of privacy—corresponding
roughly to privacy for a single output—and then combine the results
to prove the full differential privacy property. Combined with the
composition principle for approximate couplings, which generalizes
the sequential composition theorem, apRHL can express simple,
compositional proofs of algorithms like the one-side Laplace implementation of the Exponential mechanism [17] and the Above
Threshold algorithm [17] while abstracting away reasoning about
probabilistic events. Existing privacy proofs for these algorithms,
even on paper, involve ad hoc computation of probabilities.
While apRHL substantially expands the range of formal verification in differential privacy, there are still private algorithms that
apRHL cannot verify. Roughly, there are three missing pieces:

• Accuracy-dependent privacy. Some algorithms are only private if an accuracy property holds.
• Advanced composition. This principle shows slower growth
in the privacy cost, in exchange for a small probability of
violating privacy. The proof involves an technical martingale
concentration argument.
• Interactive privacy. Some private algorithms are interactive,
receiving a continuous sequence of adaptive inputs while
producing intermediate outputs.
These three missing pieces correspond to three fundamental principles of differential privacy. While there are many algorithms from
the privacy literature that use one (or more) of these three features, to
structure our presentation we will work with a variant of the Sparse
Vector technique based on the Between Thresholds algorithm [13],
a single unifying example that uses all three features (§ 2). After
reviewing some technical preliminaries about differential privacy,
approximate couplings, and the logic apRHL (§ 3), we describe
extensions to apRHL to verify privacy for new classes of algorithms.
• New proof rules that allow reasoning within apRHL while
assuming an accuracy property, incorporating accuracy proofs
from the Hoare logic aHL [11] (§ 4). We demonstrate these
rules on a classic example of accuracy-dependent privacy: the
Propose-test-release framework [16, 48].
• A proof rule that analyzes loops using the advanced composition principle; soundness relies on a novel generalization of
advanced composition to approximate couplings (§ 5).
• New proof rules for adversaries, external procedure calls that
model an adaptive source of inputs (§ 6).
• Orthogonal to reasoning about accuracy, advanced composition, and adversarial inputs, we introduce a general construction that may be of independent interest called the optimal
subset coupling. This construction gives an approximate lifting relating subsets that yields the best possible , and we use
this construction to give a new interval coupling rule for the
Laplace distribution (§ 7).
We then show how to combine these ingredients to verify our
main running example, the Between Thresholds algorithm (§ 8). We
finish with related work (§ 9) and some concluding thoughts (§ 10).

2.

MOTIVATING EXAMPLE

Before diving into the technical details we’ll first present our
motivating example, which involves accuracy-dependent privacy,
advanced composition, and interactive privacy. We first review the
definition of differential privacy, a relational property about probabilistic programs proposed by Dwork, McSherry, Nissim and Smith.
Definition 1. Let the adjacency relation be Φ ⊆ A × A, and , δ >
0. A program M : A → Distr(B) satisfies (, δ)-differential
privacy with respect to Φ if for every pair of inputs a, a0 ∈ A such
that Φ(a, a0 ) and every subset of outputs S ⊆ B, we have
Pr [y ∈ S] ≤ exp()

y←M a

Pr 0 [y ∈ S] + δ.

y←M a

When δ = 0, we say that M is -differentially private.
Intuitively, Φ relates inputs that differ in a single individual’s data.
Then, differential privacy requires that the two resulting distributions
on outputs should be close.

ASVbt (a, b, M, N, d) :=
i ← 0; l ← [];
$ L
u←
/2 (0);
A ← a − u; B ← b + u;
while i < N ∧ |l| < M do
q ← A(l);
$ L 0
S←
 /3 (evalQ(q, d));
if (A ≤ S ≤ B) then l ← i :: l;
i ← i + 1;
return l
Figure 1: Sparse Vector for Between Thresholds

Our motivating example is Adaptive Sparse Vector for Between
Thresholds (ASVbt ), a variant of the Sparse Vector algorithm. Our
algorithm takes a stream of numeric queries as input, and answers
only the queries that take a value within some range. The main
benefit of Sparse Vector is that queries that take a value outside
the range do not increase the privacy cost, even though testing
whether whether the query is (approximately) in the range involves
private data. Sparse Vector is an appealing example, because of its
popularity and its difficulty. In particular, the privacy proof of Above
Threshold is non-compositional and notoriously tricky, and several
variants1 of the algorithm were supposedly proved to be private
but were later shown to be non-private (Lyu et al. [34] provide a
comprehensive survey).
The code of ASVbt is shown in Fig. 1. At a high level, the algorithm accepts a stream of adversarially chosen queries and produces
a list of queries whose answer lies (approximately) between two
threshold parameters a and b. The algorithm computes noisy versions A and B of a and b using the Laplace mechanism L , which
we review in the next section, and then performs an interactive loop
for a fixed number (N ) of iterations. Each step, a stateful adversary A receives the current list l of queries whose answer on input
database d lies between [A, B] and selects a new query q. If its noisy
answer S lies in [A, B] and there have been fewer than M queries
between threshold, the algorithm adds q to the list l. Our algorithm
differs from standard presentations of Adaptive Sparse Vector [17]
in two significant respects:
• we use BetweenThresholds rather than AboveThreshold
for deciding whether to add a query to the list;
• we do not rerandomize the noise on the thresholds each time
a query is added to l; therefore, our algorithm adds less noise.
ASVbt satisfies the following privacy guarantee.
Theorem 2. Let  and δ both be in (0, 1). Set

0 , p
,
4 2M ln(2/δ)
and suppose a and b are such that
b−a≥

6
4
ln(4/0 ) + ln(2/δ).
0


1
There exist multiple versions of Sparse Vector. The earliest reference seems to be Dwork et al. [20]; several refinements were
proposed by Hardt and Rothblum [30], Roth and Roughgarden [44].
Applications often use their own variants, e.g. Shokri and Shmatikov
[46]. The most canonical version of the algorithm is the version
by Dwork and Roth [17].

If all adversarial queries q are 1-sensitive (i.e. |evalQ(q, d) −
evalQ(q, d0 )| ≤ 1 for every adjacent databases d and d0 ), then
ASVbt is (, δ)-differentially private.
The formal proof of this theorem, which we have verified in an
implementation of our logic within the EasyCrypt system, involves
several features:
• reasoning principles for mixing accuracy and privacy guarantees, using a combination of relational logics [6, 10] and
non-relational logics [11];
• a generalization of the advanced composition theorem for
handling the body of the loop;
• an adversary rule for handling interactive inputs in the loop;
and
• a new reasoning principle, called optimal subset coupling, for
handling the Laplace mechanism in the loop.
We stress that the use of pointwise equality, which is required for
proving privacy of between thresholds, makes the proof significantly
more challenging than other examples involving solely adaptive
adversaries, advanced composition, and accuracy-dependent privacy.
We remark that Bun et al. [13] proposed Between Threshold and
proved its privacy. Their proof does not use advanced composition,
and follows from a somewhat complicated calculations about the
probabilities of certain events. Our proof demonstrates the power of
approximate liftings: somewhat surprisingly, we arrive at an elegant
privacy proof without probabilistic reasoning.

3.

BACKGROUND

Before presenting our new extensions, we first review some preliminaries about differential privacy, the connection to approximate
liftings, the program logic apRHL [6] and its extension apRHL+
[10], and the union bound logic aHL [11].

3.1

Mathematical preliminaries

To avoid measure-theoretic issues, we base our technical development on distributions over discrete
sets B. A function µ : B → R≥0
P
is a distribution over B if b∈supp(µ) µ(b) = 1. As usual, the support supp(µ) is the subset of B with non-zero weight under µ. We
write Distr(B) for the set of discrete distributions over B. Equality
of distributions is defined as pointwise equality of functions.
We will also use marginal distributions. Formally, the first and
second marginals of a distribution µ ∈ Distr(B1 × B2 ) are simply
the projections: the distributions π1 (µ) ∈ Distr(B1 ) and π2 (µ) ∈
Distr(B2 ) given by
X
X
π1 (µ)(b1 ) =
µ(b1 , b2 )
π2 (µ)(b2 ) =
µ(b1 , b2 ).
b2 ∈B2

3.2

b1 ∈B1

Differential privacy

We will need several tools from differential privacy; readers
should consult the textbook by Dwork and Roth [17] for a more
comprehensive introduction. Most differentially private algorithms
are constructed from private primitive operations. The most famous
primitive is the Laplace mechanism.
Definition 3 (Laplace mechanism [19]). Let  > 0. The (discrete)
Laplace mechanism L : Z → Distr(Z) is defined by L (t) =
t + ν, where ν ∈ Z with probability proportional to
Pr[ν] ∝ exp (− · |ν|).

The level of privacy depends on the sensitivity of the query, which
measures how far the function may differ on two related inputs.
Roughly, adding the same level of Laplace noise to a higher sensitivity query will be less private.
Definition 4 (Sensitivity). A function F : A → Z is k-sensitive
with respect to Φ ⊆ A × A if |F (a1 ) − F (a2 )| ≤ k for every
a1 , a2 ∈ A such that Φ(a1 , a2 ).
The Laplace mechanism satisfies an accuracy specification.
Proposition 5 (Laplace accuracy). Let , β > 0, and suppose x is
the result from running L (t). Then |x−t| ≤ 1 ln β1 with probability
at least 1 − β.
Besides private primitives, the other main tools for constructing private programs are the composition theorems. These results
describe the privacy level for a combination of private programs—
say, calls to the Laplace mechanism. We will use a bit of notation for compositions. Let {fi } be a set of n functions of type
A → D → Distr(A). Denote the n-fold composition f n : A →
D → Distr(A) by
(
unit a
:k=0
k
f (a, d) =
bind f k−1 (a, d) fk (−, d) : k ≥ 1.
Here, unit : A → Distr(A) and bind : Distr(A) → (A →
Distr(B)) → Distr(B) are the monadic operations for distributions. They satisfy the following equalities:

1 if a = b
unit(a)(b) =
0 otherwise
and for f : A → Distr(B) and F : A → B → Distr(C) ,
X
(bind f F )(a)(c) =
f (a)(b) F (a)(b)(c).
b

We will also use this composition notation when the functions {fi }
have type A → Distr(A), simply dropping the parameter d above
when defining f n : A → Distr(A).
Then, the most basic composition theorem in differential privacy
is sequential composition.
Theorem 6 (Sequential composition). Let fi : A → D →
Distr(A) be a sequence of n functions, such that for every fixed
a ∈ A, the functions fi (a) : D → Distr(A) are (i , δi )differentially private for some adjacency relation on D. Then for
every initial value a ∈ A, the composition f n (a) : D → Distr(A)
is (∗ , δ ∗ )-differentially private for
∗ =

n
X
i=1

i

and δ ∗ =

n
X

δi .

i=1

That is, the epsilons and deltas sum up through composition.
The sequential composition theorem is quite useful, and is the
main principle supporting modular verification of differential privacy. However, there is another composition theorem, known as
advanced composition [22]. Instead of summing up the privacy
costs, this theorem gives slower growth of  in exchange for increasing the δ parameter. Advanced composition is an extremely
common tool for analyzing differentially private algorithms, but it
is not supported by most formal verification systems today.
Theorem 7 (Advanced composition). Let fi : A → D →
Distr(A) be a sequence of n functions, such that for every fixed a ∈
A, the functions fi (a) : D → Distr(A) are (, δ)-differentially

private for some adjacency relation on D. Then, for every a ∈ A
and ω ∈ (0, 1), the composed function f n (a) : D → Distr(A) is
(∗ , δ ∗ )-differentially private for
p

∗ =
2n ln(1/ω)  + n(e − 1) and δ ∗ = nδ + ω.

of Ψ ⊆ A1 × A2 , written µ1 Ψ](,δ) µ2 , if there exist two witness
distributions µL ∈ Distr(A1 × A2 ) and µR ∈ Distr(A1 × A2 )
such that
1. π1 (µL ) = µ1 and π2 (µR ) = µ2 ;
2. supp(µL ) ⊆ Ψ and supp(µR ) ⊆ Ψ; and

In particular, if we have 0 ∈ (0, 1), ω ∈ (0, 1/2), and

3. ∆ (µL , µR ) ≤ δ.

0
= p
,
2 2n ln(1/ω)
2

a short calculation shows that the function f
differentially private.

n

0

∗

is ( , δ )-

Kairouz et al. [32] propose sharper versions of this composition
theorem, including a provably optimal version and a version for the
heterogeneous case when the privacy level (i , δi ) may depend on
i. We will use Theorem 7 for simplicity, but our techniques enable
other composition theorems to be easily plugged in.

3.3

Approximate liftings generalize several concepts for relating distributions. When µL = µR , we have a (0, 0)-lifting, sometimes
called an exact probabilistic lifting. Such a lifting, with any Ψ,
implies a probabilistic coupling between (µ1 , µ2 ).
Approximate liftings satisfy the following property, also known
as the fundamental lemma of approximate liftings.
Lemma 10 (Barthe and Olmedo [2]). Let E1 ⊆ B1 , E2 ⊆ B2 ,
µ1 ∈ Distr(B1 ) and µ2 ∈ Distr(B2 ). Let
Ψ = {(x1 , x2 ) ∈ B1 × B2 | x1 ∈ E1 ⇒ x2 ∈ E2 }.

Approximate liftings

While the definition of differential privacy seems to be a straightforward property about probabilities in two distributions, a recent
line of work initiated by Barthe et al. [6] and subsequently developed [2, 10] shows that differential privacy is a consequence of an
approximate version of probabilistic coupling, called approximate
liftings. Couplings are a long-standing tool in probability theory for
analyzing pairs of distributions, but the relation between differential
privacy and approximate couplings is still being explored.
Unlike couplings, where there is a single accepted definition,
several incomparable notions of approximate liftings have been
proposed. The first definition is by Barthe et al. [6] but has some
technical shortcomings; we will use a more recent definition by
Barthe and Olmedo [2]. We begin by defining a distance on distributions, closely related to (, δ)-differential privacy.
Definition 8 (Barthe and Olmedo [2]). Let  ≥ 0. The -DP divergence ∆ (µ1 , µ2 ) between two distributions µ1 ∈ Distr(A) and
µ2 ∈ Distr(A) is defined as


sup
Pr [x ∈ S] − exp() Pr [x ∈ S] .
S⊆A

x←µ1

x←µ2

For the connection to differential privacy, it is not hard to see
that if M : D → Distr(A), then M is (, δ)-differentially
private iff for every pair of adjacent inputs d, d0 , we have
∆ (M (d), M (d0 )) ≤ δ. This distance is also central to the definition of approximate liftings.

If µ1 Ψ](,δ) µ2 , then
Pr [x1 ∈ E1 ] ≤ exp() Pr [x2 ∈ E2 ] + δ.

x1 ←µ1

Using this lemma, one can prove that differential privacy is equivalent to a particular form of approximate lifting.
Proposition 11 (Barthe and Olmedo [2]). A probabilistic computation M : D → Distr(A) is (, δ)-differentially private for adjacency relation Φ iff
M (a) =](,δ) M (a0 )
for every two adjacent inputs a and a0 .
Approximate liftings form the basis of the program logic apRHL,
to which we turn next.

3.4

C ::=
|
|
|
|
|
|
|

2
First, note that e −1 ≤ 2 for  ∈ (0, 1); this follows by convexity
of e − 2 − 1. Then, we have:
p
p
2n ln(1/ω) + n(e − 1) ≤ 2n ln(1/ω) + 2n2

0
0
0
+ ·
2
2 2 ln(1/ω)
0
0
≤ + = 0 ,
2
2

where the last inequality is because ω ∈ (0, 1/2) and 0 ∈ (0, 1),
and the last factor is maximized at 0 = 1 and ω = 1/2:
1
0
≤
< 1.
2 ln(1/ω)
2 ln(2)

The relational program logic

The logic apRHL, originally proposed by Barthe et al. [6], is a
relational program logic for verifying differential privacy. We take
this logic as our point of departure; we briefly recall the main points
here.
We consider a simple imperative language with random sampling,
oracle calls and adversary calls; the latter two are new to the present
work. The set of commands is defined inductively:

Definition 9 (Barthe and Olmedo [2]). Two distributions µ1 ∈
Distr(A1 ) and µ2 ∈ Distr(A2 ) are related by the (, δ)-lifting

=

x2 ←µ2

skip
C; C
X ←E
$ L (E)
X ←

if E then C else C
while E do C
(X , . . . , X ) ← A(E, . . . , E)
(X , . . . , X ) ← O(E, . . . , E)

noop
sequencing
deterministic assignment
Laplace mechanism
conditional
while loop
adversary call
procedure call

where X is a set of variables and E is a set of expressions. Variables and expressions are typed, and range over standard types like
booleans, integers, databases, queries, lists, etc. We omit the semantics of expressions, which is standard. Commands are interpreted
as maps State → Distr(State); this is also a standard choice
(e.g., see Barthe et al. [6]).3 We will write [[c]]m to mean the output
distribution of command c, executed on input memory m.
3

We will assume that commands are terminating on all executions.
The logic apRHL can also reason about possibly non-terminating
programs by working with sub-distributions instead of distributions.

An apRHL judgment has the form
0

` c ∼h,δi c : Φ =⇒ Ψ.
Reminiscent of Hoare logic, Φ represents the pre-condition while Ψ
represents the post-condition. Both Φ and Ψ are first order formulas
over the program variables. For expressing relational properties,
program variables are tagged with either h1i or h2i to indicate
whether they belong to c or c0 respectively. For instance, we can
assert that the variable x differs by at most 1 in the two runs with
the assertion |xh1i − xh2i| ≤ 1.
Crucially, the post-condition Ψ is interpreted as an approximate
lifting over the output distributions. More formally, the judgment is
valid iff for every two memories m1 and m2 such that m1 Φ m2 ,
we have
([[c1 ]]m1 ) Ψ](,δ) ([[c2 ]]m2 ).
We present selected rules, taken from prior presentations of apRHL
[6, 10] in Fig. 2; F V (Φ) denotes the set of program variables in
the assertion Φ, and M V (c) denotes the set of program variables
that are modified (i.e., written) by program c. Many of the rules
bear a resemblance to the standard Hoare logic rules. The rules
[A SSN ] and [C OND ] are relational versions of the assignment and
conditional rules; note that [C OND ] assumes that the two guards are
equal in the pre-condition. The rule [S EQ ] reflects the composition
principle of approximate liftings, where the indices  and δ add; this
rule generalizes the standard composition theorem of differential
privacy. The rule [W HILE ] extends this reasoning to loops with
a bound number of iterations, again assuming that the guards are
equal in both programs.
The next two rules, [L AP N ULL ] and [L AP G EN ], are for relating
two sampling instructions from the Laplace distribution. Intuitively
[L AP N ULL ] models adding identical noise on both sides, so that
the distance between the samples (y1 h1i, y2 h2i) is equal to the
distance between the means (e1 h1i, e2 h2i). [L AP G EN ] is a general
rule for assuming that the two samples are shifted and related by
y1 h1i + k = y2 h2i; the privacy cost depends on how far the means
(e1 h1i + k, e2 h2i) are.
The final group of rules are the structural rules. Besides the usual
rules for consequence and framing ([C ONSEQ ] and [F RAME ]), the
most interesting rule is the pointwise equality rule [PW-E Q ]. This
rule proves differential privacy by showing a pointwise judgment
for each possible output value i, and is the key tool for supporting
privacy proofs beyond the standard composition theorems.

3.5

The union bound logic

When reasoning about privacy, we will sometimes need to prove
probabilistic bounds on accuracy. Since accuracy properties are not
relational, we cannot verify them in apRHL. There is a long history
of research for formally verifying probabilistic properties, and we
are free to choose any of these techniques to interface with our logic.
In our favor, we are interested in simple accuracy properties of the
form Pr[Ψ] < β, where Ψ is an assertion on the program memory.
We call such assertions bad event assertions, since they state that the
probability of some event Ψ—the “bad event”—is at most β. We
will prove accuracy assertions in the Hoare logic aHL [11], which
is specialized to prove bad event assertions.
We will highlight just the features of aHL needed for our purposes;
readers should consult Barthe et al. [11] for a complete presentation.
Concretely, aHL judgments have the following form:
`β c : Φ =⇒ Ψ,
where Φ and Ψ are (non-probabilistic) assertions over program
memories, and β ∈ [0, 1] is a real-valued index. Assertions in aHL

are non-relational, and mention program variables from a single
memory instead of program variables tagged with h1i or h2i. To
mediate between the non-relational assertions of aHL and the relational assertions of apRHL, from a non-relational assertion Φ we
can define relational assertions Φh1i and Φh2i by interpreting Φ
where all program variables are tagged with h1i or h2i respectively.
The semantics of commands is unchanged from apRHL; we
interpret commands as maps State → Distr(State). The above
judgement means: for any initial memory satisfying Φ, the probability that ¬Ψ holds in the resulting distribution on memories is
at most β. For instance, the accuracy specification of the Laplace
mechanism (Proposition 5) is given by the following aHL judgment:
$ L (e) : > =⇒ |y − e| ≤
`β y ←


1
1
log

β

for every β ∈ (0, 1).

4.

ACCURACY-DEPENDENT PRIVACY

Let us begin with our first class of private algorithms, where
privacy follows from an accuracy property. For our purposes, these
accuracy properties are non-relational probabilistic properties that
hold on a single execution of a single program. For instance, the
assertion Pr[x > 0] < 0.2, stating that the probability x is positive
is at most 0.2, is an accuracy property. Accuracy properties appear
in privacy proofs in a variety of ways. For instance, they may imply
that the privacy cost  is smaller than expected. Or, privacy may be
conditional: if the accuracy property holds then we have differential
privacy, otherwise the algorithm fails and there is no guarantee.
Programs in the latter case satisfy (, δ)-differential privacy, where
the probability of failure is included in δ.

4.1

Up-to-bad reasoning

To integrate accuracy assertions into apRHL, we will use a
technique from cryptographic verification: up-to-bad reasoning.
Roughly speaking, rather than directly proving the equality lifting
corresponding to differential privacy:
µ1 (=)](,δ) µ2 ,
we will prove a conditional, up-to-bad lifting:
µ1 {(x1 , x2 ) | (¬Φ(x1 , x2 ) → x1 = x2 )}](,δ) µ2 .
Here, Φ is an assertion involving just variables from one side.
Roughly speaking, the lifting shows that if the bad event Φ does not
hold, then we have differential privacy. Then, we conclude the proof
with a structural rule that combines the bad event assertion—proved
externally in aHL—with the up-to-bad lifting, removing the bad
event while adjusting the privacy parameters (, δ).
To support this reasoning in our program logic, we propose the
two rules in Fig. 3. The rules, [U T B-L] and [U T B-R], internalize
an approximate version of up-to-bad reasoning. If the assertion Θ
holds, then we have the (, δ)-lifting of equality. So, if we know
the probability of ¬Θ is at most δ 0 , then we can show the (, δ +
δ 0 )-differential privacy when Θ is a property of the first run, and
(, δ + e δ 0 )-differential privacy when Θ is a property of the second
run. The asymmetry in the left and right versions of the rule reflects
the asymmetric definition of approximate lifting, which is in turn
inspired by the asymmetric definition of differential privacy.
In order to include these rules, we show that they are valid. To
prove the equality lifting for privacy, we would like to use the equivalence in Proposition 11. However, there is a catch: we only know
that the distributions over e are differentially private—the distributions over the whole memory may not be differentially private.

A SSN

C OND

` x1 ← e1 ∼h0,0i x2 ← e2 : Ψ {e1 h1i, e2 h2i/x1 h1i, x2 h2i} =⇒ Ψ

` c1 ∼h,δi c2 : Φ ∧ b1 h1i =⇒ Ψ
` c01 ∼h,δi c02 : Φ ∧ ¬b1 h1i =⇒ Ψ
` if b1 then c1 else c01 ∼h,δi if b2 then c2 else c02 : Φ ∧ b1 h1i = b2 h2i =⇒ Ψ
S EQ

W HILE

` c1 ∼h,δi c2 : Φ =⇒ Ψ0
` c01 ∼h0 ,δ0 i c02 : Ψ0 =⇒ Ψ
` c1 ; c01 ∼h+0 ,δ+δ0 i c2 ; c02 : Φ =⇒ Ψ

` c1 ∼hk ,δk i c2 : Θ ∧ b1 h1i ∧ b2 h2i ∧ eh1i = k =⇒ Θ ∧ b1 h1i = b2 h2i ∧ eh1i < k
|= Θ ∧ eh1i ≤ 0 → ¬b1 h1i
` while b1 do c1 ∼hPn k ,Pn δk i while b2 do c2 : Θ ∧ b1 h1i = b2 h2i ∧ eh1i ≤ n =⇒ Θ ∧ ¬b1 h1i ∧ ¬b2 h2i
k=1

L AP N ULL
L AP G EN

k=1

y1 ∈
/ F V (e1 )
y2 ∈
/ F V (e2 )
$ L (e ) : > =⇒ y h1i − y h2i = e h1i − e h2i
$ L (e ) ∼
y
` y1 ←
1
2
1
2
 1
h0,0i 2 ←  2

0
$
$ L (e ) ∼ 0
` y1 ←
 1
hk ·,0i y2 ← L (e2 ) : |k + e1 h1i − e2 h2i| ≤ k =⇒ y1 h1i + k = y2 h2i

C ONSEQ

` Φ0 ∼h0 ,δ0 i c1 : c2 =⇒ Ψ0

F RAME

|= Φ → Φ0
|= Ψ0 → Ψ
` c1 ∼h,δi c2 : Φ =⇒ Ψ

0 ≤ 

δ0 ≤ δ

` c1 ∼h,δi c2 : Φ =⇒ Ψ
F V (Θ) ∩ M V (c1 , c2 ) = ∅
` c1 ∼h,δi c2 : Φ ∧ Θ =⇒ Ψ ∧ Θ

PW-E Q

∀i. ` c1 ∼h,δi i c2 : Φ =⇒ xh1i = i → xh2i = i
` c1 ∼h,P δi i c2 : Φ =⇒ xh1i = xh2i
i∈I

Figure 2: Selected proof rules of apRHL [6, 10]

U T B-L

U T B-R

|= Φ → Φ0 h1i

` c ∼h,δi c0 : Φ =⇒ Θh1i → eh1i = eh2i
` c ∼h,δ+δ0 i c0 : Φ =⇒ eh1i = eh2i

`δ0 c : Φ0 =⇒ Θ

|= Φ → Φ0 h2i

` c ∼h,δi c0 : Φ =⇒ Θh2i → eh1i = eh2i
` c ∼h,δ+e δ0 i c0 : Φ =⇒ eh1i = eh2i

`δ0 c0 : Φ0 =⇒ Θ

Figure 3: Up-to-bad rules
Therefore, we will use a new property of approximate liftings: they
are well-behaved when mapping the underlying distribution.
Proposition 12. For a function f : A → B, let f ] : Distr(A) →
Distr(B) denote function lifted to a map on distributions. If f is
surjective, and R is a relation on B, then

Theorem 13. The rules [U T B-L] and [U T B-R] are sound.
Proof. We will start with [U TB -L]. Take any two memories
(m1 , m2 ) such that (m1 , m2 ) |= Φ, and let µ1 , µ2 be [[c]]m1 and
[[c0 ]]m2 respectively. Note that m1 |= Φ0 . By validity of the premise,
we know
Pr [¬Θ] ≤ δ 0

µ1 {(x1 , x2 ) | f (x1 ) R f (x2 )}](,δ) µ2
if and only if

m∼µ1

and we have a pair of witnesses µL , µR for the relation
]

](,δ) ]

f (µ1 ) {(y1 , y2 ) | y1 R y2 }

In particular, if we have a set E of equivalence classes of A
and the distribution µ/E : Distr(E) represents the probability of
being in each equivalence class, taking f : A → E mapping an
element to its equivalence class and R to be the equivalence relation
gives a result by Barthe and Olmedo [2, Proposition 8]:
](,δ)

µ1 (=E )

R , Θh1i → eh1i = eh2i,

f (µ2 ).

](,δ)

µ2 ⇐⇒ µ1 /E (=)

µ2 /E.

This result allows us to prove an approximate lifting for a distribution over memories by proving an approximting lifting for the
distribution over a single variable or expression. We defer the details
of the proof to the appendix. Now, we are ready to show soundness
of the up-to-bad rules.

such that ∆ (µL , µR ) ≤ δ. Our goal is to show that the marginal
distributions of [[e]] in µ1 , µ2 satisfy (, δ + δ 0 )-differential privacy,
i.e. for any set S,
Pr [[[e]]m ∈ S] ≤ e 0Pr [[[e]]m0 ∈ S] + δ + δ 0 .

m∼µ1

m ∼µ2

To begin, we know that
Pr [[[e]]m ∈ S] = Pr [[[e]]m ∈ S ∧ m |= Θ]

m∼µ1

m∼µ1

+ Pr [[[e]]m ∈ S ∧ m |= ¬Θ]
m∼µ1

≤ Pr [[[e]]m ∈ S ∧ m |= Θ] + δ 0
m∼µ1

since the probability of ¬Θ in µ1 is at most δ 0 . Now, we can conclude with the coupling:
Pr [[[e]]m ∈ S ∧ m |= Θ] + δ

PTR returns a default value ⊥. In code:
$ L (DistToInst (d));
dist ←

f
if dist > ln(1/δ)/ + 1 then
r ← f (d);
else
r ← ⊥;
return r

0

m∼µ1

=

Pr

(m,m0 )∼µL

≤ e
≤ e

[[[e]]m ∈ S ∧ m |= Θ] + δ 0

Pr

[[[e]]m ∈ S ∧ m |= Θ] + δ + δ 0

Pr

[[[e]]0m ∈ S] + δ + δ 0

(m,m0 )∼µR
(m,m0 )∼µR

= e 0Pr [[[e]]0m ∈ S] + δ + δ 0 ,
m ∼µ2

where the first inequality uses ∆ (µL , µR ) ≤ δ, while the second
inequality uses (m, m0 ) ∈ supp(µR ). So, the distributions of [[e]]
satisfy differential privacy. By Proposition 11 and Proposition 12
with equivalence classes defined by the value of [[e]], we can conclude soundness of [U T B-L].
We can show soundness of [U T B-R] in a similar way. Let µ1 , µ2
be as above. We can use the coupling as follows:
Pr [[[e]]m ∈ S]

The key to the privacy of PTR is that if the noise when estimating
dist is not too large, then there are two cases. If dist is large, then
there is no privacy cost for releasing the value of q when dist is
large. Otherwise, we return a default value ⊥ revealing nothing. In
either case, we just have privacy cost  from computing the noisy
distance. If the noise when estimating dist is too large (happening
with probability at most δ), we may violate privacy. So, we get an
(, δ)-private algorithm.
Theorem 14. PTR is (, δ)-differentially private for , δ > 0.
Proof sketch. To prove differential privacy, we will use the rule
[U T B-L]. We can take the event Θ to hold exactly when the noise
is not too large:

m∼µ1

=

Pr

(m,m0 )∼µL

≤ e

Pr
0

[[[e]]m ∈ S] + δ

Pr

[[[e]]m ∈ S ∧ m0 |= Θ]

Pr

[[[e]]m ∈ S ∧ m0 |= ¬Θ] + δ

Pr
0

[[[e]]0m ∈ S] + e

(m,m )∼µR


=e

(m,m0 )∼µR

+ e
≤ e

(m,m0 )∼µR

(m,m )∼µR


=e

Θ , |dist − DistToInst f (d)| < ln(1/δ)/.

[[[e]]m ∈ S]

Pr [[[e]]m0 ∈ S] + e

m0 ∼µ2



Pr
0

[m0 |= ¬Θ] + δ

(m,m )∼µR

`δ c : Φh1i =⇒ Θ,
and rule [U T B-L] gives (, δ)-differential privacy.

0

Pr [m |= ¬Θ] + δ

m0 ∼µ2

≤ e 0Pr [[[e]]m0 ∈ S] + δ + e δ 0
m ∼µ2

The first inequality uses the bound on the distance between the witnesses: ∆ (µL , µR ) ≤ δ. The second inequality uses the support of
µR . The final inequality uses the fact that Prm0 ∼µ2 [m0 |= ¬Θ] ≤
δ 0 . Since the distributions of [[e]] in µ1 , µ2 satisfy (, δ + e δ 0 )differential privacy, we can again use Proposition 11 and Proposition 12 to show [U T B-R] is sound.

4.2

Then, we couple the noise to be the same, so that we take the same
branch in both runs. Then, under assumption Θ, we know that if we
estimate that the distance to instability is large and we take the first
branch, then in fact f (dh1i) = f (dh2i) as desired. Finally, using a
tail bound for the Laplace distribution in aHL gives

Propose-Test-Release

To give a small example of up-to-bad reasoning, we can prove
privacy for the Propose-Test-Release (PTR) framework [16, 48], a
classic example of privacy depending on an accuracy guarantee. The
goal is to release the answer to a function f . Rather than adding
noise directly to the answer (which may be non-numeric), PTR
estimates the distance to instability of the database d with respect
to f , denoted DistToInst f (d). This quantity measures the distance
from d to the closest database d0 such that f (d) 6= f (d0 ), where
adjacent databases are at distance 1. We will use the following two
properties of DistToInst:
DistToInst f (d) > 1 → ∀d0 . (Adj(d, d0 ) → f (d) = f (d0 ))
Adj(d, d0 ) → |DistToInst f (d) − DistToInst f (d0 )| ≤ 1
Since the distance itself is private information, PTR first adds
noise to the distance, calling the noisy result dist. If it is large
enough, then PTR returns the value of f with no noise. Otherwise,

5.

ADVANCED COMPOSITION

Advanced composition is a key tool for giving a more precise
privacy analysis of a composition of private programs. In this section,
we extend apRHL with a new loop rule that supports advanced
composition for arbitrary invariants and we show how the rule can
be applied for proving privacy of a non-interactive variant of ASVbt .
Before presenting our solution, we stress that there are some technical challenges in extending apRHL with advanced composition.
On the one hand, apRHL derives its expressiveness from its ability
to reason about arbitrary approximate liftings, and not simply about
approximate liftings for the equality relation; as a consequence,
an advanced composition rule for apRHL should support approximate liftings in order to be useful (in fact, an advanced composition
rule for just approximate liftings of equality would be too weak
for verifying our running example). On the other hand, the proof
of advanced composition is substantially more technical than the
proof for the sequential composition theorem, using sophisticated
results from fields such as martingale theory and hypothesis testing. We overcome these obstacles by showing approximate liftings
from a version of differential privacy; as we saw before, differential privacy is also a consequence of an approximate lifting of
equality. The key observation is that the two witnesses µL and µR
used in the definition of an approximate lifting define a mechanism µ : B → Distr(A1 × A2 ) such that µ(true) = µL and
µ(false) = µR where ∆ (µL , µR ) ≤ δ iff µ is (, δ)-differentially
private. Next, we show how to take advantage of this observation.
Since the (, δ) parameters from approximate lifting are defined
by the -distance ∆ (µ1 , µ2 ) between the two witnesses, we will
first show an advanced composition theorem for -distance.

Proposition 15 (Advanced composition for -distance). Let fi , gi :
A → Distr(A) such that ∆ (fi (a), gi (a)) ≤ δ for every a ∈ A.
For any ω > 0, let:
p

∗ ,
2n ln(1/ω)  + n(e − 1) and δ ∗ , nδ + ω.
Then for every n ∈ N and a ∈ A, ∆∗ (f n (a), g n (a)) ≤ δ ∗ .
Proof. Let hi : A → B → Distr(A) be such that for every
a ∈ A, hi (a, true) = fi (a) and hi (a, false) = gi (a). Then
∆ (fi (a), gi (a)) ≤ δ iff hi (a) : B → Distr(A) is (, δ)differentially private for every a ∈ A.
By directly applying the advanced composition theorem of differential privacy (Theorem 7), the function hn (a) : B → Distr(A)
is (∗ , δ ∗ )-differentially private for each a ∈ A. So for every
b, b0 ∈ B and a ∈ A, ∆∗ (hn (a, b), hn (a, b0 )) ≤ δ ∗ . Now for
every a ∈ A, hn (a, true) = f n (a) and hn (a, false) = g n (a).
Therefore, ∆∗ (f n (a), g n (a)) ≤ δ ∗ .
Now that we have an advanced composition for -distance, it is
a simple matter to extend our result to approximate liftings. Note
here that we apply advanced composition not to the distributions
on A—which are related by an approximate lifting, but perhaps not
related by differential privacy—but rather to the two witnesses of
the lifting, distributions on pairs in A × A.
Proposition 16 (Advanced composition for lifting). Let fi , fi0 :
A → Distr(A) and Φ ⊆ A × A such that for every a, a0 ∈ A,
(a, a0 ) |= Φ implies
fi (a) Φ](,δ) fi0 (a0 ).
Let n ∈ N and let (0 , δ 0 ) be as in Theorem 7. For any ω > 0, let
p

0 ,
2n ln(1/ω)  + n(e − 1) and δ 0 , nδ + ω.
Then for every a, a0 ∈ A such that (a, a0 ) |= Φ, we have
0

f n (a) Φ](

,δ 0 )

f 0n (a0 ).

Proof. We can map any pair (a, a0 ) ∈ Φ to the left and right
witnesses of the approximate lifting. That is, there exists hli , hri :
(A × A) → Distr(A × A) such that for every (a, a0 ) |= Φ:
• π1 (hli (a, a0 )) = fi (a) and π2 (hri (a, a0 )) = fi0 (a0 )
• supp(hli (a, a0 )) ⊆ Φ and supp(hri (a, a0 )) ⊆ Φ
• ∆ (hli (a, a0 ), hri (a, a0 )) ≤ δ
Without loss of generality, we can assume that hli (a, a0 ) =
hri (a, a0 ) = 0 if (a, a0 ) |= ¬Φ. By Proposition 15, we also
have ∆0 (hli (a, a0 ), hri (a, a0 )) ≤ δ 0 for every i ∈ N and
(a, a0 ) |= Φ. By induction on i, for every (a, a0 ) |= Φ we
have supp((hl )n (a, a0 )) ⊆ Φ and supp((hr )n (a, a0 )) ⊆ Φ,
π1 ((hl )n (a, a0 )) = f n (a) and π2 ((hr )n (a, a0 )) = fi0n (a0 ).
We remark that our connection between the witnesses of liftings
and differential privacy allows us to directly import other composition theorems of differential privacy and their proofs without change.
For instance, Kairouz et al. [32] consider two variants of advanced
composition: an optimal variant that provably gives the best bound
on  and δ, and a heterogeneous variant that allows  and δ be different for the different mechanisms. In unpublished work, Rogers
et al. [43] consider a version of the advanced composition theorem
where the privacy level i and δi for the i-th mechanism may be
chosen adaptively, i.e., depending on the results from the first i − 1

mechanisms. These composition theorems are quite tricky to prove,
involving sophisticated tools from martingale theory and hypothesis
testing. We expect that we can internalize all of these composition
theorems—and directly generalize to liftings—with minimal effort.
Based on the previous result, we introduce a new rule [ACW HILE ] that formalizes advanced composition for loops. The soundness for the new rule, which is given in Fig. 4 follows immediately
from the results of the previous section.
Theorem 17. The rule [AC-W HILE ] is sound.

6.

INTERACTIVE PRIVACY

So far, we have seen how to incorporate composition theorems
and accuracy proofs into our logic. Now, we consider the last piece
needed to verify ASVbt : proving privacy for interactive algorithms.
To date, privacy has only been formally verified for algorithms where
the entire input is available in a single piece; such algorithms are
called offline algorithms. In contrast, interactive or online algorithms
accept input piece by piece, in a finite stream of input, and must
produce an intermediate outputs as inputs arrive.
The differential literature proposes several interactive algorithms;
examples include private counters [14, 21], the Sparse Vector mechanism, and other algorithms using these mechanisms [30]. The main
difficulty in verifying privacy is to model adaptivity: later inputs can
depend on earlier outputs. Indeed, differential privacy behaves well
under adaptivity, a highly useful property enabling applications to
adaptive data analysis and statistics [23].
We can view adaptive inputs as controlled by an adversary, who
receives earlier outputs and selects the next input. We draw on techniques for formally verifying cryptographic proofs, which often also
involve an adversary who is trying to break the protocol. We take
inspiration from the treatment of adversaries in the logic pRHL,
an exact version of apRHL that has been used for verifying cryptographic proofs [4]. Specifically, we extend apRHL with a rule
[A DV ] for the adversary. The rule, displayed in Figure 5, generalizes the adversary rule from pRHL; let Φ an assertion that does not
contain any adversary variable, and assume that the adversary A
has access to oracles O1 , . . . , On and that each oracle guarantees
equality of outputs and an invariant Φ, provided it is called on equal
inputs that satisfy Φ. Then, A guarantees equality of outputs and
an invariant Φ, provided it is called on equal inputs that satisfy Φ.
Moreover,
theP
privacy cost of calling the adversary A is equal to
P
n
h n
k=1 qk k ,
k=1 qk δk i where hi , δi i is the cost of calling once
the oracle Oi , and qi is the maximal number of adversarial queries
for oracle Oi . One can prove the soundness of the adversary rule by
induction on the code of the adversary.
Proposition 18. The rule [A DV ] is sound.
Note that the proof of sparse vector only makes a restricted use of
the [A DV ] rule: as A does not have access to any oracle, the pRHL
rule suffices for the proof. However, the following, oracle based,
presentation of sparse vector uses the full power of the [A DV ] rule:
l ← [];
$ L
u←
/2 (0);
A ← a − u;
B ← b + u;
x ← AO ();
return l
where O is an oracle that takes a query and checks whether it is
between thresholds and updates a public list l, and A is allowed
to query O up to N times. In addition, we note that our new rule
can also be useful for cryptographic proofs which involve reasoning
about statistical distance.

AC-W HILE

p

|= Θ ∧ eh1i ≤ 0 → ¬b1 h1i
∗ ,
2n ln(1/ω)  + n(e − 1)
δ ∗ , nδ + ω
ω>0
` c1 ∼h,δi c2 : Θ ∧ b1 h1i ∧ b2 h2i ∧ eh1i = k =⇒ Θ ∧ b1 h1i = b2 h2i ∧ eh1i < k
` while b1 do c1 ∼h∗ ,δ∗ i while b2 do c2 : Θ ∧ b1 h1i = b2 h2i ∧ eh1i ≤ n =⇒ Θ ∧ ¬b1 h1i ∧ ¬b2 h2i
Figure 4: Advanced composition rule

A DV

` ~x ← A(~e) ∼hPn

k=1

∀i, ~
y , ~z. ` ~
y ← Oi (~z) ∼hi ,δi i ~
y ← Oi (~z) : ~zh1i = ~zh2i ∧ Φ =⇒ ~
y h1i = ~
y h2i ∧ Φ
Pn
~
x
←
A(~
e
)
:
~
e
h1i
=
~
e
h2i
∧
x
h1i
=
x
h2i
∧
Φ
=⇒
~
x
h1i
=~
xh2i ∧ xA h1i = xA h2i ∧ Φ
A
A
qk δk i
qk k ,
k=1

where q1 , . . . , qn are the maximal number of queries that A can make to oracles O1 , . . . , On and xA is the state of the adversary.
Figure 5: Adversary rule

7.

OPTIMAL SUBSET COUPLING

The privacy proof of ASVbt relies on a new interval coupling
rule [L AP I NT ] for Laplace sampling, Fig. 6. This rule allows us to
relate a larger interval with a smaller interval nested inside. That
is, we can assume that the sample y1 h1i lies in [p, q] if and only if
the sample y2 h2i lies in [r, s] contained in [p, q]. The privacy cost
depends on two things: the difference in sizes of the two intervals
(q − p) − (s − r), and the size of the inner interval s − r. Roughly,
a larger inner interval and smaller outer interval yield a smaller
privacy cost.
To show that this rule is sound, we will first prove a general
construction for liftings of the form
µ (y1 ∈ P ↔ y2 ∈ Q)](,0) µ
for Q ⊆ P . We call such such liftings subset couplings, since they
relate a set of outputs to a subset of outputs. Our construction applies
to all discrete distributions, and is optimal in a precise sense: among
all liftings of the relation, our construction gives the smallest (i.e.,
the most precise) .
Theorem 19 (Optimal subset coupling). Let µ be a distribution over
S, and consider two proper subsets P, Q of S such that Q ⊆ P .
Then µ(P ) ≤ αµ(Q) if and only if the following lifting holds:
µ R](ln α,0) µ
where the relation R is defined by the following clause:
(y1 , y2 ) ∈ R , y1 ∈ P ↔ y2 ∈ Q

Here, x0 is an arbitrary element of S \ P . We set λ = µ(Q)/µ(P ).
Note that λ satisfies:
λ = (1 − λ)

µ(Q)
.
µ(P \ Q)

For the witnesses, it is not hard to see that the marginal conditions are
satisfied, and that x R y for all pairs (x, y) in the supports of µL and
µR . Furthermore, for all x ∈ P and y ∈ Q, we have µL (x, y) =
(1/λ) · µR (x, y) by our choice of λ. By the condition on marginals
and the support, we have a (ln(1/λ), 0)-lifting. This immediately
implies the (ln α, 0)-lifting for any α ≥ 1/λ = µ(P )/µ(Q).
This result is very much in the spirit of the optimal or maximal
coupling for exact probabilistic couplings (see, e.g., [49]). By computing the total variation distance between two distributions, the
maximal coupling construction shows how to create a coupling that
exactly realizes the total variation distance.
Similarly, by the optimal subset coupling, we can construct a
subset coupling and calculate the distance  in the lifting by simply
proving a property of the discrete Laplace distribution. Formally, let
L (v) for v ∈ Z have distribution over Z with probability proportional to
Pr[r] ∝ exp(−|r − v|).
We write L to mean L (0). We will use the following property, a
discrete version of Bun et al. [13, Claim 5.13].
Lemma 20. Let r be a draw from L , and take a, a0 , b, b0 ∈ Z such
that a < b and [a, b] ⊆ [a0 , b0 ]. Then,
Pr[r ∈ [a0 , b0 ]] ≤ α Pr[r ∈ [a, b]]

Proof. The reverse direction follows from the fundamental lemma
of approximate liftings [2]. For the forward implication, we construct two witnesses. Note that the theorem is trivial if µ(P \Q) = 0
since we can just take the identity coupling, so we will assume otherwise. Define the following witnesses:


if x ∈
/ P \Q∧x=y
µ(x)
if x ∈ P \ Q ∧ y ∈ Q
µL (x, y) = µ(x)µ(y)
µ(Q)


0
otherwise.

µ(y)
if x = y ∧ y ∈
/P





λ
·
µ(y)
if
x
=
y
∧
y
∈
Q

if
x
∈
P
\
Q
∧
y∈Q
µR (x, y) = (1−λ)µ(x)µ(y)
µ(P \Q)



µ(y)
if x = x0 ∈ S \ P ∧ y ∈ P \ Q



0
otherwise.

with
α=

exp(η)
,
1 − exp(−(b − a + 2)/2)

η = (b0 − a0 ) − (b − a).

The proof follows by a small calculation; we defer the details to
the appendix. With this property, we can now prove soundness of
our subset rule for sampling from the Laplace distribution.
Theorem 21. The rule [L AP I NT ] is sound.
Proof. Suppose that [[eh1i]] = v1 , [[eh2i]] = v2 , and |v1 − v2 | =
∆ ≤ k. Let the noises be w1 = xh1i − v1 , w2 = xh2i = v2 ; note
that both samples are distributed as L (0). Note that xh1i ∈ [a0 , b0 ]
exactly when w1 ∈ [a0 − v1 , b0 − v1 ], and similarly for x2 and w2 .
By Proposition 12, to show a lifting on memories, it suffices to find
a lifting on the distribution over the sampled variable y, taking f

0 , ln
L AP I NT



exp(η)
1 − exp(−σ/2)


Φ , |eh1i − eh2i| ≤ k ∧ (p + k ≤ r < s ≤ q − k) ∧ (q − p) − (s − r) ≤ η ∧ 0 < σ ≤ (s − r) + 2
$
$ L (e) ∼ 0
` y1 ←

h ,0i y2 ← L (e) : Φ =⇒ y1 h1i ∈ [p, q] ↔ y2 h2i ∈ [r, s]

Figure 6: Interval coupling for Laplace
to be the function that maps a memory m to the value m(y). So, it
suffices to show
0

L (0) {w1 ∈ I1 ↔ w2 ∈ I2 }](

,0)

L (0)

where I1 , [a0 − v1 , b0 − v1 ] and I2 , [a − v2 , b − v2 ]. Since
ah1i + k ≤ ah2i and bh1i ≤ bh2i − k, we know I2 ⊆ I1 . Then,
we can directly apply Lemma 20 on these two intervals with η =
|I1 | − |I2 | = (b0 − a0 ) − (b − a), and we are done.

8.

PROVING PRIVACY FOR ASVbt
We verify differential privacy for the full version of ASVbt with
an adaptive adversary that chooses its queries interactively. We recall
the theorem.
Theorem 22. Let  and δ both be in (0, 1). Set

.
0 , p
4 2M ln(2/δ)
If all adversarial queries q are 1-sensitive (i.e. |evalQ(q, d) −
evalQ(q, d0 )| ≤ 1 for every adjacent databases d and d0 ), then
ASVbt is (, δ)-differentially private. Formally,
` ASVbt ∼h,δi ASVbt : Φ =⇒ rh1i = rh2i
where Φ is defined as
={a,b,N,qs} ∧Adj(dh1i, dh2i) ∧ bh1i − ah1i ≥ γ

Threshold coupling. Let ct be the initialization command, including all commands before the loop. First, we can prove:

for
6
4
γ , 0 ln(4/0 ) + ln(2/δ).


Proof sketch. Now, we put everything together to prove ASVbt is
(, δ)-private algorithm. We present just the key points of the proof
here; the full proof is formalized in the EasyCrypt system. We first
transform the algorithm to an equivalent algorithm:4

ASVbt (a, b, M, N, d) :=
i ← 0; l ← [];
$ L
u←
/2 (0);
A ← a − u; B ← b + u;
while i < N ∧ |l| < M do
i0 ← i; hd ← −1;
while i0 < N do
if (hd = −1)
q ← A(l);
$ L 0
S←
 /3 (evalQ(q, d));
if (A ≤ S ≤ B) then hd ← i;
i ← i + 1;
i0 ← i0 + 1;
if (hd 6= −1) then l ← hd :: l;
return l
4

The main change is that the loop iterations in Fig. 1 are grouped
into blocks of queries, each handled by an inner loop. Each outer
iteration now corresponds to finding a single query between the
thresholds. The inner iterations loop through the queries until there
is a between threshold query. To allow the inner loop to be analyzed
in a synchronized fashion, the inner loop always continues up to
iteration N , doing nothing for all iterations beyond the first between
threshold query.
This transformation allows us to use both advanced composition
and pointwise equality. At a high level, we follow four steps. First,
we set up the threshold noise, so that the noisy interval [A, B]
is smaller in the first run than in the second run; this costs a bit
of privacy. Then, we handle the loop working inside to out: we
apply the adversary rule, the subset coupling, and pointwise equality
to the inner loop to show privacy for each block of queries that
stops as soon as we see a between threshold query, assuming that
the noisy intervals [A, B] are sufficiently large. Next, we apply
advanced composition to bound the privacy cost of the outer loop,
still assuming [A, B] is sufficiently large. Finally, we use up-to-bad
reasoning to remove this assumption, increasing δ slightly for the
final (, δ)-privacy bound.
We now detail each step. To reduce notation, we will suppress the
adjacency predicate Adj(dh1i, dh2i) which is preserved throughout
the computation and the proof.

We have formally verified equivalence of this program with the
program in Fig. 1 by using a recently-proposed asynchronous loop
rule [3].

` ct ∼h  ,0i ct : Φ =⇒ Φ0
2
where Φ0 , Ah1i + 1 = Ah2i ∧ Bh1i = Bh2i + 1, by applying
the rule [L AP G EN ] to ensure uh1i = uh2i + 1 as a post-condition.
This step costs (/2, 0) privacy.

The inner loop. For the inner loop, we will assume the threshold
condition Φ0 and lh1i = lh2i initially; both conditions are preserved
by the inner loop. We will also assume that the noisy interval [A, B]
is sufficiently large:5
6
ln(4/0 ).
0
Let ci be the inner loop. We will first prove the pointwise judgment:
Ψ,B−A≥

`ci ∼h0 ,0i ci :
Φ0 ∧ Ψh1i ∧ lh1i = lh2i =⇒ (hdh1i = v) → (hdh2i = v)
(1)
for each index v.
We focus on the case where 0 ≤ v ≤ N , as other cases are easy.
First, we apply the [W HILE ] rule, with i = 0 except for i = v,
where we set v = 2 . Whenever we call the adversary for the next
query, we know that lh1i = lh2i, so we may apply adversary rule
with cost (0, 0) to ensure that qh1i = qh2i throughout.
Then, the proof for the rest of the loop body goes as follows:
5
While Ψ does not have tagged variables, we will later interpret A
and B as coming from the first run.

• For the iterations i < v and i > v, we use the rule [L AP N ULL ] to couple the noisy query answers Sh1i, Sh2i. This
has no privacy cost and preserves the invariant.
• For the iteration i = v, suppose that Sh1i ∈ [Ah1i, Bh1i]
(otherwise we are done). We can apply a coupling for the
Laplace distribution, [L AP I NT ], to ensure that Sh2i ∈
[Ah2i, Bh2i] as well. Under Ψh1i and the coupling on
the noisy thresholds Φ0 , the inner interval [Ah2i, Bh2i]
has size at least (6/0 ) ln(4/0 ) − 2. Taking (p, q, r, s) =
(Ah1i, Bh1i, Ah2i, Bh2i), η = 2, σ = (6/0 ) ln(4/0 ), and
k = 1, a calculation6 shows that [L AP I NT ] gives a (0 , 0)lifting so the critical iteration has privacy cost 0 .
This establishes Eq. (1). By the pointwise equality rule [PW-E Q ],
we have:
` ci ∼h0 ,0i ci : Φ0 ∧ Ψh1i ∧ lh1i = lh2i =⇒ hdh1i = hdh2i
By [F RAME ] and some manipulations, we can assume that lh1i =
lh2i at the end of each iteration of the outer loop.

The outer loop. For the outer loop, we apply advanced composition. Letting co be the outer loop, our choice of 0 and corresponds
to the setting in Theorem 7, so we have the following judgment by
[AC-W HILE ]:
` co ∼h/2,0i co : lh1i = lh2i ∧ Φ0 ∧ Ψh1i =⇒ lh1i = lh2i.
Since co does not modify the thresholds and preserves Ψh1i,
[F RAME ] and some manipulations allows us to move this assertion into the post-condition:
` co ∼h/2,0i co : lh1i = lh2i ∧ Φ0 =⇒ Ψh1i → lh1i = lh2i.

Applying up-to-bad reasoning. Finally, we can apply [S EQ ]
with our judgement for the initialization ci and the outer loop co ,
giving:
` ASVbt ∼h/2,0i ASVbt : Φ0 =⇒ Ψh1i → lh1i = lh2i
for
Φ0 , ={a,b,N,qs} ∧ Adj(dh1i, dh2i) ∧ bh1i − ah1i ≥ γ.
To conclude the proof, all that remains is to remove the assertion
Ψh1i. We will bound the probability that Ψh1i does not hold. The
accuracy rule for the Laplace mechanism gives
$ L
`δ u ←
/2 (0) : b − a ≥ γ =⇒ |u| ≤

2
log(1/δ),


from which we can conclude
`δ ASVbt : b − a ≥ γ =⇒ Ψ.
6

We will show that for λ ∈ (0, 1/2), we have
exp(2λ/3)
≤ exp(λ)
1 − exp(−σλ/6)

when σ ≥ (6/λ) ln(4/λ). Substituting, it suffices to show:
exp(2λ/3)
≤ exp(λ)
1 − λ/4
λ/4 + exp(−λ/3) − 1 ≤ 0.
Since the function on the left is convex in λ, the maximum occurs
on the boundary of the domain. We can directly check that the
inequality holds at λ = {0, 1/2}, and we are done.

Finally, applying [U T B-L] yields the desired judgment:
` ASVbt ∼h/2,δi ASVbt : Φ0 =⇒ lh1i = lh2i

9.

RELATED WORKS

Differential privacy [19] has been an area of intensive research
in the last decade. We refer readers interested in a more comprehensive treatment of the algorithmic aspects of differential privacy
to the excellent monograph by Dwork and Roth [17]. Several tools
have been developed to support the development of differentially
private data analysis. PINQ [36] internalizes the use of standard
composition in the form of a privacy budget management platform,
Airavat [45] uses differential privacy combined with the map-reduce
approach, GUPT [40] implements the general idea of sample and
aggregate [41]. Other tools implement algorithms targeting specific
applications like: location data [35], genomic data [27, 47], mobility
data [37], and browser error reports [26].
Several tools have been proposed for providing formal verification of the differential privacy guarantee, using a wide variety of
verification approaches: dynamic checking [24, 36], relational program logic [2, 6] and relational refinement type systems [9], linear
(dependent) type systems [29, 42], product programs [7], methods based on computing bisimulations families for probabilistic
automata [50, 51], and methods based on counting variants of satisfiability modulo theories [28]. None of these techniques can handle
advanced composition, interactive online algorithms and privacy
depending on accuracy. Barthe et al. [5] present a system for reasoning about computational differential privacy [39] a relaxation of
differential privacy where the adversary are computationally-bound.
Coupling is an established tool in probability theory, but it seems
less familiar to computer science. It was only quite recently that
couplings have been used in cryptography; according to Hoang and
Rogaway [31], who use couplings to reason about generalized Feistel networks, Mironov [38] first used this technique in his analysis
of RC4. There are seemingly few applications of coupling in formal
verification, despite considerable research on probabilistic bisimulation (first introduced by Larsen and Skou [33]) and probabilistic
relational program logics (first introduced by Barthe et al. [4]).
The connection between liftings and couplings was recently noted
by Barthe et al. [8] and explored for differential privacy by Barthe
et al. [10]. The latter uses a coupling argument to prove differentially private the sparse vector algorithm that we also consider in
this work. The additional challenges that we face are: first, the integration of advanced composition, providing a much better privacy
bound; second, the proof that sparse vector is differentially private
also in the interactive model, which requires additionally to have a
logic that permits to reason about the adversary. Moreover, Barthe
et al. [10] do not provide methods to prove privacy using accuracy.
In promising recent work, Zhang and Kifer [52] design a system
to automatically verify differentially privacy for examples where
the privacy proof uses tools beyond the standard composition theorem, including the Sparse Vector technique. Their proof strategy
is morally similar to couplings, but their work uses a combination
of product programs and lightweight refinement types backed by
novel type-inference techniques, rather than a relational program
logic like we consider. Their system can also optimize the privacy
cost, something that we do not consider. While their work is highly
automated, their system is limited to pure, (, 0) differential privacy,
so it cannot verify the algorithms we consider, where privacy follows from accuracy or the advanced composition theorem. Their
techniques also seem limited to modeling couplings that arise from
bijections; in particular, it is not clear how to prove privacy for ex-

amples that use more advanced couplings like the optimal subset
coupling.

10.

CONCLUDING REMARKS

We have presented an extension of the logic apRHL [6] that
can express three classes of privacy proofs beyond current state-ofthe-art techniques for privacy verification: privacy depending on
accuracy, privacy from advanced composition, and privacy for interactive algorithm. We have formalized a generalization of the adaptive Sparse Vector algorithm, known as Between Thresholds [13].
This and other possible generalizations of sparse vector could bring
interesting results in domains like geo-indistinguishability [1].
For the future, it would be interesting to explore generalizations
of differential privacy like the recent notion of concentrated differential privacy [12, 18]. This generalization features a simple
composition principle that internalizes the advanced composition
principle of standard differential privacy. However, it is currently
unclear whether the definition of concentrated differential privacy,
which involves Rényi divergences, can be modeled using apRHL.
Additionally, there is still room for improving the expressivity of
apRHL for differential privacy. One interesting example combining accuracy and privacy is the large margin mechanism [15]. The
privacy proof for this algorithm requires careful reasoning about
the size of the support when applying pointwise equality, and sophisticated facts about the accuracy Sparse Vector. This example
seems beyond the reach of our techniques, but we believe it could
be handled by generalizing the existing rules.
Finally, it would be interesting to explore a tighter integration of
accuracy and privacy proofs. We currently use two systems, aHL
and apRHL, to verify privacy. This can lead to awkward proofs
since the two logics can only interact in specific places in the proof
(i.e., the up-to-bad rules). A combined version of the logics could
allow more natural proofs.

References
[1] M. E. Andrés, N. E. Bordenabe, K. Chatzikokolakis, and
C. Palamidessi. Geo-indistinguishability: differential privacy
for location-based systems. In ACM SIGSAC Conference on
Computer and Communications Security (CCS), Berlin, Germany, pages 901–914, 2013.
[2] G. Barthe and F. 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, 2013.
[3] G. Barthe, B. Grégoire, J. Hsu, and P.-Y. Strub. Coupling
proofs are probabilistic product programs.
[4] G. Barthe, B. Grégoire, and S. Zanella-Béguelin. Formal
certification of code-based cryptographic proofs. In ACM
SIGPLAN–SIGACT Symposium on Principles of Programming
Languages (POPL), Savannah, Georgia, pages 90–101, New
York, 2009.
[5] G. Barthe, G. Danezis, B. Grégoire, C. Kunz, and S. Z.
Béguelin. Verified computational differential privacy with
applications to smart metering. In IEEE Computer Security Foundations Symposium (CSF), New Orleans, Louisiana,
pages 287–301, 2013.

[6] G. Barthe, B. Köpf, F. Olmedo, and S. Zanella-Béguelin. Probabilistic relational reasoning for differential privacy. ACM
Transactions on Programming Languages and Systems, 35(3):
9, 2013.
[7] G. Barthe, M. Gaboardi, E. J. Gallego Arias, J. Hsu, C. Kunz,
and P.-Y. Strub. Proving differential privacy in Hoare logic.
In IEEE Computer Security Foundations Symposium (CSF),
Vienna, Austria, 2014.
[8] G. Barthe, T. Espitau, B. Grégoire, J. Hsu, L. Stefanesco, and
P.-Y. Strub. Relational reasoning via probabilistic coupling. In
International Conference on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR), Suva, Fiji, volume 9450,
pages 387–401, 2015.
[9] G. Barthe, M. Gaboardi, E. J. Gallego Arias, J. Hsu, A. Roth,
and P.-Y. Strub. Higher-order approximate relational refinement types for mechanism design and differential privacy. In
ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India, 2015.
[10] G. Barthe, M. Gaboardi, B. Grégoire, J. Hsu, and P.-Y. Strub.
Proving differential privacy via probabilistic couplings. In
IEEE Symposium on Logic in Computer Science (LICS), New
York, New York, 2016.
[11] G. Barthe, M. Gaboardi, B. Grégoire, J. Hsu, and P.-Y. Strub. A
program logic for union bounds. In International Colloquium
on Automata, Languages and Programming (ICALP), Rome,
Italy, 2016.
[12] M. Bun and T. Steinke. Concentrated Differential Privacy:
Simplifications, Extensions, and Lower Bounds. May 2016.
[13] M. Bun, T. Steinke, and J. Ullman. Make Up Your Mind: The
Price of Online Queries in Differential Privacy. Apr. 2016.
[14] T.-H. H. Chan, E. Shi, and D. Song. Private and continual
release of statistics. ACM Transactions on Information and
System Security, 14(3):26, 2011.
[15] K. Chaudhuri, D. J. Hsu, and S. Song. The large margin mechanism for differentially private maximization. In Conference
on Neural Information Processing Systems (NIPS), Montréal,
Québec, pages 1287–1295, 2014.
[16] C. Dwork and J. Lei. Differential privacy and robust statistics.
In ACM SIGACT Symposium on Theory of Computing (STOC),
Bethesda, Maryland, pages 371–380, 2009.
[17] C. Dwork and A. Roth. The algorithmic foundations of differential privacy. Foundations and Trends in Theoretical Computer Science, 9(3–4):211–407, 2014.
[18] C. Dwork and G. N. Rothblum. Concentrated Differential
Privacy. Mar. 2016.
[19] C. Dwork, F. McSherry, K. Nissim, and A. Smith. Calibrating
noise to sensitivity in private data analysis. In IACR Theory of
Cryptography Conference (TCC), New York, New York, pages
265–284, 2006.
[20] C. Dwork, M. Naor, O. Reingold, G. N. Rothblum, and
S. P. Vadhan. On the complexity of differentially private
data release: efficient algorithms and hardness results. In
ACM SIGACT Symposium on Theory of Computing (STOC),
Bethesda, Maryland, pages 381–390, 2009.

[21] C. Dwork, M. Naor, T. Pitassi, and G. N. Rothblum. Differential privacy under continual observation. In ACM SIGACT
Symposium on Theory of Computing (STOC), Cambridge, Massachusetts, pages 715–724, 2010.
[22] C. Dwork, G. N. Rothblum, and S. Vadhan. Boosting and
differential privacy. In IEEE Symposium on Foundations of
Computer Science (FOCS), Las Vegas, Nevada, pages 51––60,
2010.

[36] F. McSherry. Privacy integrated queries. In ACM SIGMOD
International Conference on Management of Data (SIGMOD),
Providence, Rhode Island, 2009.
[37] D. J. Mir, S. Isaacman, R. Cáceres, M. Martonosi, and R. N.
Wright. DP-WHERE: differentially private modeling of human
mobility. In IEEE International Conference on Big Data
(ICBD), Santa Clara, California, pages 580–588, 2013.

[23] C. Dwork, V. Feldman, M. Hardt, T. Pitassi, O. Reingold, and
A. Roth. The reusable holdout: Preserving validity in adaptive
data analysis. Science, 349(6248):636–638, 2015.

[38] I. Mironov. (Not so) random shuffles of RC4. In IACR International Cryptology Conference (CRYPTO), Santa Barbara,
California, volume 2442 of Lecture Notes in Computer Science, pages 304–319. Springer, 2002.

[24] H. Ebadi, D. Sands, and G. Schneider. Differential privacy:
Now it’s getting personal. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL),
Mumbai, India, pages 69–81, 2015.

[39] I. Mironov, O. Pandey, O. Reingold, and S. P. Vadhan. Computational differential privacy. In IACR International Cryptology
Conference (CRYPTO), Santa Barbara, California, pages 126–
142, 2009.

[25] F. Eigner and M. Maffei. Differential privacy by typing in
security protocols. In IEEE Computer Security Foundations
Symposium (CSF), New Orleans, Louisiana, pages 272–286,
2013.

[40] P. Mohan, A. Thakurta, E. Shi, D. Song, and D. E. Culler.
GUPT: privacy preserving data analysis made easy. In ACM
SIGMOD International Conference on Management of Data
(SIGMOD), Scottsdale, Arizona, pages 349–360, 2012.

[26] Ú. Erlingsson, V. Pihur, and A. Korolova. RAPPOR: randomized aggregatable privacy-preserving ordinal response. In
ACM SIGSAC Conference on Computer and Communications
Security (CCS), Scottsdale, Arizona, pages 1054–1067, 2014.

[41] K. Nissim, S. Raskhodnikova, and A. Smith. Smooth sensitivity and sampling in private data analysis. In ACM SIGACT
Symposium on Theory of Computing (STOC), San Diego, California, 2007.

[27] S. E. Fienberg, A. B. Slavkovic, and C. Uhler. Privacy preserving GWAS data sharing. In IEEE International Conference on
Data Mining Workshops (ICDMW), Vancouver, British Colombia, pages 628–635, 2011.

[42] J. Reed and B. C. Pierce. Distance makes the types grow
stronger: A calculus for differential privacy. In ACM SIGPLAN
International Conference on Functional Programming (ICFP),
Baltimore, Maryland, 2010.

[28] M. Fredrikson and S. Jha. Satisfiability modulo counting:
a new approach for analyzing privacy properties. In IEEE
Symposium on Logic in Computer Science (LICS), Vienna,
Austria, pages 42:1–42:10, 2014.

[43] R. Rogers, A. Roth, J. Ullman, and S. Vadhan. Privacy odometers and filters: Pay-as-you-go composition. 2016.

[29] M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C.
Pierce. Linear dependent types for differential privacy. In ACM
SIGPLAN–SIGACT Symposium on Principles of Programming
Languages (POPL), Rome, Italy, pages 357–370, 2013.
[30] M. Hardt and G. N. Rothblum. A multiplicative weights mechanism for privacy-preserving data analysis. In IEEE Symposium on Foundations of Computer Science (FOCS), Las Vegas,
Nevada, pages 61–70, 2010.
[31] V. T. Hoang and P. Rogaway. On generalized Feistel networks.
In IACR International Cryptology Conference (CRYPTO),
Santa Barbara, California, volume 6223 of Lecture Notes
in Computer Science, pages 613–630. Springer, 2010.
[32] P. Kairouz, S. Oh, and P. Viswanath. The composition theorem
for differential privacy. 2015.

[44] A. Roth and T. Roughgarden. Interactive privacy via the median mechanism. In ACM SIGACT Symposium on Theory of
Computing (STOC), Cambridge, Massachusetts, pages 765–
774, 2010.
[45] I. Roy, S. T. V. Setty, A. Kilzer, V. Shmatikov, and E. Witchel.
Airavat: Security and privacy for MapReduce. In USENIX
Symposium on Networked Systems Design and Implementation
(NSDI), San Jose, California, pages 297–312, 2010.
[46] R. Shokri and V. Shmatikov. Privacy-preserving deep learning.
In ACM SIGSAC Conference on Computer and Communications Security (CCS), Boulder, Colorado, pages 1310–1321,
2015.
[47] S. Simmons, C. Sahinalp, and B. Berger. Enabling privacypreserving GWAS in heterogenous human populations. In
RECOMB, 2016.

[33] K. G. Larsen and A. Skou. Bisimulation through probabilistic
testing. In ACM Symposium on Principles of Programming
Languages (POPL), Austin, Texas, pages 344–352, 1989.

[48] A. Thakurta and A. Smith. Differentially private feature selection via stability arguments, and the robustness of the lasso.
In Conference on Computational Learning Theory (CoLT),
Princeton, New Jersey, pages 819–850, 2013.

[34] M. Lyu, D. Su, and N. Li. Understanding the sparse vector
technique for differential privacy. 2016.

[49] H. Thorisson. Coupling, Stationarity, and Regeneration.
Springer, 2000.

[35] A. Machanavajjhala, D. Kifer, J. M. Abowd, J. Gehrke, and
L. Vilhuber. Privacy: Theory meets practice on the map. In International Conference on Data Engineering (ICDE), Cancún,
México, pages 277–286, 2008.

[50] M. C. Tschantz, D. Kaynar, and A. Datta. Formal verification of differential privacy for interactive systems (extended
abstract). Electronic Notes in Theoretical Computer Science,
276(0):61–79, 2011.

[51] L. Xu, K. Chatzikokolakis, and H. Lin. Metrics for differential privacy in concurrent systems. In IFIP International
Conference on Formal Techniques for Distributed Objects,
Components and Systems (FORTE), Berlin, Germany, volume
8461 of Lecture Notes in Computer Science, pages 199–215,
June 2014.
[52] D. Zhang and D. Kifer. AutoPriv: Automating differential
privacy proofs. 2016.

µ1 ([a1 ]f ) = 0, then (π1 µL )(a1 ) = 0 = µ1 (a1 ). Otherwise, assume µ1 ([a1 ]f ) 6= 0 and compute:
X
X
µL (a1 , a2 ) =
αL (a1 , a2 )νL (f (a1 ), f (a2 ))
a2

a2

=

X

αL (a1 , a2 )νL (f (a1 ), f (a2 ))

a2 :µ2 ([a2 ]f )=0

+

X

αL (a1 , a2 )νL (f (a1 ), f (a2 ))

a2 :µ2 ([a2 ]f )6=0

APPENDIX
A. OMITTED PROOFS
Proposition 12. For a function f : A → B, let f ] : Distr(A) →
Distr(B) denote function lifted to a map on distributions. If f is
surjective, and R is a relation on B, then
µ1 {(x1 , x2 ) | f (x1 ) R f (x2 )}](,δ) µ2
if and only if

α1 (a1 ) · νL (f (a1 ), f (a2 ))

[a2 ]f :µ2 ([a2 ]f )=0

+

X

α1 (a1 ) · α2 (a2 ) · νL (f (a1 ), f (a2 ))

a2 :µ2 ([a2 ]f )6=0

X

=

α1 (a1 ) · νL (f (a1 ), f (a2 ))

[a2 ]f :µ2 ([a2 ]f )=0

X

+

α1 (a1 ) · νL (f (a1 ), f (a2 ))

[a2 ]f :µ2 ([a2 ]f )6=0

f ] (µ1 ) {(y1 , y2 ) | y1 R y2 }](,δ) f ] (µ2 ).
In particular, if we have a set E of equivalence classes of A
and the distribution µ/E : Distr(E) represents the probability of
being in each equivalence class, taking f : A → E mapping an
element to its equivalence class and R to be the equivalence relation
gives a result by Barthe and Olmedo [2, Proposition 8]:
µ1 (=E )](,δ) µ2 ⇐⇒ µ1 /E (=)](,δ) µ2 /E.
Proof. For the forward direction, take the witnesses µL , µR ∈
Distr(A × A) and define witnesses νL ,(f × f )] (µL ) and
νR ,(f × f )] (µR ). The support condition is clear, the marginal
requirement is clear, and the distance requirement also follows directly: for any set S ⊆ B × B, apply the distance condition on
µL , µR for the set f −1 (S).
For the reverse direction, let νL , νR ∈ Distr(B × B) be the witnesses to the second lifting. We aim to construct a pair of witnesses
µL , µR ∈ Distr(A × A) to the first lifting. The basic idea is to
define µL and µR based on equivalence classes of elements in A
mapping to a particular b ∈ B, and then smooth out the probabilities
within each equivalence class. To begin, for a ∈ A, define
[a]f , f −1 (f (a))

X

=

αi (a) , Prµi [{a} | [a]f ]

We also assume a function ρ that takes a set S and selects an arbitrary
representative ρ(S) ∈ S. We take αi (a) = 0 when µi ([a]f ) = 0.
Now, we define µL and µR as
µL : (a1 , a2 ) 7→ αL (a1 , a2 ) · νL (f (a1 ), f (a2 ))
µR : (a1 , a2 ) 7→ αR (a1 , a2 ) · νR (f (a1 ), f (a2 ))
where


α1 (a1 ) · α2 (a2 ) : µ2 ([a2 ]f ) 6= 0
αL (a1 , a2 ) = α1 (a1 )
: µ2 ([a2 ]f ) = 0 ∧ a2 = ρ([a2 ]f )

0
: otherwise


α1 (a1 ) · α2 (a2 ) : µ1 ([a1 ]f ) 6= 0
αR (a1 , a2 ) = α2 (a2 )
: µ1 ([a1 ]f ) = 0 ∧ a1 = ρ([a1 ]f )

0
: otherwise
The support and marginal conditions follow from the support
and marginal conditions of νL , νR . For instance, note that if

= α1 (a1 )

X

νL (f (a1 ), b2 )

b2 ∈f (A)

= α1 (a1 )µ1 ([a1 ]f ) = µ1 (a1 ).
The last step uses f (A) = B because f is surjective, so we may apply the marginal condition of π1 νL =f ] (µ1 ). A similar calculation
shows π2 µR = µ2 .
We now check the distance condition ∆ (µL , µR ) ≤ δ. Since we
have ∆ (νL , νR ) ≤ δ, we know that
νL (b1 , b2 ) ≤ e νR (b1 , b2 ) + δ(b1 , b2 )
P
for δ(b1 , b2 ) ≥ 0 and b1 ,b2 δ(b1 , b2 ) ≤ δ. We now prove that,
for any (a1 , a2 ) ∈ A × A, we have µL (a1 , a2 ) ≤ e µR (a1 , a2 ) +
ζ(a1 , a2 ) where ζ(a1 , a2 ) , αL (a1 , a2 ) · δ(f (a1 ), f (a2 )). Let
(a1 , a2 ) ∈ A × A and bi , f (ai ). Then, consider a1 ∈ A. If
µ1 ([a1 ]f ) = 0, we can immediately bound
µL (a1 , a2 ) = 0 ≤ e µR (a1 , a2 ) + ζ(a1 , a2 ).
Otherwise, assume µ1 ([a1 ]f ) 6= 0. Then, we can bound:
µL (a1 , a2 ) = αL (a1 , a2 ) · νL (b1 , b2 )
≤ αL (a1 , a2 ) · (e νR (b1 , b2 ) + δ(b1 , b2 ))
= e (αR (a1 , a2 ) · νR (b1 , b2 )) + αL (a1 , a2 ) · δ(b1 , b2 )
= e µR (a1 , a2 ) + αL (a1 , a2 ) · δ(b1 , b2 )
≤ e µR (a1 , a2 ) + ζ(a1 , a2 ).
The third line changes from αL to αR in the first factor. Note that
αL (a1 , a2 ) 6= αR (a1 , a2 ) exactly when µ2 ([a2 ]f ) = 0, when
νR (b1 , b2 ) = 0 as well.
Now, we just need to bound sums of ζ(a1 , a2 ). First, we can
show that the sum of αL within any equivalence class is at most 1.
Consider b1 , b2 . If µ1 (f −1 (b2 )) = 0, then we have
X
X
X
αL (a1 , a2 ) =
α1 (a1 ) ≤ 1.
a1 ∈f −1 (b1 ) a2 ∈f −1 (b2 )

Otherwise, if µ1 (f −1 (b2 )) 6=
α1 (a1 )α2 (a2 ) and again
X
X
a1 ∈f −1 (b1 ) a2 ∈f −1 (b2 )

a1 ∈f −1 (b1 )

0, we have αL (a1 , a2 )
αL (a1 , a2 ) ≤ 1.

≤

Hence,
X
X
ζ(a1 , a2 ) =
δ(b1 , b2 )
a1 ,a2

X

X

αL (a1 , a2 )

a1 ∈f −1 (b1 ) a2 ∈f −1 (b2 )

b1 ,b2

≤

X

δ(b1 , b2 ) ≤ δ.

1 + (η + 1)(e − 1)
e(η+1)
≤
= e ,

1 + η(e − 1)
eη

b1 ,b2

So for any S ⊆ A × A, we have µL (S) ≤ e µR (S) + δ. This
shows that ∆ (µL , µR ) ≤ 0, as desired.
Lemma 20. Let r be a draw from L , and take a, a0 , b, b0 ∈ Z such
that a < b and [a, b] ⊆ [a0 , b0 ]. Then,
Pr[r ∈ [a0 , b0 ]] ≤ α Pr[r ∈ [a, b]]
with
α=

exp(η)
,
1 − exp(−(b − a + 2)/2)

η = (b0 − a0 ) − (b − a).

Proof. We first define some notation. Let W be the total mass of the
Laplace distribution, without normalization. By direct calculation,
W =

+∞
X

exp(−|r|) =

r=−∞

e + 1
.
e − 1

Let L(x, y) be the mass of the Laplace distribution in [x, y] for
x, y ≤ 0. Again by direct calculation,
L(x, y) =

b
1 X
e(y+1) − ex
.
exp(r) =
W r=a
e + 1

With this notation, we want to show L(a0 , b0 ) ≤ αL(a, b). There
are four cases: a < b ≤ 0, a < 0 < b with |a| ≤ |b|, 0 ≤ a < b,
and a < 0 < b with |a| ≥ |b|. By symmetry of the Laplace
distribution it suffices to consider the first two cases.
For the first case, a < b ≤ 0. By direct calculation:
L(a0 , b0 ) ≤ L(a, b) +

b+η
1 X r
e
W
r=b+1

(b+1+η)

=

e

e

The last line is because (b + 1) ≥ (b − a + 2)/2, and because
1 + η(e − 1) ≤ eη for η ∈ Z for all η,  ≥ 0. To see this last
fact, note that the inequality holds (with equality) at η = 0. We can
directly check that

− ea
+1


 η
1
e − e−(b−a+1)
(b+1)
a
(e
−
e
)
e + 1
1 − e−(b−a+1)
 η

e − e−(b−a+1)
=
L(a, b) ≤ αL(a, b)
1 − e−(b−a+1)
=

For the second case, a < 0 < b with |a| ≤ |b|. By direct
calculation:
 

e −1
L(a0 , b0 ) ≤ L(a, b) + ηL(a, a) = L(a, b) + η
ea
e + 1

 


e −1
ea
≤ 1+η
L(a, b)
e + 1 L(0, b)


η(e − 1)ea
= 1+ 
L(a, b)
e − e−b


1 − e−(b+1) + η(e − 1)e(a−1)
=
L(a, b)
1 − e−(b+1)


1 + η(e − 1)
≤
L(a, b)
1 − e−(b+1)


e2η
≤
≤α
1 − e−(b−a+2)/2

for  ≥ 0, so the inequality is preserved as we increase η.

