Programming Frameworks for Differential Privacy111To appear as a chapter in
[FvH24].
Marco Gaboardi<EMAIL_ADDRESS>Boston University

Michael Hay<EMAIL_ADDRESS>Colgate University

Salil Vadhan<EMAIL_ADDRESS>Harvard University

Many programming frameworks have been introduced to support the development of
differentially private software applications. In this chapter, we survey some
of the conceptual ideas underlying these frameworks in a way that we hope will
be helpful for both practitioners and researchers. For practitioners, the
survey can provide a starting point for understanding what features may be
valuable when selecting a programming framework. For researchers, it can help
organize existing work in a unified way and provide context for understanding
new features in future frameworks.

We do not attempt to be comprehensive in our coverage of the landscape of
software tools for differential privacy (which is constantly growing) or in
the issues relevant to implementation. In particular, we focus on programming
frameworks for expressing and reasoning about differentially private
statistical analyses, sometimes referred to as “queries.” We refer readers
interested in frameworks for large-scale machine learning pipelines to Chapter
LABEL:ch:7 and the references therein. Furthermore, there are a number of
important issues in programming with differential privacy that we did not
address, such as randomness generation, security, finite arithmetic, side
channels, and scalability; discussions of these can be found in many of the
papers we reference.

##  1 Introduction

One of the reasons for the popularity of Differential Privacy [DMNS06, DMNS16]
is that it is based on a simple and elegant mathematical definition which
enjoys several important properties. One of these properties is composability,
which is captured by a number of composition theorems for differential privacy
and its variants, as presented in Chapters LABEL:ch:1 and LABEL:ch:3. In
essence, these composition theorems tell us that the privacy loss of a
“combined” mechanism can be seen as a function of the privacy losses of the
different components. This enables reasoning in terms of a privacy-loss
budget, where a global limit on privacy loss is enforced by tracking the
accumulated privacy losses of differentially private queries made by data
analysts. In addition, it also tells us that different differentially private
mechanisms can be put together to form a “combined” mechanism incurring a
graceful degradation of the privacy loss. This property naturally leads to the
idea of designing programming frameworks for differential privacy. In this
chapter, we use the term “programming framework” in a rather broad and
inclusive way to refer to those tools that have been designed to support the
development of differentially private applications and which provide some
building blocks in the form of basic mechanisms and methods to combine them.

Composability is not the only property that makes the design of programming
frameworks possible. Another important property that differential privacy
enjoys is resilience to postprocessing, guaranteeing that manipulations of the
result of a differentially private mechanism cannot compromise the privacy of
the data. (See Chapter LABEL:ch:1.) In addition, resilience to postprocessing
also guarantees that once the result of a mechanism is computed, we can forget
about the method that was used to compute it. This property provides a sort of
modularity that is akin to the one usually encountered in programming
languages, where one can use library functions based on their specification,
without knowing the details of their implementation. In particular, this
property allows one to use differentially private components inside larger
software projects without worrying about how the results computed by these
components will be used. Composability and resilience to postprocessing also
permit one to solve a data analysis problem by first decomposing it into
subproblems and then combining the results.

There are several reasons why using programming frameworks for designing
differentially private applications is preferable to building differential
privacy applications from scratch:

#### Increasing reliability.

Differential privacy is in its essence a probabilistic requirement on programs
and reasoning about probabilistic guarantees can be challenging and error-
prone, even for experts. (See, for example, [HPN11, Mir12, JMRO22, CSVW22,
HDH+22].) Errors in the design of differential privacy analyses, or bugs in
their implementations, can compromise the privacy property of applications and
undermine their goals. By providing a small set of programming primitives
which can be thoroughly vetted, programming frameworks can help improve
reliability and decrease errors in design and implementations of
differentially private data analyses. In other words, programming frameworks
can reduce the verification of the privacy properties of a program to the
verification of the different components the frameworks provide.

#### Integration with familiar programming workflows.

Programming frameworks for differential privacy provide programming-level
building blocks that can be used to implement differential privacy
applications. These building blocks are usually presented as components of a
library or of a domain-specific language. These libraries and domain-specific
languages can be integrated in standard programming workflow. Hence, data
analysts using these frameworks can combine general-purpose programming and
domain-specific programming.

#### Focusing on functionality and utility.

When designing a differentially private data analysis for a specific
statistical problem one has to ensure that the analysis both respects the
probabilistic requirement of differential privacy and solves the intended
statistical problem. Programming frameworks often provide ways of
automatically ensuring that the differential privacy guarantee is met, without
having to reason directly about the definition of differential privacy. So, by
using these frameworks, a programmer or analyst can focus mainly on
guaranteeing that the analysis solves the statistical problem at hand, which
is the domain expertise of most end-user data scientists (who may not have
expertise in differential privacy).

#### Supporting different computing environments.

Some programming frameworks are designed in a way that decouples the
programming environment from the environment in which programs are actually
executed, often called the computing environment. This separation allows a
user to select a different computing environment based on their own
requirements, which can include efficiency, security, and/or integration with
existing data infrastructure.

#### Improving code reuse and helping build communities.

Another benefit of programming frameworks is that these frameworks can help
the design of standardization processes and open-source initiatives
incentivizing code reuse and better design practices. Programming frameworks
can offer a common language that can be used by different contributors as a
lingua franca. This in turn can help build communities of programmers and
users around differential privacy.

There is by now a plethora of programming frameworks for differential privacy.
A non-exhaustive list includes: APEx [GHIM19], Adaptive Fuzz [WCHRP17],
Airavat [RSK+10], Chorus [JNHS20], DFuzz [GHH+13] Diffprivlib [HBMAL19],
DPella [LVRG20], Duet [NDA+19], Ektelo [ZMK+18], Flex [JNS18], Fuzz [RP10,
HPN11] Google SQL [WZL+20], Gupt [MTS+12], OpenDP [GHV20], PINQ [McS09],
PrivateSQL [KTH+19], and PSI [GHK+16].

Some of these are actively maintained open-source software tools, whereas
others were only built as research prototypes. Moreover, the landscape is
rapidly changing, with new tools emerging at a rapid pace. Thus we do not
attempt to provide a comprehensive description of any specific tools in this
survey. Instead, we identify some of the essential characteristics that cut
across all of the tools, and only use the specific tools as exemplars of
different design choices.

#### Acknowledgements:

Marco Gaboardi’s work was partially supported by NSF through award #
CNS-2040249. Salil Vadhan’s work was supported by a grant from the Sloan
Foundation and a Simons Investigator Award. Marco Gaboardi and Salil Vadhan’s
work was also partially supported by Cooperative Agreement CB20ADR0160001 with
the U.S. Census Bureau. We thank Gary Benedetto, Mark Fleischer, Philip
Leclerc, and Rolando Rodríguez from the Census Bureau for many helpful
comments. The views expressed in this paper are those of the authors and not
those of the U.S. Census Bureau, or any other sponsor.

##  2 Characteristics of DP Programming Frameworks

We organize our survey of differentially private programming frameworks around
the following key characteristics.

#### Privacy Calculus.

A specific aspect of programming frameworks for differential privacy is that
they provide some form of a quantitative calculus that allows one to bound the
privacy loss of analyses written in the framework. These privacy calculi
internalize different general techniques that have been identified in the
differential privacy research literature. For example, several of the
programming frameworks are based on privacy calculi designed around the
concept of global sensitivity [DMNS16], and others around the sample-and-
aggregate framework [NRS07]. In most of the cases, these calculi provide a
form of _privacy specification_ for different components that can be inspected
to guarantee differential privacy for an entire analysis built from those
components.

#### Composition and Interactivity.

In addition to providing a privacy calculus to determine the privacy loss of a
single analysis, programming frameworks for differential privacy often provide
tools for tracking and controlling the cumulative privacy loss over multiple
analyses via composition theorems for differential privacy. These tools range
in their level of generality from supporting single, nonadaptive batches of
queries to interactive systems where a human analyst can adaptively choose the
next query based on the results of previous ones.

#### Expressivity.

One key design aspect of any programming framework is expressivity.
Programming frameworks for differential privacy are no exception. Differential
privacy is often presented as a property of programs working on some data, but
what exactly these programs are, and which statistical tasks they may be able
to accomplish, may vary. For example, some programming frameworks are designed
to support only programs representing a restricted class of queries, while
others attempt to approximate arbitrary data analyses.

###  2.1 Privacy Calculus

Programming frameworks for differential privacy are usually based on some form
of a privacy calculus, which is a principled way to guarantee that a data
analysis is differentially private without explicitly computing the
probability distributions of the data analysis on each pair of neighboring
datasets. Generally, the privacy calculus specifies (a) how do we determine
whether an individual statistical computation is differentially private, and
(b) how does the privacy loss accumulate over multiple statistical
computations. The latter is known as composition and is treated in the next
section, along with interactivity. In this section, we focus on the former,
how we determine that an individual computation is differentially private.

Most of the differential privacy programming frameworks use some form of
reasoning based on sensitivity, or equivalently, stability.222Historically,
the terms sensitivity and stability have been used for related concepts in
different settings in the differential privacy literature. From the paper that
defined differential privacy [DMNS16], sensitivity has referred to functions
mapping datasets to real numbers, vectors, or a general metric space, and
measures how much the value of the function can change when one individual’s
data changes. Starting from PINQ [McS09], stability has referred to functions
mapping datasets to datasets, measuring how much output datasets can differ
per change in output datasets. As discussed below, both are special cases of
more general notions bounding output “distances” as a function of input
“distances” for mappings between arbitrary sets that have some notion of
elements being “close” to each other. We choose “stability” as the terminology
for the more general notion, mainly because it represents a feature we seek:
functions that are most compatible with privacy are ones that remain “stable”
or “in-sensitive” to small changes in their input.

We describe these concepts and some of their different incarnations below.

#### Differential privacy and global stability.

Recall from Chapter LABEL:ch:1 that a mechanism $M$ satisfies (pure)
differentially privacy if for every two datasets $x,x^{\prime}$ that are
adjacent (i.e. differ on one individual’s data), the output distributions
$M(x)$ and $M(x^{\prime})$ are $\varepsilon$-close to each other (in the sense
that for every set $T$ of outputs, the probabilities of $T$ under $M(x)$ and
$M(x^{\prime})$ are within a factor of $e^{\varepsilon}$ of each other). More
generally, by the group privacy property of pure differential privacy, if $x$
and $x^{\prime}$ are at distance at most $d$ (i.e, differ on at most $d$
individuals’ data), then the output distributions are at most
$d\varepsilon$-close to each other. Thus, differential privacy can be viewed
as a stability or Lipschitz property of randomized algorithms $M$, whereby
close inputs map to close output distributions. We think of this as a global
stability property because the stability constant $\varepsilon$ provides a
uniform bound over all pairs of datasets $x$ and $x^{\prime}$.

Thus, it is natural to use notions of global stability as the basis for the
privacy calculus of a DP programming tool. Below we describe some of the
variants of global stability that arise in existing frameworks, in increasing
levels of generality.

Before proceeding, we remark that, even for simple tabular datasets, there are
many ways to formalize the notion of adjacent datasets, and it is important to
be careful and consistent about this choice when implementing differential
privacy. In this chapter, except when explicitly stated otherwise, we model
datasets as unordered multisets of records, and consider two datasets to be
adjacent if we can obtain one from the other by adding or removing one
individual’s data. This formulation is often known as unbounded DP as it
treats the number $n$ of records as being unbounded and potentially private
information. In contrast, bounded DP treats the number $n$ of records as
fixed, public information, and two datasets as adjacent if one can be obtained
from the other by changing one individual’s data.

#### Stable dataset transformations.

The tool PINQ [McS09] supports chaining (pure) differentially private
algorithms $M$ with transformations $T$ from datasets to datasets that are
themselves stable. Specifically, we say that $T$ is $c$-stable if for every
two datasets $x$ and $x^{\prime}$, the distance between the datasets $T(x)$
and $T(x^{\prime})$ is at most a factor of $c$ larger than the distance
between $x$ and $x^{\prime}$. As a simple example, a “map” transformation

$T_{f}(\\{x_{1},\ldots,x_{n}\\})=\\{f(x_{1}),\ldots,f(x_{n})\\}$ (1)

is 1-stable, since record $x_{i}$ of the input affects only one record
$f(x_{i})$ of the output.

Two key properties of stable transformations that make them useful for a
privacy calculus are the following Chaining Rules:

  1. 1.

if $T$ is $c$-stable and $M$ is $\varepsilon$-DP, then $M\circ T$ is
$c\varepsilon$-DP, and

  2. 2.

if $T_{1}$ is $c_{1}$-stable and $T_{2}$ is $c_{2}$-stable, then $T_{1}\circ
T_{2}$ is $c_{1}c_{2}$-stable

For example, using Chaining Rule 1 with $T$ being a map function $T_{f}$ as in
Equation (1) and $M$ being a differentially private noisy sum operator (which,
say, clamps the values to $[0,1]$, adds them up, and adds Laplace noise), we
can estimate sums of arbitrary bounded functions $f$ applied to records.

These two rules are the core of the privacy calculus of PINQ [McS09]. In
addition, PINQ allows for reasoning about the stability of one-to-many
transformations, which map a single dataset to several datasets (e.g.
partitioning, which we will discuss in the next paragraph) and many-to-one
transformations (e.g. database joins).

#### Special cases of stable dataset transformations.

Some frameworks are based on specific families of stable transformations. For
example, Airavat [RSK+10] allows stable transformations of the mapping kind
$T_{f}$ from Equation (1) as well as a $k$-stable generalization where each
input record maps to $k$ output records:

$T_{f_{1},\ldots,f_{k}}(\\{x_{1},\ldots,x_{n}\\})=\\{f_{j}(x_{i}):j=1,\ldots,k,i=1,\ldots,n\\}.$

This allows for efficient implementation in a map-reduce framework. These map
transformations can be composed with a small family of differentially private
reducers, like the noisy sum.

A different generalization of map transformations is used, for example, in the
programming tool GUPT [MTS+12], which allows $f$ to map a set of records (i.e.
a dataset) to a single record. Then we can obtain a 1-stable transformation by
specifying a (possibly random) partition $P=(P_{1},\ldots,P_{m})$ of the set
of possible data records, and outputting

$T_{P,f}(x)=\\{f(x_{P_{1}}),\ldots,f(x_{P_{m}})\\},$

where $x_{P_{i}}$ consists of the records of $x$ in the partition piece
$P_{i}$. This is a 1-stable transformation because each input record $x_{j}$
affects at most one of the output records.333 However, if we worked with
bounded DP, then the transformation would only be 2-stable, because changing
one input record could move that record from one piece of the partition to
another, thereby affecting two of the output records. We can then apply an
arbitrary differentially private aggregator (such as a DP approximation of the
average or median) to the output of $T_{P,f}(x)$ to obtain a differentially
private approximation of the estimator $f$, with the privacy justified by
Chaining Rule 1. This realizes the “sample-and-aggregate” framework introduced
in [NRS07]. The appeal of this framework is that $f$ can be an arbitrary, non-
private statistical analysis, and as long as $f$ gives similar results on the
different subsets of the dataset specified by $P$, then the aggregator should
also give a similar result (with additional noise, to achieve privacy). The
disadvantage is that dataset sizes often need to be quite large for sample-
and-aggregate to be effective, since (a) each set $P_{i}$ in the partition may
need to be large in order for the $f(x_{P_{i}})$’s to well-approximate $f(x)$,
and (b) the number $m$ of sets on the partition may need to be large in order
for the noise introduced by the DP aggregator to be small.

#### Stability on general metric spaces.

Going beyond stable dataset-to-dataset transformations, Fuzz [RP10] can allow
for reasoning about transformations between arbitrary metric spaces.
Specifically, a transformation $T:\mathcal{X}\rightarrow\mathcal{Y}$ from
metric space $(\mathcal{X},d_{\mathcal{X}})$ to metric space
$(\mathcal{Y},d_{\mathcal{Y}})$ is $c$-stable (a.k.a. $c$-Lipschitz) if for
all $x,x^{\prime}\in\mathcal{X}$, we have

$d_{\mathcal{Y}}(T(x),T(x^{\prime}))\leq c\cdot
d_{\mathcal{X}}(x,x^{\prime}).$

For example, if $\mathcal{X}$ is the space of all datasets, $d_{\mathcal{X}}$
is the usual notion of distance on datasets discussed above,
$\mathcal{Y}=\mathbb{R}$, and $d_{\mathcal{Y}}(y,y^{\prime})=|y-y^{\prime}|$,
then a transformation $T$ is $c$-stable if and only if $T$ has global
sensitivity at most $c$ — the basis of the standard Laplace mechanism for
differential privacy [DMNS16].

A benefit of this generalization is that it allows for breaking differentially
private algorithms into smaller components, which in turn provides more
modularity, code reuse, and easier verifiability. Let’s consider the standard
global sensitivity paradigm [DMNS16] for designing differentially private
algorithms. Let $T$ be a function from datasets to real numbers that has
global sensitivity at most $c$, i.e. is $c$-stable as above. Then, as
explained in Chapter LABEL:ch:1, the mechanism

$M(x)=T(x)+\mathrm{Lap}(c/\varepsilon),$

is an $\varepsilon$-differentially private algorithm. With reasoning about
stability between arbitrary metric spaces, we can decompose the construction
and analysis of $M$ into two simpler, modular components. Specifically, note
that $M=N\circ T$, where $T$ is the function of global sensitivity at most
$c$, and $N(z)=z+\mathrm{Lap}(c/\varepsilon)$ adds noise to single real
numbers. The noise-addition mechanism $N$ has the property that two inputs $z$
and $z^{\prime}$ that are close as real numbers (rather than as datasets) map
to close output distributions. Specifically the distance between the
distributions of $N(z)$ and $N(z^{\prime})$ is at most a factor of
$(\varepsilon/c)$ times $|z-z^{\prime}|$. Thus, by an appropriate
generalization of Chaining Rule 1, the composition $N\circ T$ is
$c\cdot(\varepsilon/c)$-DP.

More generally, we call a (randomized) function like $N$ where close inputs
(with respect to any input metric) map to close output distributions (with
respect to any metric on probability distributions) a measurement. In
contrast, if we only allowed for reasoning about stable transformations and DP
algorithms on datasets as above, then $M=T\circ N$ would have to be treated as
an atomic function; now we can separate the components, and reuse the same
noise-addition measurement $N$ for different stable transformations $T$ (and
conversely).

Another benefit of this generalization is extending the privacy calculus to
other input types, such as a database consisting of multiple tables. What
distance metric is appropriate for a database is a nuanced question that
depends on what data is being represented. Consider, for instance, a graph
database consisting of a Node table and an Edge table. The right choice of
metric would depend on whether one wants to protect a single edge, a node and
all of its incident edges, or some other property of the data. Several
programming frameworks support database inputs but vary in the distance
metrics they support. For example, Flex [JNS18] measures distance in terms of
number of rows (across all tables). On the graph database example, whether
Flex offers node or edge-level protection would depend on the query being
asked. PrivateSQL [KTH+19] uses distance metrics that incorporate integrity
constraints that hold on the data. An example of such a constraint is if $u$
is removed from the Node table, then all incident edges must be removed from
the Edge table as well. This allows PrivateSQL, for instance, to capture node-
level protection. GoogleSQL [WZL+20] is designed for databases where each row
is “owned” by a user, each user may own several rows, and distances between
two databases is measured in users rather than individual rows. This captures
the notion of user-level protection that is desirable in applications where
one user might “own” a large number of rows (e.g., a database of credit card
transactions). A limitation of this approach, however, is that it cannot be
easily applied to graph data, because it cannot support scenarios where a data
item can have multiple owners, which is the case for edges in this
example.444For more information on differential privacy for databases, we
recommend Near and He [NH+21].

#### Beyond metric spaces.

The standard mathematical definition of a metric $d(x,x^{\prime})$ is a real-
valued function that satisfies requirements of nonnegativity, symmetry, and
the triangle inequality. However, not all “closeness” notions that appear in
the design of differentially private algorithms are convenient to express in
terms of such metrics. For example, approximate differential privacy measures
the closeness of distributions via two real parameters $\varepsilon$ and
$\delta$, whereas metrics are required to express distance via a single real
number. Thus, the OpenDP Programming Framework [GHV20] allows for expressing
more general stability notions whereby “$d_{\mathrm{in}}$-close” inputs map to
“$d_{\mathrm{out}}$-close” outputs (or output distributions), for arbitrary,
user-defined closeness relations that can be expressed in terms of parameters
$d_{\mathrm{in}}$ and $d_{\mathrm{out}}$ of arbitrary type. In particular,
OpenDP can support a variety of privacy measures, such as approximate DP
[DKM+06], concentrated DP [DR16, BS16], and $f$-DP [DRS22]. Also Duet [NDA+19]
supports several privacy measures but it only supports stability notions over
metric spaces. Duet combines two domain-specific languages: one is similar to
Fuzz and supports only reasoning about transformations between arbitrary
metric spaces, while the other supports instead reasoning about arbitrary
measurements.

#### Local stability.

A difficulty with reasoning about global stability is that it can sometimes be
overly conservative, in that the pair $x,x^{\prime}$ of datasets that maximize
$d(T(x),T(x^{\prime}))/d(x,x^{\prime})$ may be artificial ones that are
unlikely to arise in practice. Thus, it is attractive to try to reason using
local stability, where we take $x$ to be our actual, given dataset, and
consider the quantity

$\mathrm{LS}_{T}(x)=\max_{x^{\prime}:d(x,x^{\prime})=1}d(T(x),T(x^{\prime})).$

Note that this is a data-dependent quantity, in contrast to global stability
that does not depend on the given $x$.

Unfortunately, directly trying to substitute local stability for global
stability in DP algorithms generally does not preserve privacy; the problem is
that the stability itself (which ultimately controls the amount of noise
introduced) can reveal sensitive information. Thus, there is a large body of
work on how to approximate this idea (using variants of local stability) while
obtaining algorithms that are genuinely differentially private. Flex [JNS18]
is a tool whose design draws on this body of work to tackle the problem of
privately answering database queries that involve joins. Whereas a join query
can have large, possibly unbounded, _global_ stability, its _local_ stability
can be much smaller. For instance, local sensitivity of a join between a Node
and Edge tables would be a function of the maximum node degree as opposed to
the number of nodes. Flex leverages this property in its approach, called
_elastic sensitivity_ , which is a calculus for deriving an upper bound on the
local stability of a complex database query expression. Flex combines its
elastic sensitivity with techniques from prior work on appropriately
calibrating noise to bounds on local stability.

###  2.2 Composition and Interactivity

In differential privacy, _composition_ refers to reasoning about the privacy
properties of an algorithm that is composed of one or more differentially
private algorithms. The basic composition theorem for (pure) differential
privacy says that if mechanisms $M_{1}$ and $M_{2}$ are $\epsilon_{1}$-DP and
$\epsilon_{2}$-DP respectively, then the mechanism $M(x)=(M_{1}(x),M_{2}(x))$
that applies both mechanisms to the same dataset and outputs both results is
$(\epsilon_{1}+\epsilon_{2})$-DP. Composition has two key applications in the
context of programming frameworks. First, it allows for tracking the
_cumulative_ privacy loss that results from executing multiple statistical
computations. Some programming frameworks help users manage the cumulative
privacy loss by allowing them to impose a privacy loss “budget” and ensuring
that the cumulative loss does not exceed the budget. Second, it is a useful
tool in algorithm design as it facilitates the creation of new differentially
private algorithms from existing components. Some programming frameworks
facilitate the creation of new mechanisms in this way. Both of these
applications of composition are enhanced by frameworks that support
_interactivity_ , where human analysts or programs can adaptively choose which
mechanism $M_{2}$ to apply after receiving the result of a previous mechanism
$M_{1}$.

While the composition rules for pure DP are fairly straightforward (epsilons
add up), the composition rules for other variants of DP are less so, and this
has been and continues to be an active area of research [KOV15, MV16, RRUV16,
ACG+16, DR16, BS16, Mir17, DRS22, VW21, VZ22, Lyu22, WRRW22]. (See Chapter
LABEL:ch:3 for more on composition.) We organize the rest of this section
around the kinds of composition that are supported by programming frameworks
for differential privacy.

#### No composition.

Some programming frameworks, such as Flex [JNS18] and Diffprivlib [HBMAL19],
do not support composition or interactivity. That is, they enable one to
control or calculate the privacy loss of an individual differentially private
mechanism or query, but tracking the cumulative privacy loss is left to the
user or an application built on top of the framework.

#### Non-adaptive composition.

Several programming frameworks allow the user to construct a program that
evaluates a _batch_ of statistical computations $M_{1},\dots,M_{\ell}$. The
computations are _nonadaptive_ , meaning that the sequence of computations is
fixed: each $M_{i}$ has fixed privacy loss parameters and its only input is
the private dataset. An archetypal example is the released prototype of PSI
[GHK+16] and its successor DP Creator [DPC22], which allows a data curator to
choose a set of summary statistics (e.g., means, quantiles, histograms) to be
released under a fixed privacy loss budget. Other frameworks that fall into
this category include Airavat [RSK+10], PrivateSQL [KTH+19].

Such frameworks are responsible for calculating the cumulative privacy loss of
the program and typically ensuring it does not exceed a user-specified budget.
Some employ the basic, pure DP sequential composition theorem alluded to in
the introduction to this section, but PSI uses (an approximation of) the
optimal composition theorem for approximate DP [MV16]. However, these
frameworks do not explicitly track the cumulative privacy loss across batches
or support interaction with the user.555The paper describing the design of PSI
[GHK+16] proposes a way to support interactivity with multiple batches, but
the prototype implementation does not offer that functionality.

#### Adaptive composition.

Adaptive composition refers to the idea that subsequent mechanisms may depend
on the results of evaluating earlier mechanisms ($M_{2}$ can depend on
$M_{1}(x)$). In the most basic form of adaptive composition, one again has a
fixed sequence of $\ell$ statistical computations, $M_{1},\dots,M_{\ell}$
where the privacy loss of each $M_{i}$ is fixed, but each subsequent
computation can depend on the results of previous computations—i.e., mechanism
$M_{i}$ is provided the results of earlier computations as auxiliary input.
Formally, we compute the $i$’th result as
$y_{i}=M_{i}(x;(y_{1},y_{2},\ldots,y_{i-1}))$, where $x$ is the private
dataset. With this kind of adaptivity, one can support iterative algorithms
such as $k$-means clustering, an algorithm for grouping data into $k$
clusters. Such an algorithm is inherently adaptive because it proceeds in
rounds where the assignment to clusters in each round depends on a statistical
summary produced in the previous round.

An example of a programming tool that supports this kind of composition is
Fuzz. Fuzz uses a type system to statically analyze (at “compile time”) the
composition of a program. While Fuzz does support adaptive composition, it is
limited to programs where the stability (or sensitivity, see Section 2.1) is a
constant and therefore precludes supporting, say, a version of $k$-means where
the number $k$ of clusters or the number $\ell$ of iterations are user-
specified inputs to the program. DFuzz [GHH+13] overcomes this limitation by
extending the static type system approach to allow types to depend on input
variables. Other more complex type system have been studied, in order to go
even farther in supporting the verification of differential privacy data
analyses. We will discuss some of them briefly in Section 3.2.

#### Fully adaptive composition and interactivity.

With the previously described programming frameworks, the entire statistical
computation, even if adaptive, must be specified up front. While such
frameworks can be useful for building complex algorithms, in many practical
applications, however, it may be undesirable to bundle all computations into a
single “one shot” algorithm. Instead, analysts may prefer to interactively
query the data, receive (differentially private) responses, and adaptively
choose the next query. In such a setting, the composition can be said to be
fully adaptive because the number of rounds, the choice of mechanism, and its
privacy parameters are all adaptively chosen by the analyst. Composition is
more subtle in this setting [RRUV16].

The interactive setting can be modeled as an interactive protocol between two
parties, an arbitrary adversarial strategy $\mathcal{A}$ (the analyst) and an
interactive measurement $\mathcal{M}(x)$. The interaction proceeds in rounds
where in round $i$, $\mathcal{A}$ selects a query $q_{i}$ adaptively based on
all previous answers $(a_{1},\dots,a_{i-1})$ and any randomness of
$\mathcal{A}$. One can think of a query as a request to perform a
differentially private computation with given privacy loss parameters. The
query is sent to the interactive mechanism $\mathcal{M}$ which evaluates the
query and returns answer $a_{i}$. Differential privacy is defined with respect
the adversary’s _view_ , denoted
$\mathrm{View}(\mathcal{A}\leftrightarrow\mathcal{M}(x))$, of this interaction
[VW21].

We highlight two programming frameworks in this setting. Both support a form
of interaction known as a _privacy filter_ [RRUV16], an interactive mechanism
that takes a global privacy loss budget and admits adaptively selected
computations provided that evaluating the computation would not cause the
cumulative privacy loss to exceed a pre-specified budget. A variant is the
concept of a _privacy odometer_ [RRUV16], which tracks cumulative privacy loss
but does not enforce a pre-determined budget.

In the programming tool PINQ, the interactive mechanism is represented by a
_PINQueryable_ , a stateful object that encapsulates a private data source (a
collection of records) and allows it to be queried within a given privacy-loss
budget. Each _PINQueryable_ exposes a set of pre-defined methods, which
represent the available queries. An example method is $\mathrm{NoisyAverage}$,
which takes an $\epsilon$ and a function $f$ and applies $f$ to each tuple in
the source, clamps the result to $[-1,1]$, and returns a noisy average of the
clamped results. The analyst $\mathcal{A}$ can be expressed as arbitrary code,
written in the language C#; in particular, $\mathcal{A}$ can make fully
adaptive queries to the _PINQueryable_ , and the _PINQueryable_ tracks the
cumulative privacy loss and enforces the budget.

The programming tool Adaptive Fuzz [WCHRP17] is built on top of Fuzz: it adds
an outer “adaptive” layer that wraps around the static typechecker and runtime
of Fuzz. Unlike PINQ, the available queries are not limited to a pre-defined
set of methods, but rather a query can be any computation that the Fuzz
typechecker can verify to be differentially private. An example of an
application that Adaptive Fuzz can support is fitting a model using
differentially private gradient descent with a data-dependent stopping
criteria, such as the model error falling below a threshold. If the stopping
criteria is reached before the budget is exhausted, any remaining budget can
be applied to additional (adaptively chosen) computations.

#### Hierarchical (and concurrent) interactivity.

While there are several frameworks that support interactivity, most operate
like Adaptive Fuzz with a single “level” of interactivity: there is exactly
one interactive mechanism that governs the adaptivity and any query to that
mechanism must correspond to a _non-interactive_ differentially private
program. _Hierarchical interactivity_ refers to the idea that an interactive
mechanism could recursively spawn new interactive mechanisms.

Hierarchical interaction has many potential applications. It could be useful
as a way of structuring programs that naturally have multiple layers of
interactivity – for instance, the first layer of interactivity might be a
privacy filter and the second layer of interactivity might include the
execution of interactive primitives like Sparse Vector or Private
Multiplicative Weights [DR14]. Another application could be to allow a data
curator to allow _multiple_ analysts to operate concurrently on the data, each
with their own privacy filter or odometer, such that the cumulative privacy
loss is tracked appropriately. One could also imagine novel algorithms that
involve asking interleaving queries to two or more instantiations of
interactive mechanisms.

PINQ supports (a limited form of) hierarchical interactivity. Some of the
methods available on a _PINQueryable_ are capable of spawning new
_PINQueryable_ objects. For instance, the $\mathrm{Partition}$ method splits
the dataset into multiple, disjoint datasets and returns a new _PINQueryable_
for each one. Using such methods it is possible to start with an initial
private data source and spawn a tree of related queryables.666In fact, rather
than a tree, the result structure can be a directed acyclic graph because PINQ
also supports operators like $\mathrm{Join}$ that combines two queryables into
one. Such a tree is illustrated in Fig. 1.

Figure 1:  Illustration of hierarchical interactivity in PINQ. When a query
(yellow circle) is submitted to _PINQueryable_ $C_{1}$, its agent (A) forwards
the budget request (yellow bar) to the agent of its parent, $Q$. In this case,
because the children represent disjoint partitions of $Q$’s data, the agent of
$Q$ keeps track of the cumulative privacy loss incurred at each child (red
bars). When it receives the request from the child, it calculates how much
this query would increase the maximum privacy loss and sends a request to the
agent of its parent, $P$, who checks the residual cost against a budget. Since
the request is under budget, response data (D) flows back to the
_PINQueryable_ where the query initiated.

Fig. 1 also illustrates PINQ’s method for reasoning about the the composition
of these multiple, related queryables. Each queryable internally has an agent
which is responsible for managing requests to consume privacy budget through
one of the measurement methods (like NoisyAverage). The agent associated with
each new queryable has a reference to its parent queryable. The child is
responsible for handling its request and translating it into an appropriate
request to its parent. For instance suppose $Q$ is a queryable with parent $P$
and children $C_{1},\dots,C_{k}$ that are the result of calling
$\mathrm{Partition}$ on $Q$. Because partition splits the data into disjoint
subsets, interactions with the children satisfy _parallel composition_ [McS09]
and the cumulative privacy loss is the maximum of the loss incurred by any of
the children.777This is similar to the stability analysis underlying the
sample-and-aggregate framework and GUPT discussed above in Section 2.1.
Therefore, when the agent of $Q$ receives a request from its children, the
amount of the request to its parent is only the _change_ in the maximum (which
might be zero).

Somewhat surprisingly, the more general concurrent composition of multiple
mechanisms has only recently been formally studied [VW21] and researchers have
only recently presented proofs that other variants of DP such as $f$-DP
[DRS22] and Renyi-DP [Mir17, BS16] satisfy concurrent composition theorems
[VZ22, Lyu22, HST+23].

#### Extensibility.

With both PINQ and AdaptiveFuzz, the composition is “baked in” to the
programming framework itself. For example, the implementation of PINQ supports
a specific definition of privacy (pure DP); its components exchange
information using the parameters of that definition ($\epsilon$) and the
agents apply the composition rules of PureDP. Perhaps more fundamentally, it
leans heavily on the fact that with group privacy under pure DP, the privacy
loss grows linearly with the size of the group, which allows it to view an
$\varepsilon$-DP measurement on a $c$-stable transformation of the dataset as
equivalent to a $c\varepsilon$-DP measurement on the source. (See Section
2.1.) Adapting PINQ to support a variant of DP like zCDP that has a non-linear
relationship between group size and privacy loss seems non-trivial, especially
if one wants to provide tight privacy accounting.

An explicit design goal of OpenDP is extensibility and its approach to
handling composition makes it easy, in principle, to expand the library with
new forms of composition. In the OpenDP formulation of a measurement (as
discussed in Section 2.1), the privacy properties are explicitly encoded in a
privacy map that transforms distances between input data(sets) to distances
between output probability distributions, and the latter can be measured in
any desired way.

To extend OpenDP with a new form of composition, one must simply define a new
measurement operator that captures that composition operation. For example,
basic non-adaptive composition is implemented as a measurement function that
takes as input a list of measurement functions and applies them sequentially
to the data. It can use the privacy maps of the measurements being combined
plus the sequential composition theorem to determine its own privacy map.

###  2.3 Expressivity

Expressivity refers to the richness and variety of analyses that can be
expressed in a given programming framework. These are naturally impacted by a
framework’s privacy calculus and support for composition. In particular, given
that most analyses are expressed as a chaining of measurements and stable
transformations, e.g. $M\circ T_{k}\circ T_{k-1}\circ\cdots T_{1}$, or
compositions of such chainings, the expressivity of a programming framework is
greatly impacted by which transformations, measurements, and composition
procedures are supported. Thus, another relevant feature is extensibility, the
support for adding new, user-defined building-block components such as
transformations, measurements, and composition procedures, as just discussed.
Following the same approach we used in previous sections we will not aim to
have a general ranking between the frameworks in terms of expressivity, rather
we will highlight some points with respect to expressivity in the design space
of programming frameworks for differential privacy.

#### Allowing general-purpose programming together with DP.

Several programming frameworks for differential privacy have been designed as
libraries or domain-specific languages embedded inside general-purpose
programming languages. This allows one to use the richness of the host
language to enhance the expressivity of the programming framework. One of the
earliest such examples is PINQ [McS09], which is designed as a domain-specific
language integrated in the general-purpose language C#. Specifically, PINQ has
been implemented as a C# component built on top of the data-processing
component LINQ. PINQ provides several basic transformations, mostly inspired
by SQL such as filters, joins, groupby, map, etc and several basic
measurements representing aggregation operations, such as count, sum, average,
etc. In fact, most of the PINQ transformations and measurements consists of a
thin layer of code encapsulating the corresponding LINQ transformations. This
encapsulation mechanism is needed to guarantee differential privacy through a
privacy calculus based on global sensitivity of the sort we discussed in
Section 2.1.

Thanks to the integration with a general purpose programming language, PINQ
supports general purpose programming that can be used to describe more complex
data types, and to implement new transformation and mechanisms. Indeed, PINQ’s
set of data types, transformations and measurements can be easily extended, in
principle, by providing new implementations that match the same interface that
primitive components have to match, and that respect the principles of the
privacy calculus that PINQ implements. In fact this is a recipe for
extensibility that several other programming frameworks for differential
privacy have followed: new transformation and measurement primitives can be
easily added to a programming framework by taking operations that are
implemented in the underlying language and encapsulating them in order to
guarantee their stability and sensitivity properties for their sound use in
the corresponding privacy calculus.

As we discussed in Section 2.2, private data sources in PINQ are encapsulated
in a _PINQueryable_ object and can be accessed through chains of
transformations followed by an aggregation. This chaining is one of the main
principles for the interactions of _PINQueryable_ objects with transformations
and measurements. The encapsulation of data using queryables allows, in
principle, extensions of PINQ that implement different forms of composition
with different degrees of adaptivity and hierarchical and concurrent
interactivity. Both chaining and composition are implemented in PINQ as C#
routines that offer at the same time an interface for users and a component of
the privacy calculus. Similarly to transformations and measurements, one could
extend this family of chaining and composition components by providing new
implementations in the underlying general-purpose language. However, while
possible in principle, as discussed in the PINQ design document [McS09], these
extensions are less straightforward than extensions of transformations and
measurements, since they require redefining _PINQueryable_ and its methods.
More recent programming frameworks such as OpenDP, take a more explicit view
on chaining and composition components: they are first class citizens, called
combinators, with an explicit interface that can be used to interact with
them, and explicit requirements for their privacy calculus properties. Thus,
to add a new form of composition to OpenDP simply requires adding a new
combinator capturing it.

In some situations, programming frameworks for differential privacy also allow
user to write and run arbitrary programs. Often these programs are required to
be pure or “purified,” i.e. without side effects that can potentially
compromise privacy. Programming frameworks that work in synergy with a
general-purpose programming language can use the resources of the host
language in these situations. For example, as discussed in the PINQ design
document [McS09], one can write C# programs using a set of methods which are
side-effect free and which can be used in mapping operations in a data
processing. The distinction between methods that can have potential side
effects and those that are side-effect-free is built into PINQ. Other
approaches, such as the one implemented in DPella [LVRG20], make this kind of
distinction using types.

There is one additional benefit of using a general-purpose language that is
worth discussing. General-purpose programming languages usually provide
methods to access a variety of different kinds of data sources, e.g.
relational databases, tabular data in various forms, streaming sources, etc.
This allow programming frameworks for differential privacy to easily also
support different kinds of data sources, and to process data independently
from the way it is stored.

#### Support for a specific class of queries.

Most of the programming frameworks, instead of aiming to support the
implementation of arbitrary differentially private data analyses, focus on a
specific class of functions that are useful to implement a large class of
analyses. For example, PINQ [McS09], PrivateSQL [KTH+19], Flex [JNS18], and
others all aim at supporting SQL-like queries.

A different example is Ektelo [ZMK+18]. Essentially, Ektelo is very similar to
PINQ in many respects: it also provides transformations and measurement
similar to the ones provided by PINQ, and a privacy calculus for them.
However, instead of focusing on the components that are needed for SQL-like
queries, it includes a large variety of basic transformations and measurements
that allow one to construct numerous important differentially private
algorithms for estimating workloads of linear queries. Linear queries are
queries of a simplified form: they compute the average, or the sum, of the
results obtained by mapping a given function (characterizing the specific
linear query) on each record of a dataset. Despite their simplicity, when
combined together in a workload, i.e. multiple queries together, linear
queries allow one to solve many important statistical problems, such as
histograms, CDFs, and contingency tables.

Ektelo’s basic components include transformations and measurements, but also
operations of three other families: 1) Operations that allow one to partition
the data and to work on the individual partitions. For example, Ektelo
provides a data-dependent operation AHPpartition which, given the data as an
histogram, selects a partition of the data where the counts within a partition
group are close. 2) Operations that allow one to manage the workload of
queries by selecting queries that have different properties. For example,
Ektelo supports an operation Worst-approx which returns a query, from a
workload of queries, which has the property that on a synthetic dataset (or
synthetic data distribution) deviates most from the true dataset. 3)
Operations that perform some sort of inference as post-processing of the
private answers. For example, Ektelo provides an operation MW which implements
the Multiplicative Weight inference algorithm. All these operations can be
combined to design more complex data analyses. For example, one can use basic
transformations and measurements and operations of types 2) and 3) to
implement the private data release algorithm MWEM [HLM12].

Despite the fact that its design focuses on the restricted class of linear
queries, Ektelo is able to express in a concise way numerous differentially
private algorithm that have been proposed for a variety of tasks. Moreover,
thanks to its additional operations, Ektelo is also able to go beyond tasks
that are usually considered as proper linear queries. For example, one can use
Ektelo to privately select the structure of a Bayesian network.

Another programming framework using an approach similar to the one of Ektelo
is Chorus [JNHS20]. Instead of focusing on linear queries, Chorus focuses on
SQL queries and it provides several components to rewrite, analyze and post-
process queries. These components allow Chorus to express in a concise way
numerous complex differentially private algorithm such as MWEM, Sparse Vector,
etc.

#### Support for a specific class of DP algorithms.

As we discussed in Section 2.1, there are several privacy calculi that one
could use to guarantee differential privacy. Programming frameworks usually
support one such privacy calculus, and the privacy calculus that a programming
framework uses also affects its expressivity.

Programming frameworks that have been designed around the notion of global
stability, such as PINQ and many others, allow one to implement a broad range
of general differentially private data analyses. In contrast, programming
frameworks that support other models, such as GUPT [MTS+12] for the sample and
aggregate framework, or Flex [JNS18] for the local stability framework, are
more limited in the class of data analyses that they can support.

The limitations of GUPT, and the sample and aggregate framework more
generally, come from the fact that this framework only captures differentially
private data analyses that can be implemented as a transformation that can be
run independently on the pieces of a partition of the dataset, followed by one
of a few pre-specified differentially private aggregators combining the
obtained results. Most differentially private algorithms cannot be decomposed
in this way.

The limitations of Flex and other local stability frameworks is that these
frameworks are usually based on some approximation of the local stability that
cannot in general be computed efficiently for every problem. This means that
the programming framework using these approximation needs to be specialized to
specific tasks. For example, Flex’s elastic sensitivity calculus is based on a
careful case analysis of operators that appear in SQL expressions. It is not
obvious how to extend this definition to arbitrary data analyses, and it is
unclear whether such an extension would be tractable.

While these frameworks have limitations in terms of expressivity, they also
have some benefit. For example, as we already mentioned in Section 2.1, the
sample-and-aggregate framework allows one to take arbitrary non-private
estimators that converge as the sample size grows and automatically construct
differentially private analogues of them, albeit on larger datasets.
Similarly, methods based on local stability can provide improved accuracy in
certain situations.

#### Support for reasoning about accuracy.

Most of the programming frameworks we discussed so far focus on providing
support to users in order to write their differentially private data analyses
and guarantee they are indeed private. However, another important aspect that
users need to think about when designing differentially private analyses is
_accuracy_. While there isn’t one notion of accuracy which works in every
situation, a notion of accuracy which is often considered in the differential
privacy literature is based on probability bounds. As an example,
$(\alpha,\beta)$-accuracy expresses the following probability bound: if
$\tilde{y}$ is the result of a differentially private analysis and $y$ is the
result one would achieve if one did the analysis without privacy constraints,
then $(\alpha,\beta)$-accuracy says that with probability at least $1-\beta$,
$\|y-\tilde{y}\|\leq\alpha$ where $\|\cdot\|$ is a suitable norm. For simple
differentially private mechanisms, the $\alpha$ and $\beta$ follow from the
properties of the noise distributions they use.

Several programming frameworks have been conceived to also help users reason
about the accuracy of their differentially private data analyses. One such
example is GUPT [MTS+12], which provides its users with the possibility to
select either the privacy budget or the $(\alpha,\beta)$-accuracy they want
for each data analysis. If users specify the accuracy level they are
interested in, GUPT computes the corresponding privacy budget that is needed,
and vice versa: if users specify the privacy budget they are interested in,
GUPT computes the corresponding $(\alpha,\beta)$-accuracy. A similar approach
is also used by PSI [GHK+16], where users are provided with a budgeter
interface that they can use to specify interactively either the privacy budget
or the accuracy for the different queries. The usability of this budgeter
interface has also been evaluated with users [MTKV18, SSH+22]. The approach
used by GUPT and PSI is based on the accuracy bounds of the primitive noise
distributions they use. APEx [GHIM19] takes a further step and uses several
specific analyses and linear programming to provide accuracy estimates for
more complex algorithms, including some algorithms that have accuracy which
depends on the data.

A different approach is proposed by DPella [LVRG20], a programming framework
which combines reasoning about privacy in the style of PINQ,888Differently
from what happen in PINQ, the privacy reasoning in DPella happens at compile
time. with reasoning about $(\alpha,\beta)$-accuracy. A user of DPella can
write differentially private programs and obtain information about their
privacy or accuracy. An interesting aspect of the DPella approach is that it
allows to compose the accuracy of different mechanisms using the Union bound
and Chernoff bounds in order to provide accuracy properties for larger
programs.

##  3 Tools for Verification and Testing

As we discussed above, an important motivation for the design of domain
specific programming frameworks for differential privacy comes from the
difficulties that randomness, finite precision arithmetic, budget accounting,
etc. impose on data analysis design. Programming frameworks can help improve
the correctness and reliability of differentially private programs. However,
as we discussed in Section 2, most of the programming frameworks allow one to
assemble basic primitives as building blocks that are considered trusted. This
situation is less than ideal, since bugs in these primitives can affect the
correctness of the overall data analyses. In order to help alleviate this
problem, researchers have developed several verification and testing tools
specifically designed to improve the correctness and reliability of
differentially private primitives. In this section, we briefly review some of
them, focusing on the techniques that they are based on. All these methods
have to cope with the fact that black-box testing for differential privacy, as
well as automated verification of differential privacy, are inherently
difficult in the worst case [GM18, GNP20, BGG22].

###  3.1 Tools for testing differential privacy implementations

Testing is a powerful tool to improve the reliability and correctness of
software. Following this intuition, several testing methods have been studied
and implemented in order to increase confidence in claims of differential
privacy for data analysis implementations. Early work on testing for
differential privacy [JR11, DJRT13] reduced this problem to testing Lipchitz
properties of data analyses, while subsequent work designed methods specific
for differential privacy. StatDP [DWW+18] provides a testing framework based
on hypothesis testing and counterexample generation to find violations in data
analyses that claim to be differentially private. This testing framework
considers programs as black box but also provides the option to use program
analysis methods to estimate parameter values that can create violations.
Following similar ideas, GoogleSQL [WZL+20] includes a stochastic tester in
order to check whether some basic mechanism is differentially private. This
tester is useful to analyze mechanisms of a restricted class, corresponding to
aggregation functions, rather than end-to-end applications. DP-Finder [BGD+18]
uses testing and numerical optimization techniques to prove lower bounds on
the privacy parameters of specific programs. This method can be also used to
find violations to differential privacy in implementations. CheckDP [WDKZ20]
combines statistical testing with symbolic solving in order to guarantee data
analyses are differentially private; when the differential privacy guarantee
is violated, this approach provides counterexamples. DPCheck [ZRH+20] uses a
combination of randomized testing and symbolic execution to identify
violations of differential privacy in an automated way. DP-Sniper [BSBV21]
uses learning techniques to train a classifier to distinguish whether the
result of a mechanism comes from a dataset or an adjacent one, and when
possible to transform this classifier into a counterexample exhibiting a
violation of differential privacy. DP-Sniper is also able to identify
violations due to floating-point arithmetic.

###  3.2 Tools for the verification of differential privacy

Randomized testing as discussed above can help improve the reliability of
differential privacy components. However, when the input space of these
components is large, it is difficult for randomized testers to offer strong
guarantees in terms of coverage, and the uncovered input space can still hide
bugs in the design and implementations of these components. For this reason,
several groups of researchers have also developed formal verification
techniques which can be used to mathematically prove the design and
implementations of these components to be correct. An advantage of these
approaches is that the verification can happen before the program is run,
limiting the risks for the actual data.

A first approach in this line of work is based on the use of _program logics_
and _interactive proof assistants_. These are formal tools that have been
developed in order to formally verify properties of programs and their
implementation. The idea behind these tools is that a user needs to provide a
program, a specification that the program needs to satisfy, and a formal
proof, in the form of a computer script, that the program meets the
specification. The tool then checks that the formal proof is correct and that
indeed the program respects the specification. In the case of differential
privacy, the specification is that the program is differentially private.
Several works have followed this approach [BKOB12, BDG+13, BGA+14, BGG+16,
BFG+16, AH18] building on different program logics and proof assistants.

Another approach in this line of work is based on the use of advanced _type
systems_ , _symbolic execution_ and _constraint solvers_. In this approach, a
user needs to provide a program and its specification. The specification is
usually in the form of a type specification in some rich language of types
that also provides the guarantee that a program is differentially private.
However, the user does not need to provide a formal proof connecting the
program with its specification. Instead, this formal proof is synthesized by a
type checker combined with constraint solving. In Section 2.1, we already
discussed Fuzz [RP10], which was one of the first tools in this area. Fuzz is
limited in expressivity: it can only type programs whose sensitivity is a
constant. Several works have extended this approach [GHH+13, BGA+15, ZK17,
WDW+19, WDKZ20, FCG21] and designed more and more expressive tools. The high
level of confidence and formal guarantees that these tools provide goes beyond
what can be usually achieved by code inspection and randomized testing. On the
other hand, those tools are often difficult to use and often require expertise
in formal verification or programming-language design, as well as differential
privacy.

## References

  * [ACG+16] Martin Abadi, Andy Chu, Ian Goodfellow, H Brendan McMahan, Ilya Mironov, Kunal Talwar, and Li Zhang.  Deep learning with differential privacy.  In Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, pages 308–318, 2016.
  * [AH18] Aws Albarghouthi and Justin Hsu.  Synthesizing coupling proofs of differential privacy.  Proc. ACM Program. Lang., 2(POPL):58:1–58:30, 2018.
  * [BDG+13] Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, and Santiago Zanella Béguelin.  Verified computational differential privacy with applications to smart metering.  In 2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, LA, USA, June 26-28, 2013, pages 287–301. IEEE Computer Society, 2013\.
  * [BFG+16] Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.  Advanced probabilistic couplings for differential privacy.  In Edgar R. Weippl, Stefan Katzenbeisser, Christopher Kruegel, Andrew C. Myers, and Shai Halevi, editors, Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, pages 55–67. ACM, 2016.
  * [BGA+14] Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub.  Proving differential privacy in hoare logic.  In IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014, pages 411–424. IEEE Computer Society, 2014.
  * [BGA+15] Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub.  Higher-order approximate relational refinement types for mechanism design and differential privacy.  In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 55–68. ACM, 2015.
  * [BGD+18] Benjamin Bichsel, Timon Gehr, Dana Drachsler-Cohen, Petar Tsankov, and Martin T. Vechev.  Dp-finder: Finding differential privacy violations by sampling and optimization.  In David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang, editors, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, pages 508–524. ACM, 2018.
  * [BGG+16] Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.  Proving differential privacy via probabilistic couplings.  In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 749–758. ACM, 2016.
  * [BGG22] M. Bun, M. Gaboardi, and L. Glinskih.  The complexity of verifying boolean programs as differentially private.  In 2022 2022 IEEE 35th Computer Security Foundations Symposium (CSF) (CSF), pages 380–395, Los Alamitos, CA, USA, aug 2022. IEEE Computer Society.
  * [BKOB12] Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin.  Probabilistic relational reasoning for differential privacy.  In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 97–110. ACM, 2012.
  * [BS16] Mark Bun and Thomas Steinke.  Concentrated differential privacy: Simplifications, extensions, and lower bounds.  In Martin Hirt and Adam D. Smith, editors, Theory of Cryptography - 14th International Conference, TCC 2016-B, Beijing, China, October 31 - November 3, 2016, Proceedings, Part I, volume 9985 of Lecture Notes in Computer Science, pages 635–658, 2016.
  * [BSBV21] Benjamin Bichsel, Samuel Steffen, Ilija Bogunovic, and Martin T. Vechev.  Dp-sniper: Black-box discovery of differential privacy violations using classifiers.  In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021, pages 391–409. IEEE, 2021.
  * [CSVW22] Sílvia Casacuberta, Michael Shoemate, Salil Vadhan, and Connor Wagaman.  Widespread underestimation of sensitivity in differentially private libraries and how to fix it.  In Proceedings of the 29th ACM SIGSAC Conference on Computer and Communications Security (CCS ‘22), 7–11 November 2022.  To appear. Preprint posted as arXiv:2207.10635 [cs.CR].
  * [DJRT13] Kashyap Dixit, Madhav Jha, Sofya Raskhodnikova, and Abhradeep Thakurta.  Testing the lipschitz property over product distributions with applications to data privacy.  In Amit Sahai, editor, Theory of Cryptography - 10th Theory of Cryptography Conference, TCC 2013, Tokyo, Japan, March 3-6, 2013. Proceedings, volume 7785 of Lecture Notes in Computer Science, pages 418–436. Springer, 2013.
  * [DKM+06] Cynthia Dwork, Krishnaram Kenthapadi, Frank McSherry, Ilya Mironov, and Moni Naor.  Our data, ourselves: privacy via distributed noise generation.  In Advances in cryptology—EUROCRYPT 2006, volume 4004 of Lecture Notes in Comput. Sci., pages 486–503. Springer, Berlin, 2006.
  * [DMNS06] Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith.  Calibrating noise to sensitivity in private data analysis.  In Theory of cryptography conference, pages 265–284. Springer, 2006\.
  * [DMNS16] Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam D. Smith.  Calibrating noise to sensitivity in private data analysis.  J. Priv. Confidentiality, 7(3):17–51, 2016.
  * [DPC22] DP creator.  https://github.com/opendp/dpcreator, March 2022.
  * [DR14] Cynthia Dwork and Aaron Roth.  The algorithmic foundations of differential privacy.  Foundations and Trends® in Theoretical Computer Science, 9(3–4):211–407, 2014.
  * [DR16] Cynthia Dwork and Guy N. Rothblum.  Concentrated differential privacy.  CoRR, abs/1603.01887, 2016.
  * [DRS22] Jinshuo Dong, Aaron Roth, and Weijie J. Su.  Gaussian differential privacy.  Journal of the Royal Statistical Society: Series B (Statistical Methodology), 84(1):3–37, 2022.
  * [DWW+18] Zeyu Ding, Yuxin Wang, Guanhong Wang, Danfeng Zhang, and Daniel Kifer.  Detecting violations of differential privacy.  In David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang, editors, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, pages 475–489. ACM, 2018.
  * [FCG21] Gian Pietro Farina, Stephen Chong, and Marco Gaboardi.  Coupled relational symbolic execution for differential privacy.  In Nobuko Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 207–233. Springer, 2021\.
  * [FvH24] Ferdinando Fioretto and Pascal van Hentenryck, editors.  Differential Privacy in Artificial Intelligence: From Theory to Practice.  now publishers, 2024.  To appear.
  * [GHH+13] Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C Pierce.  Linear dependent types for differential privacy.  In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 357–370, 2013.
  * [GHIM19] Chang Ge, Xi He, Ihab F Ilyas, and Ashwin Machanavajjhala.  Apex: Accuracy-aware differentially private data exploration.  In Proceedings of the 2019 International Conference on Management of Data, pages 177–194, 2019.
  * [GHK+16] Marco Gaboardi, James Honaker, Gary King, Jack Murtagh, Kobbi Nissim, Jonathan Ullman, and Salil Vadhan.  Psi ($\\{$$\backslash$Psi$\\}$): a private data sharing interface.  arXiv preprint arXiv:1609.04340, 2016.
  * [GHV20] Marco Gaboardi, Michael Hay, and Salil Vadhan.  A programming framework for opendp.  Manuscript, May, 2020.
  * [GM18] Anna C Gilbert and Audra McMillan.  Property testing for differential privacy.  In 2018 56th Annual Allerton Conference on Communication, Control, and Computing (Allerton), pages 249–258. IEEE, 2018.
  * [GNP20] Marco Gaboardi, Kobbi Nissim, and David Purser.  The complexity of verifying loop-free programs as differentially private.  In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 129:1–129:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [HBMAL19] Naoise Holohan, Stefano Braghin, Pól Mac Aonghusa, and Killian Levacher.  Diffprivlib: the ibm differential privacy library.  arXiv preprint arXiv:1907.02444, 2019.
  * [HDH+22] Samuel Haney, Damien Desfontaines, Luke Hartman, Ruchit Shrestha, and Michael Hay.  Precision-based attacks and interval refining: how to break, then fix, differential privacy on finite computers, 2022.
  * [HLM12] Moritz Hardt, Katrina Ligett, and Frank McSherry.  A simple and practical algorithm for differentially private data release.  Advances in neural information processing systems, 25, 2012.
  * [HPN11] Andreas Haeberlen, Benjamin C. Pierce, and Arjun Narayan.  Differential privacy under fire.  In 20th USENIX Security Symposium, San Francisco, CA, USA, August 8-12, 2011, Proceedings. USENIX Association, 2011.
  * [HST+23] Samuel Haney, Michael Shoemate, Grace Tian, Salil P. Vadhan, Andrew Vyrros, Vicki Xu, and Wanrong Zhang.  Concurrent composition for interactive differential privacy with adaptive privacy-loss parameters.  In Weizhi Meng, Christian Damsgaard Jensen, Cas Cremers, and Engin Kirda, editors, Proceedings of the 30th ACM SIGSAC Conference on Computer and Communications Security (CCS ‘23), pages 1949–1963. ACM, 2023\.  Received a CCS ‘23 Distinguished Paper Award. Preliminary version presented as a poster at TPDP ‘23 and posted as arXiv:2309.05901 [cs.CR].
  * [JMRO22] Jiankai Jin, Eleanor McMurtry, Benjamin I. P. Rubinstein, and Olga Ohrimenko.  Are we there yet? timing and floating-point attacks on differential privacy systems.  In 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022, pages 473–488. IEEE, 2022.
  * [JNHS20] Noah M. Johnson, Joseph P. Near, Joseph M. Hellerstein, and Dawn Song.  Chorus: a programming framework for building scalable differential privacy mechanisms.  In IEEE European Symposium on Security and Privacy, EuroS&P 2020, Genoa, Italy, September 7-11, 2020, pages 535–551. IEEE, 2020.
  * [JNS18] Noah Johnson, Joseph P Near, and Dawn Song.  Towards practical differential privacy for sql queries.  Proceedings of the VLDB Endowment, 11(5):526–539, 2018.
  * [JR11] Madhav Jha and Sofya Raskhodnikova.  Testing and reconstruction of lipschitz functions with applications to data privacy.  In Rafail Ostrovsky, editor, IEEE 52nd Annual Symposium on Foundations of Computer Science, FOCS 2011, Palm Springs, CA, USA, October 22-25, 2011, pages 433–442. IEEE Computer Society, 2011.
  * [KOV15] Peter Kairouz, Sewoong Oh, and Pramod Viswanath.  The composition theorem for differential privacy.  In International conference on machine learning, pages 1376–1385. PMLR, 2015.
  * [KTH+19] Ios Kotsogiannis, Yuchao Tao, Xi He, Maryam Fanaeepour, Ashwin Machanavajjhala, Michael Hay, and Gerome Miklau.  Privatesql: a differentially private sql query engine.  Proceedings of the VLDB Endowment, 12(11):1371–1384, 2019.
  * [LVRG20] Elisabet Lobo-Vesga, Alejandro Russo, and Marco Gaboardi.  A programming framework for differential privacy with accuracy concentration bounds.  In 2020 IEEE Symposium on Security and Privacy (SP), pages 411–428. IEEE, 2020.
  * [Lyu22] Xin Lyu.  Composition theorems for interactive differential privacy.  arXiv preprint arXiv:2207.09397, 2022.
  * [McS09] Frank D McSherry.  Privacy integrated queries: an extensible platform for privacy-preserving data analysis.  In Proceedings of the 2009 ACM SIGMOD International Conference on Management of data, pages 19–30. ACM, 2009.
  * [Mir12] Ilya Mironov.  On significance of the least significant bits for differential privacy.  In Proceedings of the 2012 ACM conference on Computer and communications security, pages 650–661, 2012.
  * [Mir17] Ilya Mironov.  Rényi differential privacy.  In 2017 IEEE 30th computer security foundations symposium (CSF), pages 263–275. IEEE, 2017.
  * [MTKV18] Jack Murtagh, Kathryn Taylor, George Kellaris, and Salil P. Vadhan.  Usable differential privacy: A case study with PSI.  CoRR, abs/1809.04103, 2018.
  * [MTS+12] Prashanth Mohan, Abhradeep Thakurta, Elaine Shi, Dawn Song, and David E. Culler.  GUPT: privacy preserving data analysis made easy.  In K. Selçuk Candan, Yi Chen, Richard T. Snodgrass, Luis Gravano, and Ariel Fuxman, editors, Proceedings of the ACM SIGMOD International Conference on Management of Data, SIGMOD 2012, Scottsdale, AZ, USA, May 20-24, 2012, pages 349–360. ACM, 2012.
  * [MV16] Jack Murtagh and Salil Vadhan.  The complexity of computing the optimal composition of differential privacy.  In Theory of Cryptography Conference, pages 157–175. Springer, 2016\.
  * [NDA+19] Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, and Dawn Song.  Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy.  Proc. ACM Program. Lang., 3(OOPSLA):172:1–172:30, 2019.
  * [NH+21] Joseph P Near, Xi He, et al.  Differential privacy for databases.  Foundations and Trends® in Databases, 11(2):109–225, 2021.
  * [NRS07] Kobbi Nissim, Sofya Raskhodnikova, and Adam D. Smith.  Smooth sensitivity and sampling in private data analysis.  In David S. Johnson and Uriel Feige, editors, Proceedings of the 39th Annual ACM Symposium on Theory of Computing, San Diego, California, USA, June 11-13, 2007, pages 75–84. ACM, 2007.
  * [RP10] Jason Reed and Benjamin C. Pierce.  Distance makes the types grow stronger: a calculus for differential privacy.  In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 157–168. ACM, 2010.
  * [RRUV16] Ryan Rogers, Aaron Roth, Jonathan Ullman, and Salil Vadhan.  Privacy odometers and filters: Pay-as-you-go composition.  In Advances in Neural Information Processing Systems 29 (NIPS ‘16), pages 1921–1929, December 2016.  Full version posted as arXiv:1605.08294 [cs.CR].
  * [RSK+10] Indrajit Roy, Srinath T. V. Setty, Ann Kilzer, Vitaly Shmatikov, and Emmett Witchel.  Airavat: Security and privacy for mapreduce.  In Proceedings of the 7th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2010, April 28-30, 2010, San Jose, CA, USA, pages 297–312. USENIX Association, 2010.
  * [SSH+22] Jayshree Sarathy, Sophia Song, Audrey Haque, Tania Schlatter, and Salil Vadhan.  Don’t look at the data! How differential privacy reconfigures practices of data science.  Poster at the 8th Workshop on the Theory and Practice of Differential Privacy (TPDP ‘22), July 2022.
  * [VW21] Salil Vadhan and Tianhao Wang.  Concurrent composition of differential privacy.  In Theory of Cryptography Conference, pages 582–604. Springer, 2021\.
  * [VZ22] Salil Vadhan and Wanrong Zhang.  Concurrent composition theorems for all standard variants of differential privacy.  arXiv preprint arXiv:2207.08335, 2022.
  * [WCHRP17] Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C Pierce.  A framework for adaptive differential privacy.  Proceedings of the ACM on Programming Languages, 1(ICFP):1–29, 2017\.
  * [WDKZ20] Yuxin Wang, Zeyu Ding, Daniel Kifer, and Danfeng Zhang.  Checkdp: An automated and integrated approach for proving differential privacy or finding precise counterexamples.  In Jay Ligatti, Xinming Ou, Jonathan Katz, and Giovanni Vigna, editors, CCS ’20: 2020 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, USA, November 9-13, 2020, pages 919–938. ACM, 2020.
  * [WDW+19] Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, and Danfeng Zhang.  Proving differential privacy with shadow execution.  In Kathryn S. McKinley and Kathleen Fisher, editors, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, pages 655–669. ACM, 2019.
  * [WRRW22] Justin Whitehouse, Aaditya Ramdas, Ryan Rogers, and Zhiwei Steven Wu.  Fully adaptive composition in differential privacy.  arXiv preprint arXiv:2203.05481, 2022.
  * [WZL+20] Royce J. Wilson, Celia Yuxin Zhang, William Lam, Damien Desfontaines, Daniel Simmons-Marengo, and Bryant Gipson.  Differentially private SQL with bounded user contribution.  Proc. Priv. Enhancing Technol., 2020(2):230–250, 2020.
  * [ZK17] Danfeng Zhang and Daniel Kifer.  Lightdp: towards automating differential privacy proofs.  In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 888–901. ACM, 2017\.
  * [ZMK+18] Dan Zhang, Ryan McKenna, Ios Kotsogiannis, Michael Hay, Ashwin Machanavajjhala, and Gerome Miklau.  Ektelo: A framework for defining differentially-private computations.  In Proceedings of the 2018 International Conference on Management of Data, pages 115–130. ACM, 2018.
  * [ZRH+20] Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth.  Testing differential privacy with dual interpreters.  Proc. ACM Program. Lang., 4(OOPSLA):165:1–165:26, 2020.