Proving Differential Privacy with Shadow Execution

TL;DR

This paper introduces shadow execution within ShadowDP, a new proof technique that simplifies and speeds up the formal verification of differential privacy for complex algorithms with minimal annotations.

Contribution

It presents shadow execution as a novel verification method embedded in ShadowDP, enabling efficient and less annotation-intensive proofs of differential privacy.

Findings

Verifies Report Noisy Max automatically

Verifies a new Sparse Vector variant

Verification time reduced to seconds

Abstract

Recent work on formal verification of differential privacy shows a trend toward usability and expressiveness -- generating a correctness proof of sophisticated algorithm while minimizing the annotation burden on programmers. Sometimes, combining those two requires substantial changes to program logics: one recent paper is able to verify Report Noisy Max automatically, but it involves a complex verification system using customized program logics and verifiers. In this paper, we propose a new proof technique, called shadow execution, and embed it into a language called ShadowDP. ShadowDP uses shadow execution to generate proofs of differential privacy with very few programmer annotations and without relying on customized logics and verifiers. In addition to verifying Report Noisy Max, we show that it can verify a new variant of Sparse Vector that reports the gap between some noisy query answers and the noisy threshold. Moreover, ShadowDP reduces the complexity of verification: for all of the algorithms we have evaluated, type checking and verification in total takes at most 3 seconds, while prior work takes minutes on the same algorithms.

Tables

Table 1. Table 1 . Time spent on type checking and verification

Algorithm	Type Check (s)	Verification by ShadowDP (s)		Verification by (Albarghouthi and Hsu, 2017) (s)
Report Noisy Max	0.465	1.932		22
Sparse Vector Technique ($N=1$)	0.398	1.856		27
		Rewrite	Fix $ϵ$
Sparse Vector Technique	0.399	2.629	1.679	580
Numerical Sparse Vector Technique ($N=1$)	0.418	1.783	1.788	4
Numerical Sparse Vector Technique	0.421	2.584	1.662	5
Gap Sparse Vector Technique	0.424	2.494	1.826	N/A
Partial Sum	0.445	1.922	1.897	14
Prefix Sum	0.449	1.903	1.825	14
Smart Sum	0.603	2.603	2.455	255

Equations

$$P(M(a_1)\in E)\le e^{ϵ}P(M(a_2)\in E).$$

$$P(M(a_1)\in E)$$

$$\le e^{ϵ}\sum _{\eta \mid a_2+f(\eta )\in E}{p}_{1/ϵ}(f(\eta ))$$

$$=e^{ϵ}\sum _{\eta \mid a_2+\eta \in E}{p}_{1/ϵ}(\eta )=e^{ϵ}P(M(a_2)\in E)$$

$$D_1:q[0]=1,q[1]=2,q[2]=2$$

$$D_2:q[0]=2,q[1]=1,q[2]=2$$

$$\frac{}{\text{vbox}\text{vbox}\Gamma ⊢:{\mathtt{num}}_{⟨0,0⟩}}$$

$$\frac{}{\text{vbox}\text{vbox}pc⊢\Gamma \{\mathtt{skip}\rightharpoonup \mathtt{skip}\}\Gamma }$$

$$\frac{\text{vbox}pc=\perp {\Gamma }^{\prime }=\lambda x.⟨\mathcal{S}(⟨n^{\circ },n^{†}⟩),n^{†}⟩\text{ where }\Gamma ⊢x:{\mathcal{B}}_{⟨n^{\circ },n^{†}⟩}\Psi \Rightarrow ((\eta +n_{\eta })\{{\eta }_1/\eta \}=(\eta +n_{\eta })\{{\eta }_2/\eta \}\Rightarrow {\eta }_1={\eta }_2)\text{vbox}}{\text{vbox}\text{vbox}pc⊢\Gamma \{\eta :=\mathtt{Lap};\mathcal{S},n_{\eta }\rightharpoonup \eta :=\mathtt{Lap};\mathcal{S},n_{\eta }\}{\Gamma }^{\prime }[\eta \mapsto {\mathtt{num}}_{⟨n_{\eta },0⟩}]}$$

$$\frac{\text{vbox}{\Gamma }_1⊑{\Gamma }_2\text{raise}0.0pt\text{vbox}\text{vbox}\text{vbox}\text{vbox}{c}^{\circ }=\{{\hat{x}}^{\circ }:=n\mid {\Gamma }_1(x)={\mathtt{num}}_{⟨n,d_1⟩}\wedge {\Gamma }_2(x)={\mathtt{num}}_{⟨\ast ,d_2⟩}\}{c}^{\circ }=\{{\hat{x}}^{\circ }:=n\mid {\Gamma }_1(x)={\mathtt{num}}_{⟨n,d_1⟩}\wedge {\Gamma }_2(x)={\mathtt{num}}_{⟨\ast ,d_2⟩}\}{c}^{†}=\{{\hat{x}}^{†}:=n\mid {\Gamma }_1(x)={\mathtt{num}}_{⟨d_1,n⟩}\wedge {\Gamma }_2(x)={\mathtt{num}}_{⟨d_2,\ast ⟩}\}\text{vbox}{c}^{\prime }=\{\begin{array}{ll}{c}^{\circ };c^{†}& \text{ if }pc=\perp \\ c^{\circ }& \text{ if }pc=\top \end{array}\text{vbox}}{\text{vbox}\text{vbox}{\Gamma }_1,{\Gamma }_2,pc\Rrightarrow c^{\prime }}$$

$$\text{vspace}0.2em\circ (⟨e_1,e_2⟩)=e_1\text{penalty}50plus0.5filminus5.0pt†(⟨e_1,e_2⟩)=e_2\text{penalty}50plus0.5filminus5.0pt(e?{\mathcal{S}}_1:{\mathcal{S}}_2)(⟨e_1,e_2⟩)=e?{\mathcal{S}}_1(⟨e_1,e_2⟩):{\mathcal{S}}_2(⟨e_1,e_2⟩)$$

$$\mathtt{updPC}(pc,\Gamma ,e)=\{\begin{array}{l}\perp \text{ , if }pc=\perp \wedge \Psi \Rightarrow (e\iff \text{llparenthesis}e,\Gamma {\text{rrparenthesis}}^{†})\\ \top \text{ , else}\end{array}$$

$$\Psi \Rightarrow (e_1\odot e_2\iff (e_1+n_1)\odot (e_2+n_3)\wedge (e_1+n_2)\odot (e_2+n_4))$$

$$pc⊢\Gamma \{c\rightharpoonup c^{\prime }\}{\Gamma }^{\prime }$$

$$d_1\bigsqcup d_2\triangleq \{\begin{array}{ll}{d}_1& \text{if }{d}_1=d_2\\ \ast & \text{otherwise }\end{array}$$

$$pc⊢{\Gamma }_i^{\prime }\{c\rightharpoonup c_i^{\prime }\}{\Gamma }_i^{\prime \prime }\text{ for all }0\le i\le n$$

$$\frac{}{\text{vbox}\text{vbox}\eta :=\mathtt{Lap};\mathcal{S},n_{\eta }\rightrightarrows \mathtt{havoc}\eta ;{\mathbf{v}}_{ϵ}:=\mathcal{S}(⟨{\mathbf{v}}_{ϵ},0⟩)+|n_{\eta }|/r;}$$

$$pc⊢{\Gamma }_1\{c\rightharpoonup c^{\prime }\}{\Gamma }_2\text{ and }{c}^{\prime }\rightrightarrows c^{\prime \prime }$$

$$m\uplus (\gamma )(x)=\{\begin{array}{ll}m(x),& x\in \text{emVars}\\ \gamma (x),& x\in \widehat{\text{emVars}}\end{array}$$

$$[[c^{\prime }{]]}_{m_1^{\prime }}(m_2^{\prime })=[[c{]]}_{m_1}(m_2)$$

$$m_2(x)=m_1^{\prime }(x)+m_1^{\prime }(d^{\circ })$$

$$\Psi \Rightarrow ((\eta +n_{\eta })\{{\eta }_1/\eta \}=(\eta +n_{\eta })\{{\eta }_2/\eta \}\Rightarrow {\eta }_1={\eta }_2)$$

$${\Gamma }_2^{\star }{m}_1^{\prime }={\Gamma }_2^{\star }{m}_2^{\prime }⟹m_1^{\prime }=m_2^{\prime }$$

$$m^{\prime }\uplus (ϵ)({\mathbf{v}}_{ϵ})=ϵ,\text{ and }{m}^{\prime }\uplus (ϵ)(x)=m(x),\forall x\in \mathtt{dom}(m^{\prime }).$$

$$c^{\prime \prime }{\upharpoonright }_{m_1^{\prime }}^{m_2^{\prime }}\triangleq \{ϵ\mid m_2^{\prime }\uplus (ϵ)\in [[c^{\prime \prime }{]]}_{m_1^{\prime }\uplus (0)}\}$$

$$[[c^{\prime }{]]}_{m_1^{\prime }}(m_2^{\prime })\le [[c{]]}_{{\Gamma }_1^{†}{m}_1^{\prime }}({\Gamma }_2^{†}{m}_2^{\prime })\text{ when }pc=\perp$$

$$[[c^{\prime }{]]}_{m_1^{\prime }}(m_2^{\prime })$$

$$m_2^{\prime }\uplus ({ϵ}^{\prime })\in [[c^{\prime \prime }{]]}_{m_1^{\prime }\uplus (0)}\Rightarrow {ϵ}^{\prime }\le ϵ$$

$$\underset{S\subseteq {\mathcal{M}}^{\prime }}{\max }([[c^{\prime }{]]}_{m_1^{\prime }}(S)-\exp (ϵ)[[c{]]}_{{\Gamma }_1^{\circ }{m}_1^{\prime }}({\Gamma }_2^{\circ }S))$$

$$\underset{S\subseteq {\mathcal{M}}^{\prime }}{\max }([[c^{\prime }{]]}_{m_1^{\prime }}(S)-\exp (ϵ)[[c{]]}_{{\Gamma }_1^{†}{m}_1^{\prime }}({\Gamma }_2^{\circ }S))$$

$$[[c^{\prime }{]]}_{m_1^{\prime }}(m_2^{\prime })\le \exp (ϵ)[[c{]]}_{{\Gamma }_1^{\circ }{m}_1^{\prime }}({\Gamma }_2^{\circ }{m}_2^{\prime }),\forall m_2^{\prime }\in S,$$

$$[[c^{\prime }{]]}_{m_1^{\prime }}(m_2^{\prime })\le \exp (ϵ)[[c{]]}_{{\Gamma }_1^{†}{m}_1^{\prime }}({\Gamma }_2^{\circ }{m}_2^{\prime }),\forall m_2^{\prime }\in S.$$

Full text

In this paper, we propose a new proof technique, called shadow execution, and embed it into a language called ShadowDP. ShadowDP uses shadow execution to generate proofs of differential privacy with very few programmer annotations and without relying on customized logics and verifiers. In addition to verifying Report Noisy Max, we show that it can verify a new variant of Sparse Vector that reports the gap between some noisy query answers and the noisy threshold. Moreover, ShadowDP reduces the complexity of verification: for all of the algorithms we have evaluated, type checking and verification in total takes at most 3 seconds, while prior work takes minutes on the same algorithms.

Differential privacy; dependent types

††copyright: acmcopyright††price: 15.00††doi: 10.1145/3314221.3314619††journalyear: 2019††isbn: 978-1-4503-6712-7/19/06††conference: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation; June 22–26, 2019; Phoenix, AZ, USA††booktitle: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’19), June 22–26, 2019, Phoenix, AZ, USA††ccs: Software and its engineering Formal software verification

1. Introduction

Differential privacy is increasingly being used in industry (Erlingsson et al., 2014; Team, 2017; Johnson et al., 2018) and government agencies (Abowd, 2018) to provide statistical information about groups of people without violating their privacy. Due to the prevalence of errors in published algorithms and code (Lyu et al., 2017), formal verification of differential privacy is critical to its success.

The initial line of work on formal verification for differential privacy (e.g., (Barthe et al., 2015; Barthe and Olmedo, 2013; Barthe et al., 2012, 2014, 2016b)) was concerned with increasing expressiveness. A parallel line of work (e.g., (McSherry, 2009; Roy et al., 2010; Mohan et al., 2012; Zhang et al., 2018)) focuses more on usability – on developing platforms that keep track of the privacy cost of an algorithm while limiting the types of algorithms that users can produce.

A recent line of work (most notably LightDP (Zhang and Kifer, 2017) and Synthesizing Coupling Proofs (Albarghouthi and Hsu, 2017)) has sought to combine expressiveness and usability by providing verification tools that infer most (if not all) of the proof of privacy. The benchmark algorithms for this task were Sparse Vector (Lyu et al., 2017; Dwork et al., 2014) and Report Noisy Max (Dwork et al., 2014). LightDP (Zhang and Kifer, 2017) was the first system that could verify Sparse Vector with very few annotations, but it could not verify tight privacy bounds on Report Noisy Max (Dwork et al., 2014). It is believed that proofs using randomness alignment, the proof technique that underpins LightDP, are often simpler, while approximate coupling, the proof technique that underpins (Barthe et al., 2015; Barthe and Olmedo, 2013; Barthe et al., 2012, 2014, 2016b), seems to be more expressive (Albarghouthi and Hsu, 2017). Subsequently, Albarghouthi and Hsu (Albarghouthi and Hsu, 2017) produced the first fully automated system that verifies both Sparse Vector and Report Noisy Max. Although this new system takes inspiration from randomness alignment to simplify approximate coupling proofs, its verification system still involves challenging features such as first-order Horn clauses and probabilistic constraints; it takes minutes to verify simple algorithms. The complex verification system also prevents it from reusing off-the-shelf verification tools.

In this paper, we present ShadowDP, a language for verifying differentially private algorithms. It is based on a new proof technique called “shadow execution”, which enables language-based proofs based on standard program logics. Built on randomness alignment, it transforms a probabilistic program into a program in which the privacy cost is explicit; so that the target program can be readily verified by off-the-shelf verification tools. However, unlike LightDP, it can verify more challenging algorithms such as Report Noisy Max and a novel variant of Sparse Vector called Difference Sparse Vector. We show that with minimum annotations, challenging algorithms that took minutes to verify by (Albarghouthi and Hsu, 2017) (excluding proof synthesis time) now can be verified within 3 seconds with an off-the-shelf model checker.

One extra benefit of this approach based on randomness alignment is that the transformed program can also be analyzed by standard symbolic executors. This appears to be an important property in light of recent work on detecting counterexamples for buggy programs (Ding et al., 2018; Bichsel et al., 2018; Gilbert and McMillan, 2018; Farina et al., 2017). Producing a transformed program that can be used for verification of correct programs and bug-finding for incorrect programs is one aspect that is of independent interest (however, we leave this application of transformed programs to future work).

In summary, this paper makes the following contributions:

1. (1)

Shadow execution, a new proof technique for differential privacy (Section 2.4). 2. (2)

ShadowDP, a new imperative language (Section 3) with a flow-sensitive type system (Section 4) for verifying sophisticated privacy-preserving algorithms. 3. (3)

A formal proof that the verification of the transformed program by ShadowDP implies that the source code is $\epsilon$-differentially private (Section 5). 4. (4)

Case studies on sophisticated algorithms showing that verifying privacy-preserving algorithms using ShadowDP requires little programmer annotation burden and verification time (Section 6). 5. (5)

Verification of a variant of Sparse Vector Technique that releases the difference between noisy query answers and a noisy threshold at the same privacy level as the original algorithm (Lyu et al., 2017; Dwork et al., 2014). To the best of our knowledge, this variant has not been studied before.

2. Preliminaries and Illustrating Example

2.1. Differential Privacy

Differential privacy is now considered a gold standard in privacy protections after recent high profile adoptions (Erlingsson et al., 2014; Team, 2017; Johnson et al., 2018; Abowd, 2018). There are currently several popular variants of differential privacy (Dwork et al., 2006b; Dwork et al., 2006a; Bun and Steinke, 2016; Mironov, 2017). In this paper, we focus on the verification of algorithms that satisfy pure differential privacy (Dwork et al., 2006b), which has several key advantages – it is the strongest one among them, the most popular one, and the easiest to explain to non-technical end-users (Nissim et al., 2017).

Differential privacy requires an algorithm to inject carefully calibrated random noise during its computation. The purpose of the noise is to hide the effect of any person’s record on the output of the algorithm. In order to present the formal definition, we first define the set of sub-distributions over a discrete set $A$, written $\mathbf{Dist}(A)$, as the set of functions $\mu:A\rightarrow[0,1]$, such that $\sum_{a\in A}\mu(a)\leq 1$. When applied to an event $E\subseteq A$, we define $\mu(E)\triangleq\sum_{e\in E}\mu(e)$. 111As is standard in this line of work (e.g., (Barthe et al., 2016b; Zhang and Kifer, 2017)), we assume a sub-distribution instead of a distribution, since sub-distribution gives rise to an elegant program semantics in face of non-terminating programs (Kozen, 1981).

Differential privacy relies on the notion of adjacent databases (e.g., pairs of databases that differ on one record). Since differentially-private algorithms sometimes operate on query results from databases, we abstract adjacent databases as an adjacency relation ${\Psi}\subseteq A\times A$ on input query answers. For differential privacy, the most commonly used relations are:

(1) each query answer may differ by at most $n$ (for some number $n$), and

(2) at most one query answer may differ, and that query answer differs by at most $n$. This is also known as sensitivity of the queries.

Definition 0 (Pure Differential privacy).

Let $\epsilon\geq 0$. A probabilistic computation $M:A\rightarrow B$ is $\epsilon$-differentially private with respect to an adjacency relation ${\Psi}$ if for every pair of inputs $a_{1},a_{2}\in A$ such that $a_{1}{\Psi}a_{2}$, and every output subset $E\subseteq B$,

[TABLE]

2.2. Randomness Alignment

Randomness Alignment (Zhang and Kifer, 2017) is a simple yet powerful technique to prove differential privacy. Here, we illustrate the key idea with a fundamental mechanism for satisfying differential privacy–the Laplace Mechanism (McSherry and Talwar, 2007).

Following the notations in Section 2.1, we consider an arbitrary pair of query answers $a_{1}$ and $a_{2}$ that differ by at most 1, i.e., $-1\leq a_{1}-a_{2}=c\leq 1$. The Laplace Mechanism (denoted as $M$) simply releases $a+\eta$, where $\eta$ is a random noise sampled from the Laplace distribution of mean 0 and scale $1/\epsilon$; we use $p_{1/\epsilon}$ to denote its density function. The goal of randomness alignment is to “align” the random noise in two executions $M(a_{1})$ and $M(a_{2})$, such that $M(a_{1})=M(a_{2})$, with a corresponding privacy cost. To do so, we create an injective function $f:\mathbb{R}\rightarrow\mathbb{R}$ that maps $\eta$ to $\eta+c$. Obviously, $f$ is an alignment since $a_{1}+\eta=a_{2}+f(\eta)$ for any $a_{1}$, $a_{2}$. Then for an arbitrary set of outputs $E\subseteq\mathbb{R}$, we have:

[TABLE]

The first inequality is by the definition of $f$: $a_{1}+\eta\in E\implies a_{2}+f(\eta)\in E$. The $e^{\epsilon}$ factor results from the fact that p_{1/\epsilon}(\eta+c)\big{/}p_{1/\epsilon}(\eta)\leq e^{\lvert c\rvert\cdot\epsilon}\leq e^{\epsilon}, when the Laplace distribution has scale $1/\epsilon$. The second to last equality is by change of variable from $f(\eta)$ to $\eta$ in the summation, using the injectivity of $f$.

In general, let $H\in\mathbb{R}^{n}$ be the random noise vector that a mechanism $M$ uses. A randomness alignment for $a_{1}\Psi a_{2}$ is a function $f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$ such that:

1. (1)

$M(a_{2})$ with noise $f(H)$ outputs the same result as $M(a_{1})$ with noise $H$ (hence the name Randomness Alignment). 2. (2)

$f$ is injective (this is to allow change of variables).

2.3. The Report Noisy Max Algorithm

To illustrate the challenges in proving differential privacy, we consider the Report Noisy Max algorithm (Dwork et al., 2014), whose source code is shown on the top of Figure 1. It can be used as a building block in algorithms that iteratively generate differentially private synthetic data by finding (with high probability) the identity of the query for which the synthetic data currently has the largest error (Hardt et al., 2012).

The algorithm takes a list $q$ of query answers, each of which differs by at most 1 if the underlying database is replaced with an adjacent one. The goal is to return the index of the largest query answer (as accurately as possible subject to privacy constraints).

To achieve differential privacy, the algorithm adds appropriate Laplace noise to each query. Here, $\mathtt{Lap}~{}{(}2/\epsilon)$ draws one sample from the Laplace distribution with mean zero and a scale factor $(2/\epsilon)$. For privacy, the algorithm uses the noisy query answer ($q[i]+\eta$) rather than the true query answer ($q[i]$) to compute and return the index of the maximum (noisy) query answer. Note that the return value is listed right below the function signature in the source code.

Informal proof using randomness alignment

Proofs of correctness of Report Noisy Max can be found in (Dwork et al., 2014). We will start with an informal correctness argument, based on the randomness alignment technique (Section 2.2), to illustrate subtleties involved in the proof.

Consider the following two databases $D_{1},D_{2}$ that differ on one record, and their corresponding query answers:

[TABLE]

Suppose in one execution on $D_{1}$, the noise added to $q[0]$, $q[1]$, $q[2]$ is $\alpha^{(1)}_{0}=1$, $\alpha^{(1)}_{1}=2$, $\alpha^{(1)}_{2}=1$, respectively. In this case, the noisy query answers are $q[0]+\alpha^{(1)}_{0}=2$, $q[1]+\alpha^{(1)}_{1}=4$, $q[2]+\alpha^{(1)}_{2}=3$ and so the algorithm returns $1$, which is the index of the maximum noise query answer of $4$.

Aligning randomness

As shown in Section 2.2, we need to create an injective function of random bits in $D_{1}$ to random bits in $D_{2}$ to make the output the same. Recall that $\alpha^{(1)}_{0},\alpha^{(1)}_{1},\alpha^{(1)}_{2}$ are the noise added to $D_{1}$, now let $\alpha^{(2)}_{0},\alpha^{(2)}_{1},\alpha^{(2)}_{2}$ be the noise added to the queries $q[0],q[1],q[2]$ in $D_{2}$, respectively. Consider the following injective function: for any query except for $q[1]$, use the same noise as on $D_{1}$; add 2 to the noise used for $q[1]$ (i.e., $\alpha^{(2)}_{1}=\alpha^{(1)}_{1}+2$).

In our running example, execution on $D_{2}$ with this alignment function would result in noisy query answers $q[0]+\alpha^{(2)}_{0}=3$, $q[1]+\alpha^{(2)}_{1}=5$, $q[2]+\alpha^{(2)}_{2}=3$. Hence, the output once again is $1$, the index of query answer $5$.

In fact, we can prove that under this alignment, every execution on $D_{1}$ where 1 is returned would result in an execution on $D_{2}$ that produces the same answer due to two facts:

1. (1)

On $D_{1}$, $q[1]+\alpha^{(1)}_{1}$ has the maximum value. 2. (2)

On $D_{2}$, $q[1]+\alpha^{(2)}_{1}$ is greater than $q[1]+\alpha^{(1)}_{1}+1$ on $D_{1}$ due to $\alpha^{(2)}_{1}=\alpha^{(1)}_{1}+2$ and the adjacency assumption.

Hence, $q[1]+\alpha^{(2)}_{1}$ on $D_{2}$ is greater than $q[i]+\alpha^{(1)}_{i}+1$ on $D_{1}$ for any $i$. By the adjacency assumption, that is the same as $q[1]+\alpha^{(2)}_{1}$ is greater than any $q[i]+\alpha^{(2)}_{i}$ on $D_{2}$. Hence, based on the same argument in Section 2.2, we can prove that the Report Noisy Max algorithm is $\epsilon$-private.

Challenges

Unfortunately, the alignment function above only applies to executions on $D_{1}$ where index $1$ is returned. If there is one more query $q[3]=4$ and the execution gets noise $\alpha^{(1)}_{3}=1$ for that query, the execution on $D_{1}$ will return index 3 instead of 1. To align randomness on $D_{2}$, we need to construct a different alignment function (following the construction above) that adds noise in the following way: for any query except for $q[3]$, use the same noise as on $D_{1}$; add 2 to the noise used for $q[3]$ (i.e., $\alpha^{(2)}_{3}=\alpha^{(1)}_{3}+2$). In other words, to carry out the proof, the alignment for each query depends on the queries and noise yet to happen in the future.

One approach of tackling this challenge, followed by existing language-based proofs of Report Noisy Max (Barthe et al., 2016b; Albarghouthi and Hsu, 2017), is to use the pointwise lifting argument: informally, if we can show that for any value $i$, execution on $D_{1}$ returns value $i$ implies execution on $D_{2}$ returns value $i$ (with a privacy cost bounded by $\epsilon$), then a program is $\epsilon$-differential private. However, this argument does not apply to the randomness alignment technique. Moreover, doing so requires a customized program logic for proving differential privacy.

2.4. Approach Overview

In this paper, we propose a new proof technique “shadow execution”, which enables language-based proofs based on standard program logics. The key insight is to track a shadow execution on $D_{2}$ where the same noise is always used as on $D_{1}$. For our running example, we illustrate the shadow execution in Figure 2, with random noise $\alpha^{(\dagger)}_{0}$, $\alpha^{(\dagger)}_{1}$ and so on. Note that the shadow execution uses $\alpha^{(\dagger)}_{i}=\alpha^{(1)}_{i}$ for all $i$.

With the shadow execution, we can construct a randomness alignment for each query $i$ as follows:

1. Case 1:

Whenever $q[i]+\alpha^{(1)}_{i}$ is the maximum value so far on $D_{1}$ (i.e., $max$ is updated), we use the alignments on shadow execution for all previous queries but a noise $\alpha^{(1)}_{i}+2$ for $q[i]$ on $D_{2}$. 2. Case 2:

Whenever $q[i]+\alpha^{(1)}_{i}$ is smaller than or equal to any previous noise query answer (i.e., $max$ is not updated), we keep the previous alignments for previous queries and use noise $\alpha^{(1)}_{i}$ for $q[i]$ on $D_{2}$.

We illustrate this construction in Figure 2. After seeing $q[1]$ on $D_{1}$ (Case 1), the construction uses noise in the shadow execution for previous query answers, and uses $\alpha_{1}^{(1)}+2=4$ as the noise for $q[1]$ on $D_{2}$. After seeing $q[2]$ on $D_{1}$ (Case 2), the construction reuses alignments constructed previously, and use $\alpha^{(1)}_{2}=1$ as the noise for $q[2]$. When $q[3]$ comes, the previous alignment is abandoned; the shadow execution is used for $q[0]$ to $q[2]$. It is easy to check that this construction is correct for any subset of query answers seen so far, since the resulting alignment is exactly the same as the informal proof above, when the index of maximum value is known.

Randomness alignment with shadow execution

To incorporate the informal argument above to a programming language, we propose ShadowDP. We illustrate the key components of ShadowDP in this section, as shown in Figure 1, and detail all components in the rest of this paper.

Similar to LightDP (Zhang and Kifer, 2017), ShadowDP embeds randomness alignments into types. In particular, each numerical variable has a type in the form of $\mathtt{num}_{\langle{\mathbb{n}^{\circ}},{\mathbb{n}^{\dagger}}\rangle}$, where $\mathbb{n}^{\circ}$ and $\mathbb{n}^{\dagger}$ represent the “difference” of its value in the aligned and shadow execution respectively. In Figure 1, non-private variables, such as $\epsilon,size$, are annotated with distance [math]. For private variables, the difference could be a constant or an expression. For example, the type of $q$ along with the precondition specifies the adjacency relation: each query answer’s difference is specified by $*$, which is desugared to a special variable $\widehat{q}^{\circ}[i]$ (details discussed in Section 4). The precondition in Figure 1 specifies that the difference of each query answer is bounded by 1 (i.e., query answers have sensitivity of 1).

ShadowDP reasons about the aligned and shadow executions in isolation, with the exception of sampling commands. A sampling command (e.g., line 3 in Figure 1) constructs the aligned execution by either using values from the aligned execution so far (symbol $\circ$), or switching to values from the shadow execution (symbol $\dagger$). The construction may depend on program state: in Figure 1, we switch to shadow values iff $q[i]+\eta$ is the max on $D_{1}$. A sampling command also specifies the alignment for the generated random noise.

With function specification and annotations for sampling commands, the type system of ShadowDP automatically checks the source code. If successful, it generates a non-probabilistic program (as shown at the bottom of Figure 1) with a distinguished variable ${\mathbf{v}_{{\epsilon}}}$. The soundness of the type system ensures the following property: if ${\mathbf{v}_{{\epsilon}}}$ is bounded by some constant $\epsilon$ in the transformed program, then the original program being verified is $\epsilon$-private.

Benefits

Compared with previous language-based proofs of Report Noisy Max (Barthe et al., 2016b; Albarghouthi and Hsu, 2017) (both are based on the pointwise lifting argument), ShadowDP enjoys a unique benefit: the transformed code can be verified based on standard program semantics. Hence, the transformed (non-probabilistic) program can be further analyzed by existing program verifiers and other tools. For example, the transformed program in Figure 1 is verified with an off-the-shelf tool CPAChecker(Beyer and Keremoglu, 2011) without any extra annotation within seconds. Although not explored in this paper, the transformed program can also be analyzed by symbolic executors to identify counterexamples when the original program is incorrect. We note that doing so will be more challenging in a customized logic.

3. ShadowDP: Syntax and Semantics

In this section, we present the syntax and semantics of ShadowDP, a simple imperative language for designing and verifying differentially private algorithms.

3.1. Syntax

The language syntax is given in Figure 3. Most parts of ShadowDP is standard; we introduce a few interesting features.

Non-probabilistic variables and expressions

ShadowDP supports real numbers, booleans as well as standard operations on them. We use ${\mathbb{n}}$ and ${\mathbb{b}}$ to represent numeric and boolean expressions respectively. A ternary numeric expression ${{\mathbb{b}}\mathbin{?}{\mathbb{n}}_{1}:{\mathbb{n}}_{2}}$ evaluates to ${\mathbb{n}}_{1}$ when the comparison evaluates to true, and ${\mathbb{n}}_{2}$ otherwise. Moreover, to model multiple queries to a database and produce multiple outputs during that process, ShadowDP supports lists: $e_{1}::e_{2}$ appends the element $e_{1}$ to a list $e_{2}$; $e_{1}[e_{2}]$ gets the $e_{2}$-th element in list $e_{1}$, assuming $e_{2}$ is bound by the length of $e_{1}$.

Random variables and expressions

To model probabilistic computation, which is essential in differentially private algorithms, ShadowDP uses random variable $\eta\in\text{\em RVars}$ to store a sample drawn from a distribution. Random variables are similar to normal variables ($x\in\text{\em NVars}$) except that they are the only ones who can get random values from random expressions, via a sampling command $\eta:=g$.

We follow the modular design of LightDP (Zhang and Kifer, 2017), where randomness expressions can be added easily. In this paper, we only consider the most interesting random expression, $\mathtt{Lap}~{}{r}$. Semantically, $\eta:=\mathtt{Lap}~{}{r}$ draws one sample from the Laplace distribution, with mean zero and a scale factor $r$, and assigns it to $\eta$. For verification purpose, a sampling command also requires a few annotations, which we explain shortly.

Types

Types in ShadowDP have the form of $\mathcal{B}_{\langle{{\mathbb{d}}^{\circ}},{{\mathbb{d}}^{\dagger}}\rangle}$, where $\mathcal{B}$ is the base type, and ${\mathbb{d}}^{\circ}$, ${\mathbb{d}}^{\dagger}$ represent the alignments for the execution on adjacent database and shadow execution respectively. Base type is standard: it includes $\mathtt{num}$ (numeric type), $\mathtt{bool}$ (Boolean), or a list of elements with type $\tau$ ($\mathtt{list}~{}\tau$).

Distance ${\mathbb{d}}$ is the key for randomness alignment proof. Intuitively, it relates two program executions so that the likelihood of seeing each is bounded by some constant. Since only numerical values have numeric distances, other data types (including $\mathtt{bool}$, $\mathtt{list}~{}\tau$ and $\tau_{1}\rightarrow\tau_{2}$) are always associated with $\langle{0},{0}\rangle$, hence omitted in the syntax. Note that this does not rule out numeric distances in nested types. For example, $(\mathtt{list}~{}\mathtt{num}_{\langle{1},{1}\rangle})$ stores numbers that differ by exactly one in both aligned and shadow executions.

Distance ${\mathbb{d}}$ can either be a numeric expression (${\mathbb{n}}$) in the language or $*$. A variable $x$ with type $\mathtt{num}_{\langle{*},{*}\rangle}$ is desugared as $x:\Sigma_{(\langle{\widehat{x}^{\circ}:\mathtt{num}_{\langle{0},{0}\rangle}},{\widehat{x}^{\dagger}:\mathtt{num}_{\langle{0},{0}\rangle}}\rangle)}~{}\mathtt{num}_{\langle{\widehat{x}^{\circ}},{\widehat{x}^{\dagger}}\rangle}$, where $\widehat{x}^{\circ}$, $\widehat{x}^{\dagger}$ are distinguished variables invisible in the source code; hiding those variables in a $\Sigma$-type simplifies the type system (Section 4).

The star type is useful for two reasons. First, it specifies the sensitivity of query answers in a precise way. Consider the parameter $q$ in Figure 1 with type $\mathtt{list}~{}\mathtt{num}_{\langle{*},{*}\rangle}$, along with the precondition $\forall i\geq 0.~{}-1\leq\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}\leq 1$. This notation makes the assumption of the Report Noisy Max algorithm explicit: each query answer differs by at most 1. Second, star type serves as the last resort when the distance of a variable cannot be tracked precisely by a static type system. For example, whenever ShadowDP merges two different distances (e.g., $3$ and $4$) of $x$ from two branches, the result distance is $*$; the type system instruments the source code to maintain the correct values of $\widehat{x}^{\circ},\widehat{x}^{\dagger}$ (Section 4).

Sampling with selectors

Each sampling instruction is attached with a few annotations for proving differential privacy, in the form of $(\eta:=\mathtt{Lap}~{}{},\mathcal{S},{\mathbb{n}}_{\eta})$. Note that just like types, the annotations $\mathcal{S}$, ${\mathbb{n}}_{\eta}$ have no effects on the program semantics; they only show up in verification. Intuitively, a selector $\mathcal{S}$ picks a version ($k\in\{\circ,\dagger\}$) for all program variables (including the previously sampled variables) at the sampling instruction, as well as constructs randomness alignment for $\eta$, specified by ${\mathbb{n}}_{\eta}$ (note that the distance cannot be $*$ by syntactical restriction here). By definition, both $\mathcal{S}$ and ${\mathbb{n}}_{\eta}$ may depend on the program state when the sampling happens.

Return to the running example in Figure 1. As illustrated in Figure 2, the selective alignment is to

• •

use shadow variables and align the new sample by $2$ whenever a new max is encountered,

• •

use aligned variables and the same sample otherwise.

Hence, the sampling command in Figure 1 is annotated as $(\eta:=\mathtt{Lap}~{}{(2/\epsilon)},\Omega\mathbin{?}\dagger:\circ,\Omega\mathbin{?}2:0)$, where $\Omega$ is $\mathtt{q[i]+}\eta>\mathtt{bq}\lor\mathtt{i=0}$, the condition when a new max is found.

3.2. Semantics

As standard, the denotational semantics of the probabilistic language is defined as a mapping from initial memory to a distribution on (possible) final outputs. Formally, let $\mathcal{M}$ be a set of memory states where each ${m}\in\mathcal{M}$ maps all (normal and random) variables ($\text{\em NVars}\cup\text{\em RVars}$) to their values.

The semantics of an expression $e$ of base type $\mathcal{B}$ is interpreted as a function $\llbracket{e}\rrbracket:\mathcal{M}\rightarrow\llbracket{\mathcal{B}}\rrbracket$, where $\llbracket{\mathcal{B}}\rrbracket$ represents the set of values belonging to the base type $\mathcal{B}$. We omit expression semantics since it is standard. A random expression $g$ is interpreted as a distribution on real values. Hence, $\llbracket{g}\rrbracket:\mathbf{Dist}(\llbracket{\mathtt{num}}\rrbracket)$. Moreover, a command $c$ is interpreted as a function $\llbracket{c}\rrbracket:\mathcal{M}\rightarrow\mathbf{Dist}(\mathcal{M})$. For brevity, we write $\llbracket{e}\rrbracket_{{m}}$ and $\llbracket{c}\rrbracket_{{m}}$ instead of $\llbracket{e}\rrbracket({m})$ and $\llbracket{c}\rrbracket({m})$ hereafter. Finally, all programs have the form $(c;\mathtt{return}~{}{e})$ where $c$ contains no return statement. A program is interpreted as a function ${m}\rightarrow\mathbf{Dist}{\llbracket{\mathcal{B}}\rrbracket}$ where $\mathcal{B}$ is the return type (of $e$).

The semantics of commands is available in the Appendix; the semantics directly follows a standard semantics in (Kozen, 1981).

4. ShadowDP: Type System

ShadowDP is equipped with a flow-sensitive type system. If successful, it generates a transformed program with needed assertions to make the original program differentially private. The transformed program is simple enough to be verified by off-the-shelf program verifiers.

4.1. Notations

We denote by $\Gamma$ the typing environment which tracks the type of each variable in a flow-sensitive way (i.e., the type of each variable at each program point is traced separately). All typing rules are formalized in Figure 4. Typing rules share a common global invariant ${\Psi}$, such as the sensitivity assumption annotated in the source code (e.g., the precondition in Figure 1). We also write $\Gamma(x)=\langle{{\mathbb{d}}^{\circ}},{{\mathbb{d}}^{\dagger}}\rangle$ for $\exists~{}\mathcal{B}.~{}\Gamma(x)=\mathcal{B}_{\langle{{\mathbb{d}}^{\circ}},{{\mathbb{d}}^{\dagger}}\rangle}$ when the base type $\mathcal{B}$ is irrelevant.

4.2. Expressions

Expression rules have the form of $\Gamma\vdash e:\tau$, which means that expression $e$ has type $\tau$ under the environment $\Gamma$. Most rules are straightforward: they compute the distance for aligned and shadow executions separately. Rule (T-OTimes) makes a conservative approach for nonlinear computations, following LightDP (Zhang and Kifer, 2017). Rule (T-VAR) desugars star types when needed. The most interesting rule is (T-ODot), which generates the following constraint:

[TABLE]

This constraint states that the boolean value of $e_{1}\odot e_{2}$ is identical in both aligned and shadow executions. If the constraint is discharged by an external solver (our type system uses Z3 (De Moura and Bjørner, 2008)), we are assured that $e_{1}\odot e_{2}$ has distances $\langle{0},{0}\rangle$.

4.3. Commands

The flow-sensitive type system tracks and checks the distances of aligned and shadow executions at each program point. Typing rules for commands have the form of

[TABLE]

meaning that starting from the previous typing environment $\Gamma$, the new typing environment is $\Gamma^{\prime}$ after $c$. We will discuss the other components $pc$ and $c^{\prime}$ shortly.

4.3.1. Aligned Variables

The type system infers and checks the distances of both aligned and shadow variables. Since most rules treat them in the same way, we first explain the rules with respect to aligned variables only, then we discuss shadow variables in Section 4.3.2. To simplify notation, we write $\Gamma$ instead of $\Gamma^{\circ}$ for now since only aligned variables are discussed.

Flow-Sensitivity

In each typing rule $pc\vdash\Gamma~{}\{c\rightharpoonup c^{\prime}\}~{}\Gamma^{\prime}$, an important invariant is that if $c$ runs on two memories that are aligned by $\Gamma$, then the final memories are aligned by $\Gamma^{\prime}$.

Consider the assignment rule (T-Asgn). This rule computes the distance of $e$’s value, ${\mathbb{n}}^{\circ}$, and updates the distance of $x$’s value after assignment to ${\mathbb{n}}^{\circ}$.

More interesting are rules (T-If) and (T-While). In (T-If), we compute the typing environments after executing $c_{1}$ and $c_{2}$ as $\Gamma_{1}$ and $\Gamma_{2}$ respectively. Since each branch may update $x$’s distance in arbitrary way, $\Gamma_{1}(x)$ and $\Gamma_{2}(x)$ may differ. We note that numeric expressions and $*$ type naturally form a two level lattice, where $*$ is higher than any ${\mathbb{n}}$. Hence, we use the following rule to merge two distances ${\mathbb{d}}_{1}$ and ${\mathbb{d}}_{2}$:

[TABLE]

For example, $(3\sqcup 4=*)$, $(x+y\sqcup x+y=x+y)$, $(x\sqcup 3=*)$. Hence, (T-If) ends with $\Gamma_{1}\sqcup\Gamma_{2}$, defined as $\lambda x.~{}\Gamma_{1}(x)\sqcup\Gamma_{2}(x)$.

As an optimization, we also use branch conditions to simplify distances. Consider our running example (Figure 1): at Line 4, $\eta$ has (aligned) distance $\Omega\mathbin{?}2:0$, where $\Omega$ is the branch condition. Its distance is simplified to $2$ in the $\mathtt{true}$ branch and [math] in the $\mathtt{false}$ branch.

Rule (T-While) is similar, except that it requires a fixed point $\Gamma_{f}$ such that $pc\vdash\Gamma\sqcup\Gamma_{f}\ \{c\}\ \Gamma_{f}$. In fact, this rule is deterministic since we can construct the fixed point as follows (the construction is similar to the one in (Hunt and Sands, 2006)):

[TABLE]

where $\Gamma_{0}^{\prime}=\Gamma,\Gamma_{i+1}^{\prime}=\Gamma_{i}^{\prime\prime}\sqcup\Gamma,\Gamma_{n+1}^{\prime}=\Gamma_{n}^{\prime}$.

It is easy to check that $\Gamma_{n}^{\prime}=\Gamma_{n+1}^{\prime}=\Gamma_{n}^{\prime\prime}\sqcup\Gamma$ and $pc^{\prime}\vdash\Gamma_{n}^{\prime}\ \{c\rightharpoonup c_{i}^{\prime}\}\ \Gamma_{n}^{\prime\prime}$ by construction. Hence, $\Gamma_{n}^{\prime\prime}$ is a fixed point: $pc\vdash\Gamma\sqcup\Gamma_{n}^{\prime\prime}\{c\rightharpoonup c_{i}^{\prime}\}\ \Gamma_{n}^{\prime\prime}$. Moreover, the computation above always terminates since all typing rules are monotonic on typing environments222That is, $\forall pc,c,\Gamma_{1},\Gamma_{2},\Gamma_{1}^{\prime},\Gamma_{2}^{\prime},c_{1},c_{2}.~{}pc\vdash\Gamma_{i}\{c\rightharpoonup c_{i}^{\prime}\}\Gamma_{i}^{\prime}\ i\in\{1,2\}\land\Gamma_{1}\sqsubseteq\Gamma_{2}\implies\Gamma_{1}^{\prime}\sqsubseteq\Gamma_{2}^{\prime}$. and the lattice has a height of 2.

Maintaining dynamically tracked distances

Each typing rule $pc\vdash\Gamma~{}\{c\rightharpoonup c^{\prime}\}~{}\Gamma^{\prime}$ also sets the value of $\widehat{x}^{\circ}$ to maintain distance dynamically whenever $\Gamma^{\prime}(x)=*$. This is achieved by the instrumented commands in $c^{\prime}$.

None of rules (T-Skip, T-Asgn, T-Seq, T-Ret) generate $*$ type, hence they do not need any instrumentation. The merge operation in rule (T-If) generates $*$ type when $\Gamma_{1}(x)\not=\Gamma_{2}(x)$. In this case, we use the auxiliary instrumentation rule in the form of $\Gamma_{1},\Gamma_{2},pc\Rrightarrow c^{\prime}$, assuming $\Gamma_{1}\sqsubseteq\Gamma_{2}$. In particular, for each variable $x$ whose distance is “upgraded” to $*$, the rule sets $\widehat{x}^{\circ}$ to the distance previously tracked by the type system ($\Gamma_{1}(x)$). Moreover, the instrumentation commands $c_{1}^{\prime\prime},c_{2}^{\prime\prime}$ are inserted under their corresponding branches.

Consider the following example:

⬇

if (x > 1) x := y; else y := 1;

staring with $\Gamma_{0}:\{x:1,y:0\}$. In the $\mathtt{true}$ branch, rule (T-Asgn) updates $x$ to the distance of $y$, resulting $\Gamma_{1}:\{x:0,y:0\}$. Similarly, we get $\Gamma_{2}:\{x:1,y:0\}$ in the $\mathtt{false}$ branch. Moreover, when we merge the typing environments $\Gamma_{1}$ and $\Gamma_{2}$ at the end of branch, the typing environment becomes $\Gamma_{3}=\Gamma_{1}\sqcup\Gamma_{2}=\{x:*,y:0\}$. Since $\Gamma_{1}(x)\neq\Gamma_{2}(x)$, instrumentation rule is also applied, which instruments $\widehat{\mathtt{x}}^{\circ}\texttt{ := 0}$ after x := y and $\widehat{\mathtt{x}}^{\circ}\texttt{ := 1}$ after y := 1.

Rule (T-While) may also generate $*$ types. Following the same process in rule (T-If), it also uses the instrumentation rule to update corresponding dynamically tracked distance variables. The instrumentation command $c_{s}$ is inserted before loop and $c^{\prime\prime}$ after the commands in the loop body.

Well-Formedness

Whenever an assignment $x:=e$ is executed, no variable’s distance should depend on $x$. To see why, consider $x:=2$ with initial $\Gamma^{\circ}(y)=x$ and $m(x)=1$. Since this assignment does not modify the value of $y$, the aligned value of $y$ (i.e., $y+\Gamma^{\circ}(y)$) should not change. However, $\Gamma^{\circ}(y)$ changes from 1 to 2 after the assignment.

To avoid this issue, we check the following condition for each assignment $x:=e$: $\forall y\in\text{\em Vars}.~{}x\notin\text{\em Vars}(\Gamma(y))$. In case that the check fails for some $y$, we promote its distance to $*$, and use the auxiliary instrumentation $\Rrightarrow$ to set $\widehat{y}^{\circ}$ properly. Hence, well-formedness is guaranteed: no variable’s distance depends on $x$ when $x$ is updated.

Aligned branches

For differential privacy, we require the aligned execution to follow the same branch as the original execution. Due to dynamically tracked distances, statically checking that in a type system could be imprecise. Hence, we use assertions in rules (T-If) and (T-While) to ensure the aligned execution does not diverge. In those rules, $\llparenthesis{e,\Gamma}\rrparenthesis^{\circ}$ simply computes the value of $e$ in the aligned execution; its full definition is in the Appendix.

4.3.2. Shadow Variables

In most typing rules, shadow variables are handled in the same way as aligned ones, which is discussed above. The key difference is that the type system allows the shadow execution to take a different branch from the original execution.

The extra permissiveness is the key ingredient of verifying algorithms such as Report Noisy Max. To see why, consider the example in Figure 2, where the shadow execution runs on $D_{2}$ with same random noise as from the execution on $D_{1}$. Upon the second query, the shadow execution does not update max, since its noisy value $3$ is the same as the previous max; however, execution on $D_{1}$ will update max, since the noisy query value of $4$ is greater than the previous max of $2$.

To capture the potential divergence of shadow execution, each typing rule is associated with a program counter $pc$ with two possible values $\bot$ and $\top$ (introducing program counters in a type system is common in information flow control to track implicit flows (Sabelfeld and Myers, 2003)). Here, $\top$ (resp. $\bot$) means that the shadow execution might take a different branch (resp. must take the same branch) as the original execution.

When $pc=\bot$, the shadow execution is checked in the same way as aligned execution. When $pc=\top$, the shadow distances are updated (as done in Rule (T-Asgn)) so that $x+\widehat{x}^{\dagger}$ remains the same. The new value from the shadow execution will be maintained by the type system when $pc$ transits from $\bot$ to $\top$ by code instrumentation for sub-commands in (T-If) and (T-While), as we show next.

Take a branch $(\mathtt{if}~{}{e}~{}\mathtt{then}~{}{c_{1}}~{}\mathtt{else}~{}{c_{2}})$ for example. The transition happens when $pc=\bot\land pc^{\prime}=\top$. In this case, we construct a shadow execution of $c$ by an auxiliary function $\llparenthesis{c,\Gamma}\rrparenthesis^{\dagger}$. The shadow execution essentially replaces each variable $x$ with their correspondence (i.e., $x+\widehat{x}^{\dagger}$), as is standard in self-composition (Barthe et al., 2004; Terauchi and Aiken, 2005). The only difference is that $\llparenthesis{c,\Gamma}\rrparenthesis^{\dagger}$ is not applicable to sampling commands, since we are unable to align the sample variables when different amount of samples are taken. The full definition of $\llparenthesis{c,\Gamma}\rrparenthesis^{\dagger}$ is available in the Appendix. Rule (T-While) is very similar in its way of handling shadow variables.

4.3.3. Sampling Command

Rule (T-Laplace) checks the only probabilistic command $\eta:=\mathtt{Lap}~{}{}\mathbin{,}\mathcal{S}\mathbin{,}{\mathbb{n}}_{\eta}$ in ShadowDP. Here, the selector $\mathcal{S}$ and numeric distance ${\mathbb{n}}_{\eta}$ are annotations provided by a programmer to aid type checking. For the sample $\eta$, the aligned distance is specified by ${\mathbb{n}}_{\eta}$ and the shadow distance is always 0 (since by definition, shadow execution use the same sample as the original program). Hence, the type of $\eta$ becomes $\mathtt{num}_{\langle{{\mathbb{n}}_{\eta}},{0}\rangle}$.

Moreover, the selector constructs the aligned execution from either the aligned ($\circ$) or shadow ($\dagger$) execution. Since the selector may depend on a condition $e$, we use the selector function $\mathcal{S}(\langle{e_{1}},{e_{2}}\rangle)$ in Figure 4 to do so.

Rule (T-Laplace) also checks that each $\eta$ is generated in an injective way: the same aligned value of $\eta$ implies the same value of $\eta$ in the original execution.

Consider the sampling command in Figure 1. The typing environments before and after the command is shown below (we omit unrelated parts for brevity):

⬇

$\{\mathtt{bq}:\langle{*},{*}\rangle,\cdots\}$

$\eta$ := $\mathtt{Lap}~{}{(}2/\epsilon)\mathbin{,}\Omega\mathbin{?}\dagger:\circ\mathbin{\mathbin{,}}\Omega\mathbin{?}2:0\text{;}$

$\{\mathtt{bq}:\langle{\Omega\mathbin{?}{\widehat{\mathtt{bq}}^{\dagger}}:\widehat{\mathtt{bq}}^{\circ}},{{\widehat{\mathtt{bq}}^{\dagger}}}\rangle\mathbin{,}\mathtt{\eta}:\langle{\Omega\mathbin{?}2:0},{0}\rangle\mathbin{,}\cdots\}$

In this example, $\mathcal{S}$ is $\Omega\mathbin{?}\dagger:\circ$. So the aligned distance of variable $\mathtt{bq}$ will be $\Omega\mathbin{?}{\widehat{\mathtt{bq}}^{\dagger}}:\widehat{\mathtt{bq}}^{\circ}$, the shadow distance of variable $\mathtt{bq}$ is still $\widehat{\mathtt{bq}}^{\dagger}$. The aligned distance of $\eta$ is $\langle{\Omega\mathbin{?}2:0},{0}\rangle$, where the aligned part is specified in the annotation.

4.4. Target Language

One goal of ShadowDP is to enable verification of $\epsilon$-differential privacy using off-the-shelf verification tools. In the transformed code so far, we assumed $\mathtt{assert}$ commands to verify that certain condition holds. The only remaining challenging feature is the sampling commands, which requires probabilistic reasoning. Motivated by LightDP (Zhang and Kifer, 2017), we note that for $\epsilon$-differential privacy, we are only concerned with the maximum privacy cost, not its likelihood. Hence, in the final step, we simply replace the sampling command with a non-deterministic command $\mathtt{havoc}~{}{\eta}$, which semantically sets the variable $\eta$ to an arbitrary value upon execution, as shown in Figure 5.

Note that a distinguished variable ${\mathbf{v}_{{\epsilon}}}$ is added by the type system to explicitly track the privacy cost of the original program. For Laplace distribution, aligning $\eta$ by the distance of ${\mathbb{n}}_{\eta}$ is associated with a privacy cost of $|{\mathbb{n}}_{\eta}|/r$. The reason is that the ratio of any two points that are $|{\mathbb{n}}_{\eta}|$ apart in the Laplace distribution with scaling factor $r$ is bounded by $\exp(|{\mathbb{n}}_{\eta}|/r)$. Since the shadow execution uses the same sample, it has no privacy cost. This very fact allows us to reset privacy cost when the shadow execution is used (i.e., $\mathcal{S}$ selects $\dagger$): the rule sets privacy cost to $0+|{\mathbb{n}}_{\eta}|/r$ in this case.

In Figure 1, ${\mathbf{v}_{{\epsilon}}}$ is set to $\Omega\mathbin{?}0:{\mathbf{v}_{{\epsilon}}}+\Omega\mathbin{?}\epsilon:0$ which is the same as $\Omega\mathbin{?}\epsilon:{\mathbf{v}_{{\epsilon}}}$. Intuitively, that implies that the privacy cost of the entire algorithm is either $\epsilon$ (when a new max is found) or the same as the previous value of ${\mathbf{v}_{{\epsilon}}}$.

The type system guarantees the following important property: if the original program type checks and the privacy cost ${\mathbf{v}_{{\epsilon}}}$ in the target language is bounded by some constant $\epsilon$ in all possible executions of the program, then the original program satisfies $\epsilon$-differential privacy. We will provide a soundness proof in the next section. Consider the running example in Figure 1. The transformed program in the target language is shown at the bottom. With a model checking tool CPAChecker (Beyer and Keremoglu, 2011), we verified that ${\mathbf{v}_{{\epsilon}}}\leq\epsilon$ in the transformed program within 2 seconds (Section 6.3). Hence, the Report Noisy Max algorithm is verified to be $\epsilon$-differentially private.

5. Soundness

The type system performs a two-stage transformation:

[TABLE]

Here, both $c$ and $c^{\prime}$ are probabilistic programs; the difference is that $c$ executes on the original memory without any distance tracking variables; $c^{\prime}$ executes on the extended memory where distance tracking variables are visible. In the second stage, $c^{\prime}$ is transformed to a non-probabilistic program $c^{\prime\prime}$ where sampling instructions are replaced by $\mathtt{havoc}~{}{}$ and the privacy cost ${\mathbf{v}_{{\epsilon}}}$ is explicit. In this section, we use $c,c^{\prime},c^{\prime\prime}$ to represent the source, transformed, and target program respectively.

Overall, the type system ensures $\epsilon$-differential privacy (Theorem 10): if the value of ${\mathbf{v}_{{\epsilon}}}$ in $c^{\prime\prime}$ is always bounded by a constant $\epsilon$, then $c$ is $\epsilon$-differentially private. In this section, we formalize the key properties of our type system and prove its soundness. Due to space constraints, the complete proofs are available in the Appendix.

Extended Memory

Command $c^{\prime}$ is different from $c$ since it maintains and uses distance tracking variables. To close the gap, we first extend memory $m$ to include those variables, denoted as $\widehat{\text{\em Vars}}=\cup_{x\in\text{\em NVars}}\{\widehat{x}^{\circ},\widehat{x}^{\dagger}\}$ and introduce a distance environment $\gamma:\widehat{\text{\em Vars}}\rightarrow\mathbb{R}$.

Definition 0.

Let $\gamma:\widehat{\text{\em Vars}}\rightarrow\mathbb{R}$. For any $m\in\mathcal{M}$, there is an extension of $m$,written ${m}\uplus({\gamma})$, such that

[TABLE]

We use ${\mathcal{M}}^{\prime}$ to denote the set of extended memory states and $m_{1}^{\prime}$, $m_{2}^{\prime}$ to refer to concrete extended memory states. We note that although the programs $c$ and $c^{\prime}$ are probabilistic, the extra commands in $c^{\prime}$ are deterministic. Hence, $c^{\prime}$ preserves the semantics of $c$, as formalized by the following Lemma.

Lemma 0 (Consistency).

Suppose $pc\vdash\Gamma_{1}~{}\{c\rightharpoonup c^{\prime}\}~{}\Gamma_{2}$. Then for any initial and final memory $m_{1}$, $m_{2}$ such that $\llbracket{c}\rrbracket_{m_{1}}(m_{2})\neq 0$, and any extension $m_{1}^{\prime}$ of $m_{1}$, there is a unique extension $m_{2}^{\prime}$ of $m_{2}$ such that

[TABLE]

Proof.

By structural induction on $c$. The only interesting case is the (probabilistic) sampling command, which does not modify distance tracking variables. ∎

From now on, we will use $m_{2}^{\prime}$ to denote the unique extension of $m_{2}$ satisfying the property above.

$\Gamma$-Relation

To formalize and prove the soundness property, we notice that a typing environment $\Gamma$ along with distance environment $\gamma$ induces two binary relations on memories. We write ${m_{1}}\uplus({\gamma})~{}\Gamma^{\circ}~{}m_{2}$ (resp. ${m_{1}}\uplus({\gamma})~{}\Gamma^{\dagger}~{}m_{2}$) when $m_{1},m_{2}$ are related by $\Gamma^{\circ}$ (resp. $\Gamma^{\dagger}$) and $\gamma$. Intuitively, the initial $\gamma$ and $\Gamma$ (given by the function signature) specify the adjacency relation, and the relation is maintained by the type system throughout program execution. For example, the initial $\gamma$ and $\Gamma$ in Figure 1 specifies that two executions of the program is related if non-private variables $\epsilon,size$ are identical, and each query answer in $q[i]$ differs by at most one.

To facilitate the proof, we simply write $m_{1}^{\prime}~{}\Gamma~{}m_{2}$ where $m_{1}^{\prime}$ is an extended memory in the form of ${m_{1}}\uplus({\gamma})$.

Definition 0 ($\Gamma$-Relations).

Two memories $m_{1}^{\prime}$ (in the form of ${{m}_{1}}\uplus({\gamma})$) and ${{m}}_{2}$ are related by $\Gamma^{\circ}$, written $m_{1}^{\prime}~{}\Gamma^{\circ}~{}{{m}}_{2}$, if $\forall x\in\text{\em Vars}\cup\text{\em RVars}$, we have

[TABLE]

We define the relation on non-numerical types and the $\Gamma^{\dagger}$ relation in a similar way.

By the definition above, $\Gamma^{\circ}$ introduces a function from ${\mathcal{M}}^{\prime}$ to ${\mathcal{M}}$. Hence, we use $\Gamma^{\circ}m_{1}^{\prime}$ as the unique $m_{2}$ such that $m_{1}^{\prime}~{}\Gamma^{\circ}~{}m_{2}$. The $\Gamma^{\dagger}$ counterparts are defined similarly.

Injectivity

For alignment-based proofs, given any $\gamma$, both $\Gamma^{\circ}$ and $\Gamma^{\dagger}$ must be injective functions (Zhang and Kifer, 2017). The injectivity of $\Gamma$ over the entire memory follows from the injectivity of $\Gamma$ over the random noises $\eta\in\text{\em RVars}$, which is checked as the following requirement in Rule (T-Laplace):

[TABLE]

where all variables are universally quantified. Intuitively, this is true since the non-determinism of the program is purely from that of $\eta\in\text{\em RVars}$.

Lemma 0 (Injectivity).

Given $c,c^{\prime},pc,m^{\prime},m_{1}^{\prime},m_{2}^{\prime},\Gamma_{1},\Gamma_{2}$ such that $pc\vdash{\Gamma_{1}}\{c\rightharpoonup c^{\prime}\}{\Gamma_{2}}$, $\llbracket{c^{\prime}}\rrbracket_{m^{\prime}}{m_{1}^{\prime}}\not=0\land\llbracket{c^{\prime}}\rrbracket_{m^{\prime}}{m_{2}^{\prime}}\not=0,\star\in\{\circ,\dagger\}$, then we have

[TABLE]

Soundness

The soundness theorem connects the “privacy cost” of the probabilistic program to the distinguished variable ${\mathbf{v}_{{\epsilon}}}$ in the target program $c^{\prime\prime}$. To formalize the connection, we first extend memory one more time to include ${\mathbf{v}_{{\epsilon}}}$:

Definition 0.

For any extended memory $m^{\prime}$ and constant $\epsilon$, there is an extension of $m^{\prime}$, written ${m^{\prime}}\uplus({\epsilon})$, so that

[TABLE]

For a transformed program and a pair of initial and final memories $m_{1}^{\prime}$ and $m_{2}^{\prime}$, we identify a set of possible ${\mathbf{v}_{{\epsilon}}}$ values, so that in the corresponding executions of $c^{\prime\prime}$, the initial and final memories are extensions of $m_{1}^{\prime}$ and $m_{2}^{\prime}$ respectively:

Definition 0.

Given $c^{\prime}\rightrightarrows c^{\prime\prime}$, $m_{1}^{\prime}$ and $m_{2}^{\prime}$, the consistent costs of executing $c^{\prime\prime}$ w.r.t. $m_{1}^{\prime}$ and $m_{2}^{\prime}$, written ${c^{\prime\prime}}\upharpoonright^{m_{2}^{\prime}}_{m_{1}^{\prime}}$, is defined as

[TABLE]

Since $({c^{\prime\prime}}\upharpoonright^{m_{2}^{\prime}}_{m_{1}^{\prime}})$ by definition is a set of values of ${\mathbf{v}_{{\epsilon}}}$, we write $\max({c^{\prime\prime}}\upharpoonright^{m_{2}^{\prime}}_{m_{1}^{\prime}})$ for the maximum cost.

The next lemma enables precise reasoning of privacy cost w.r.t. a pair of initial and final memories:

Lemma 0 (Pointwise Soundness).

Let $pc,c,c^{\prime},c^{\prime\prime},\Gamma_{1},\Gamma_{2}$ be such that $pc\vdash{\Gamma_{1}}\{c\rightharpoonup c^{\prime}\}{\Gamma_{2}}~{}\land~{}c^{\prime}\rightrightarrows c^{\prime\prime}$, then $\forall m_{1}^{\prime},m_{2}^{\prime}$:

• (i)

the following holds:

[TABLE]

• (ii)

one of the following holds:

[TABLE]

The point-wise soundness lemma provides a precise privacy bound per initial and final memory. However, differential privacy by definition (Definition 1) bounds the worst-case cost. To close the gap, we define the worst-case cost of the transformed program.

Definition 0.

For any program $c^{\prime\prime}$ in the target language, we say the execution cost of $c^{\prime\prime}$ is bounded by some constants $\epsilon$, written $c^{\prime\prime\preceq\epsilon}$, iff for any $m_{1}^{\prime},m_{2}^{\prime}$,

[TABLE]

Note that off-the-shelf tools can be used to verify that $c^{\prime\prime\preceq\epsilon}$ holds for some $\epsilon$.

Theorem 9 (Soundness).

Given $c,c^{\prime},c^{\prime\prime},m_{1}^{\prime},\Gamma_{1},\Gamma_{2},\epsilon$ such that $\bot\!\vdash\!\Gamma_{1}\{c\!\rightharpoonup\!c^{\prime}\}\Gamma_{2}~{}\land~{}c^{\prime}\!\rightrightarrows\!c^{\prime\prime}~{}\land~{}c^{\prime\prime\preceq\epsilon}$, one of the following holds:

[TABLE]

Proof.

By definition of $c^{\prime\prime\preceq\epsilon}$, we have ${\max({c^{\prime\prime}}\upharpoonright^{m_{2}^{\prime}}_{m_{1}^{\prime}})}\leq\epsilon$ for all $m_{2}^{\prime}\in S$. Thus, by Lemma 7, we have one of the two:

[TABLE]

[TABLE]

If the first inequality is true, then

[TABLE]

and therefore (3a) holds. Similarly, (3b) holds if the second inequality is true. Note that the equality above holds due to the injective assumption, which allows us to derive the set-based privacy from the point-wise privacy (Lemma 7). ∎

We now prove the main theorem on differential privacy:

Theorem 10 (Privacy).

Given $\Gamma_{1},\Gamma_{2},c,c^{\prime},c^{\prime\prime},e,\epsilon$ such that $\Gamma_{1}^{\circ}=\Gamma_{1}^{\dagger}\land\bot\vdash\Gamma_{1}\{(c;\mathtt{return}~{}{~{}}e)\rightharpoonup(c^{\prime};\mathtt{return}~{}{~{}}e)\}\Gamma_{2}~{}\land~{}c^{\prime}\rightrightarrows c^{\prime\prime}$, we have

[TABLE]

Proof.

By the typing rule, we have $\bot\vdash\Gamma_{1}\{c\rightharpoonup c^{\prime}\}\Gamma_{2}$. By the soundness theorem (Theorem 9) and the fact that $\Gamma^{\circ}_{1}=\Gamma^{\dagger}_{2}$, we have $\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(S)\leq\exp(\epsilon)\llbracket{c}\rrbracket_{{\Gamma_{1}^{\circ}}{m_{1}^{\prime}}}({\Gamma_{2}^{\circ}}{S})$. For clarity, we stress that all sets are over distinct elements (as we have assumed throughout this paper).

By rule (T-Return), $\Gamma_{2}\vdash e:\mathtt{num}_{\langle{0},{{\mathbb{d}}}\rangle}$ or $\Gamma_{2}\vdash e:\mathtt{bool}$. For any set of values $V\subseteq\llbracket{\mathcal{B}}\rrbracket$, let $S_{V}^{\prime}=\{m^{\prime}\in\mathcal{M}^{\prime}\mid\llbracket{e}\rrbracket_{m^{\prime}}\in V\}$ and $S_{V}=\{m\in\mathcal{M}\mid\llbracket{e}\rrbracket_{m}\in V\}$, then we have $\Gamma_{2}^{\circ}{S}_{V}^{\prime}\subseteq S_{V}$:

[TABLE]

The equality in second implication is due to the zero distance when $\Gamma_{2}\vdash e:\mathtt{num}_{\langle{0},{{\mathbb{n}}}\rangle}$, and rule (T-ODot) when $\Gamma_{2}\vdash e:\mathtt{bool}$. We note that $\Gamma_{2}^{\circ}{S}_{V}^{\prime}\not=S_{V}$ in general since $\Gamma_{2}^{\circ}$ might not be a surjection. Let $P^{\prime}=(c^{\prime};\mathtt{return}~{}{~{}}e)$, then for any $\gamma$, we have

[TABLE]

Finally, due to Lemma 2, $\llbracket{P}\rrbracket_{m_{1}}(V)=\llbracket{P^{\prime}}\rrbracket_{{m_{1}}\uplus({\gamma})}(V)$. Therefore, by definition of privacy $c$ is $\epsilon$-differentially private. ∎

Note that the shallow distances are only useful for proofs; they are irrelevant to the differential privacy property being obeyed by a program. Hence, initially, we have $\Gamma^{\circ}_{1}=\Gamma^{\dagger}_{1}$ (both describing the adjacency requirement) in Theorem 2, as well as in all of the examples formally verified by ShadowDP.

6. Implementation and Evaluation

6.1. Implementation

We have implemented ShadowDP into a trans-compiler333Publicly available at https://github.com/cmla-psu/shadowdp. in Python. ShadowDP currently supports trans-compilation from annotated C code to target C code. Its workflow includes two phases: transformation and verification. The annotated source code will be checked and transformed by ShadowDP; the transformed code is further sent to a verifier.

Transformation

As explained in Section 4, ShadowDP tracks the typing environments in a flow-sensitive way, and instruments corresponding statements when appropriate. Moreover, ShadowDP adds an assertion $\mathtt{assert}~{}({\mathbf{v}_{{\epsilon}}}\leq\epsilon)$ before the $\mathtt{return}$ command. This assertion specifies the final goal of proving differential privacy. The implementation follows the typing rules explained in Section 4.

Verification

The goal of verification is to prove the assertion $\mathtt{assert}~{}({\mathbf{v}_{{\epsilon}}}\leq\epsilon)$ never fails for any possible inputs that satisfy the precondition (i.e., the adjacency requirement). To demonstrate the usefulness of the transformed programs, we use a model checker CPAChecker (Beyer and Keremoglu, 2011) v1.8. CPAChecker is capable of automatically verifying C program with a given configuration. In our implementation, predicate analysis is used. Also, CPAChecker has multiple solver backends such as MathSat (Cimatti et al., 2013), Z3 (De Moura and Bjørner, 2008) and SMTInterpol (Christ et al., 2012). For the best performance, we concurrently use different solvers and return the results as soon as any one of them verifies the program.

One limitation of CPAChecker and many other tools, is the limited support for non-linear arithmetics. For programs with non-linear arithmetics, we take two approaches. First, we verify the algorithm variants where $\epsilon$ is fixed (the approach taken in (Albarghouthi and Hsu, 2017)). In this case, all transformed code in our evaluation is directly verified without any modification. Second, to verify the correctness of algorithms with arbitrary $\epsilon$, we slightly rewrite the non-linear part in a linear way or provide loop invariants (see Section 6.2.2). We report the results from both cases whenever we encounter this issue.

6.2. Case Studies

We investigate some interesting differentially private algorithms that are formally verified by ShadowDP. We only present the most interesting programs in this section; the rest are provided in the Appendix.

6.2.1. Sparse Vector Technique

Sparse Vector Technique (Dwork et al., 2014) is a powerful mechanism which has been proven to satisfy $\epsilon$-differential privacy (its proof is notoriously tricky to write manually (Lyu et al., 2017)). In this section we show how ShadowDP verifies this algorithm and later show how a novel variant is verified.

Figure 6 shows the pseudo code of Sparse Vector Technique (Dwork et al., 2014). It examines the input queries and reports whether each query is above or below a threshold $T$.

To achieve differential privacy, it first adds Laplace noise to the threshold $T$, compares the noisy query answer $q[i]+\eta_{2}$ with the noisy threshold ${\tilde{T}}$, and returns the result ($\mathtt{true}$ or $\mathtt{false}$). The number of $\mathtt{true}$’s the algorithm can output is bounded by argument $N$. One key observation is that once the noise has been added to the threshold, outputting $\mathtt{false}$ pays no privacy cost (Dwork et al., 2014). As shown in Figure 6, programmers only have to provide two simple annotations: $\circ\mathbin{,}1$ for $\eta_{1}$ and $\circ\mathbin{,}\Omega\mathbin{?}2:0$ for $\eta_{2}$. Since the selectors in this example only select aligned version of variables, the shadow execution is optimized away (controlled by $pc$ in rule (T-If)). ShadowDP successfully type checks and transforms this algorithm. However, due to a nonlinear loop invariant that CPAChecker fails to infer, it fails to verify the program. With the loop invariant provided manually, the verification succeeds, proving this algorithm satisfies $\epsilon$-differential privacy (we also verified a variant where $\epsilon$ is fixed to $N$ to remove the non-linearity).

6.2.2. Gap Sparse Vector Technique

We now consider a novel variant of Sparse Vector Technique. In this variant, whenever $\mathtt{q[i]}+\eta_{2}\geq{\tilde{T}}$, it outputs the value of the gap $\mathtt{q[i]}+\eta_{2}-{\tilde{T}}$ (how much larger the noisy answer is compared to the noisy threshold). Note that the noisy query value $\mathtt{q[i]}+\eta_{2}$ is reused for both this check and the output (whereas other proposals either (1) draw fresh noise and result in a larger $\epsilon$ (Dwork et al., 2014), or (2) re-use the noise but do not satisfy differential privacy, as noted in (Lyu et al., 2017)). For noisy query values below the noisy threshold, it only outputs $\mathtt{false}$. We call this algorithm GapSparseVector. More specifically, Line 6 in Figure 6 is changed from out := true::out; to the following: out := (q[i] + $\eta_{2}$ - ${\tilde{T}}$)::out;. To the best of our knowledge, the correctness of this variant has not been noticed before. This variant can be easily verified with little changes to the original annotation. One observation is that, to align the out variable, the gap appended to the list must have [math] aligned distance. Thus we change the distance of $\eta_{2}$ from $\Omega\mathbin{?}2\mathbin{:}0$ to $\Omega\mathbin{?}(1-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}):0$, the other part of the annotation remains the same.

ShadowDP successfully type checks and transforms the program. Due to the non-linear arithmetics issue, we rewrite the assignment command ${\mathbf{v}_{{\epsilon}}}\text{ := }{\mathbf{v}_{{\epsilon}}}+(1-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]})\times\epsilon/4N\texttt{;}$ to $\texttt{{assert}}~{}(|1-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}|\leq 2)\text{;}~{}{\mathbf{v}_{{\epsilon}}}\text{ := }{\mathbf{v}_{{\epsilon}}}+2\times\epsilon/4N\texttt{;}$ and provide nonlinear loop invariants; then it is verified (we also verified a variant where $\epsilon$ is fixed to 1).

6.3. Experiments

ShadowDP is evaluated on Report Noisy Max algorithm (Figure 1) along with all the algorithms discussed in Section 6.2, as well as Partial Sum, Prefix Sum and Smart Sum algorithms that are included in the Appendix. For comparison, all the algorithms verified in (Albarghouthi and Hsu, 2017) are included in the experiments (where Sparse Vector Technique is called Above Threshold in (Albarghouthi and Hsu, 2017)). One exception is ExpMech algorithm, since ShadowDP currently lacks a sampling command for Exponential noise. However, as shown in (Zhang and Kifer, 2017), it should be fairly easy to add a noise distribution without affecting the rest of a type system.

Experiments are performed on a Dual $\text{Intel}^{\text{\textregistered}}$ $\text{Xeon}^{\text{\textregistered}}$ E5-2620 v4@2.10GHz CPU machine with 64 GB memory. All algorithms are successfully checked and transformed by ShadowDP and verified by CPAChecker. For programs with non-linear arithmetics, we performed experiments on both solutions discussed in Section 6.2.2. Transformation and verification all finish within 3 seconds, as shown in Table 1, indicating the simplicity of analyzing the transformed program, as well as the practicality of verifying $\epsilon$-differentially private algorithms with ShadowDP.

6.4. Proof Automation

ShadowDP requires two kinds of annotations: (1) function specification and (2) annotation for sampling commands. As most verification tools, (1) is required since it specifies the property being verified. In all of our verified examples, (2) is fairly simple and easy to write. To further improve the usability of ShadowDP, we discuss some heuristics to automatically generate the annotations for sampling commands.

Sampling commands requires two parts of annotation:

1. (1)

Selectors. The selector has two options: aligned ($\circ$) or shadow ($\dagger$), with potential dependence. The heuristic is to enumerate branch conditions. For Report Noisy Max, there is only one branch condition $\Omega$, giving us four possibilities: $\circ\ /\ \dagger\ /\ \Omega\mathbin{?}\circ\mathbin{:}\dagger\ /\ \Omega\mathbin{?}\dagger\mathbin{:}\circ$. 2. (2)

Alignments for the sample. It is often simple arithmetic on a small integer such as 0, 1, 2 or the exact difference of query answers and other program variables. For dependent types, we can also use the heuristic of using branch conditions. For Report Noisy Max, this will discover the correct alignment $\Omega\mathbin{?}2\mathbin{:}0$.

This enables the discovery of all the correct annotations for the algorithm studied in this paper. We leave a systematic study of proof automation as future work.

7. Related Work

Randomness alignment based proofs

The most related work is LightDP (Zhang and Kifer, 2017). ShadowDP is inspired by LightDP in a few aspects, but also with three significant differences. First, ShadowDP supports shadow execution, a key enabling technique for the verification of Report Noisy Max based on standard program semantics. Second, while LightDP has a flow-insensitive type system, ShadowDP is equipped with a flow-sensitive one. The benefit is that the resulting type system is both more expressive and more usable, since only sampling command need annotations. Third, ShadowDP allows extra permissiveness of allowing two related executions to take different branches, which is also crucial in verifying Report Noisy Max. In fact, ShadowDP is strictly more expressive than LightDP: LightDP is a restricted form of ShadowDP where the shadow execution is never used (i.e., when the selector always picks the aligned execution).

Coupling based proofs

The state-of-the-art verifier based on approximate coupling (Albarghouthi and Hsu, 2017) is also able to verify the algorithms we have discussed in this paper. Notably, it is able to automatically verify proofs for algorithms including Report-Noisy-Max and Sparse Vector. However, verifying the transformed program by ShadowDP is significantly easier than verifying the first-order Horn clauses and probabilistic constraints generated by their tool. In fact, ShadowDP verifies all algorithms within 3 seconds while the coupling verifier takes 255 seconds in verifying Smart Sum and 580 seconds in verifying Sparse Vector (excluding proof synthesis time). Also, instead of building the system on customized relational logics to verify differential privacy (Barthe et al., 2012, 2013; Barthe and Olmedo, 2013; Barthe et al., 2016b, a), ShadowDP bases itself on standard program logics, which makes the transformed program re-usable by other program analyses.

Other language-based proofs

Recent work such as Personalized Differential Privacy (PDP) (Ebadi et al., 2015) allows each individual to set its own different privacy level and PDP will satisfy difference privacy regarding the level she sets. PINQ (McSherry, 2009) tracks privacy consumption dynamically on databases and terminate when the privacy budget is exhausted. However, along with other work such as computing bisimulations families for probabilistic automata (Tschantz et al., 2011; Xu et al., 2014), they fail to provide a tight bound on the privacy cost of sophisticated algorithms.

8. Conclusions and Future Work

In this paper we presented ShadowDP, a new language for the verification of differential privacy algorithms. ShadowDP uses shadow execution to generate more flexible randomness alignments that allows it to verify more algorithms, such as Report Noisy Max, than previous work based on randomness alignments. We also used it to verify a novel variant of Sparse Vector that reports the gap between noisy above-threshold queries and the noisy threshold.

Although ShadowDP only involves minimum annotations, one future work is to fully automate the verification using ShadowDP, as sketched in Section 6.4. Another natural next step is to extend ShadowDP to support more noise distributions, enabling it to verify more algorithms such as ExpMech which uses Exponential noise. Furthermore, we plan to investigate other applications of the transformed program. For instance, applying symbolic executors and bug finding tools on the transformed program to construct counterexamples when the original program is buggy.

Acknowledgments

We thank our shepherd Dana Drachsler-Cohen and anonymous PLDI reviewers for their helpful suggestions. This work is funded by NSF awards #1228669, #1702760, #1816282 and #1566411.

Appendix

Appendix A ShadowDP Semantics

Given a distribution $\mu\in\mathbf{Dist}(A)$, its support is defined as $\mathtt{support}(\mu)\triangleq\{a\mid\mu(a)>0\}$. We use $\mathds{1}_{a}$ to represent the degenerate distribution $\mu$ that $\mu(a)=1$ and $\mu(a^{\prime})=0$ if $a^{\prime}\not=a$. Moreover, we define monadic functions $\mathtt{unit}$ and $\mathtt{bind}$ functions to formalize the semantics for commands:

[TABLE]

That is, $\mathtt{unit}$ takes an element in $A$ and returns the Dirac distribution where all mass is assigned to $a$; $\mathtt{bind}$ takes $\mu$, a distribution on $A$, and $f$, a mapping from $A$ to distributions on $B$ (e.g., a conditional distribution of $B$ given $A$), and returns the corresponding marginal distribution on $B$. This monadic view avoids cluttered definitions and proofs when probabilistic programs are involved.

Figure 7 provides the semantics of commands.

Appendix B Constructing Shadow Execution

Figure 8 shows the rule for generating shadow execution expressions as well as aligned execution expressions. Figure 9 shows the rules for generating shadow execution commands. The shadow execution essentially replaces each variables $x$ with their correspondence (i.e., $x+\Gamma(x)$) in $c$, as standard in self-composition construction (Barthe et al., 2004; Terauchi and Aiken, 2005). Compared with standard self-composition, the differences are:

1. (1)

$\llparenthesis{c,\Gamma}\rrparenthesis^{\dagger}$ is not applicable to sampling commands, since if the original execution takes a sample while the shadow execution does not, we are unable to align the sample variable due to different probabilities. 2. (2)

For convenience, we use $x+{\mathbb{n}}^{\dagger}$ where $\Gamma\vdash x:\langle{{\mathbb{n}}^{\circ}},{{\mathbb{n}}^{\dagger}}\rangle$ whenever the shadow value of $x$ is used; correspondingly, we update $\widehat{x}^{\dagger}$ to $v-x$ instead of updating the shadow value of $x$ to some value $v$.

Appendix C Extra Case Studies

In this section, we study extra differentially private algorithms to show the power of ShadowDP. As Section 6.2, the shadow execution part is optimized away when the selectors never use the shadow variables.

C.1. Numerical Sparse Vector Technique

Numerical Sparse Vector Technique (Dwork et al., 2014) is an interesting variant of Sparse Vector Technique which outputs numerical query answers when the query answer is large. To achieve differential privacy, like Sparse Vector Technique, it adds noise to the threshold $T$ and each query answer $\mathtt{q[i]}$; it then tests if the noisy query answer is above the noisy threshold or not. The difference is that Numerical Sparse Vector Technique draws a fresh noise $\eta_{3}$ when the noisy query answer is above the noisy threshold, and then releases $\mathtt{q[i]}+\eta_{3}$ instead of simply releasing $\mathtt{true}$. The pseudo code for this algorithm is shown in Figure 10.

In this algorithm, ShadowDP needs an extra annotation for the new sampling command of $\eta_{3}$. We use the same approach in Gap Sparse Vector Technique for this new sampling command. Recall the observation that we want the final output variable out to have distance $\langle{0},{-}\rangle$, which implies that the numerical query $\mathtt{q[i]}+\eta_{3}$ should have distance $\langle{0},{-}\rangle$. We can deduce that $\eta_{3}$ must have distance $-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}$ inside the branch, thus we write “$\circ,-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}$” for $\eta_{3}$. The rest of the annotations remain the same as standard Sparse Vector Technique.

For the non-linear issue of the verifier, we rewrite the privacy cost assignment from

[TABLE]

[TABLE]

With manual loop invariants provided, CPAChecker successfully verified the rewritten program.

C.2. Partial Sum

We now study an $\epsilon$-differentially private algorithm PartialSum (Figure 11) which simply sums over a list of queries. To achieve differential privacy, it adds noise using Laplace mechanism to the final sum and output the noisy sum. One difference from the examples in Section 6.2 is the adjacency assumption: at most one query answer may differ by 1 as specified in the precondition.

In this example, since the noise is added to the final sum, it makes no difference if we choose the aligned version or shadow version of normal variables (they are both identical to the original execution). To decide the distance of the random variable, we want the final output to have distance $\langle{0},{-}\rangle$, it is easy to deduce that the distance of $\eta$ should be $-\widehat{\mathtt{sum}}^{\circ}$. Adding the annotation $\circ,\ -\widehat{\mathtt{sum}}^{\circ}$ to Line 5 in Figure 11, ShadowDP successfully transforms and verifies the program. Note that since the cost update command ${\mathbf{v}_{{\epsilon}}}:={\mathbf{v}_{{\epsilon}}}+|\widehat{\mathtt{sum}}|\times\epsilon\text{;}$ contains non-linear arithmetic, we carefully rewrite this command to $\mathtt{assert}~{}(|\widehat{\mathtt{sum}}|\leq 1);\ {\mathbf{v}_{{\epsilon}}}:={\mathbf{v}_{{\epsilon}}}+\epsilon;$. ShadowDP is able to type check and verify this algorithm within seconds.

C.3. Smart Sum and Prefix Sum

Another interesting algorithm SmartSum (Chan et al., 2011) has been previously verified (Barthe et al., 2012, 2014) with heavy annotations. We illustrate the power of our type system by showing that this algorithm can be verified with very little annotation burden for the programmers.

This algorithm (Figure 12) is designed to continually release aggregate statistics in a privacy-preserving manner. The annotations are only needed on Line 4 and 9 in Figure 12. We use the same observation as stated in Section 6.2.2, in order to make the aligned distance of the output variable out 0. To do that, we assign distance $-\widehat{\mathtt{sum}}^{\circ}-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}$ to $\eta_{1}$ and $-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}$ to $\eta_{2}$, and use $\circ$ for both random variables. This algorithm is successfully transformed by ShadowDP. However, due to the non-linear issue described in Section 6.1, we change the commands of Line 6 and Line 12 from

[TABLE]

to

⬇

if ($|-\widehat{\mathtt{sum}}^{\circ}-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}|>0$)

$\texttt{{assert}}~{}(|-\widehat{\mathtt{sum}}^{\circ}-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}|\leq 1)\texttt{;}~{}{\mathbf{v}_{{\epsilon}}}:={\mathbf{v}_{{\epsilon}}}+\epsilon$;

if ($|-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}|>0$)

$\texttt{{assert}}~{}(|-\widehat{\mathtt{q}}^{\circ}\mathtt{[i]}|\leq 1)\texttt{;}~{}{\mathbf{v}_{{\epsilon}}}:={\mathbf{v}_{{\epsilon}}}+\epsilon$;

Moreover, one difference of this algorithm is that it satisfies $2\epsilon$-differential privacy (Chan et al., 2011) instead of $\epsilon$-differential privacy, thus the last assertion added to the program is changed to $\mathtt{assert}~{}({\mathbf{v}_{{\epsilon}}}\leq 2\times\epsilon)\mathtt{;}$. With this CPAChecker is able to verify this algorithm.

We also verified a variant of Smart Sum, called Prefix Sum algorithm (Albarghouthi and Hsu, 2017). This algorithm is a simplified and less precise version of Smart Sum, where the else branch is always taken. More specifically, we can get Prefix Sum by removing Lines 3 - 8 from Figure 12. The annotation remains the same for $\eta_{2}$, type checking and transformation follows Smart Sum. Note that Prefix Sum satisfies $\epsilon$-differential privacy, so the last assertion remains unchanged. CPAChecker then verifies the transformed Prefix Sum within 2 seconds.

Appendix D Soundness Proof

We first prove a couple of useful lemmas. Following the same notations as in Section 5, we use $m$ for original memory and $m^{\prime}$ for extended memory with aligned and shadow variables but not the distinguished privacy tracking variable ${\mathbf{v}_{{\epsilon}}}$. Moreover, we assume that memory tracks the entire list of sampled random values at each point.

Lemma 0 (Numerical Expression).

$\forall e,m^{\prime},\Gamma$, such that $\Gamma\vdash e:\mathtt{num}_{\langle{{\mathbb{n}}^{\circ}},{{\mathbb{n}}^{\dagger}}\rangle}$, we have

[TABLE]

[TABLE]

Proof.

Induction on the inference rules.

• •

(T-Num): trivial.

• •

(T-Var): If $\Gamma^{\circ}(x)$ is $*$, ${\mathbb{n}}^{\circ}$ is $\widehat{x}^{\circ}$. By Definition 3, ${\Gamma^{\circ}{m^{\prime}}}(x)=m^{\prime}(x)+m^{\prime}(\widehat{x}^{\circ})$. If $\Gamma^{\circ}(x)={\mathbb{d}}^{\circ}$, ${\mathbb{n}}^{\circ}$ is ${\mathbb{d}}^{\circ}$. Again, we have ${\Gamma^{\circ}{m^{\prime}}}(x)=m^{\prime}(x)+\llbracket{{\mathbb{d}}^{\circ}}\rrbracket_{m^{\prime}}$ by Definition 3. The case for $\Gamma^{\dagger}$ is similar.

• •

(T-OPlus, T-OTimes, T-Ternary, T-Index): by the induction hypothesis (list is treated as a collection of variables of the same type).

∎

Lemma 0 (Boolean Expression).

$\forall e,m^{\prime},\Gamma$, such that $\Gamma\vdash e:\mathtt{bool}$, we have

[TABLE]

Proof.

Induction on the inference rules.

• •

(T-Boolean): trivial.

• •

(T-Var): the special case where ${\mathbb{d}}^{\circ}={\mathbb{d}}^{\dagger}=0$. Result is true by Definition 3.

• •

(T-ODot): by Lemma 1 and induction hypothesis, we have $\llbracket{e_{i}}\rrbracket_{{m}^{\prime}}+\llbracket{{\mathbb{n}}_{i}^{\circ}}\rrbracket_{{m}^{\prime}}=\llbracket{e_{i}}\rrbracket_{\Gamma^{\circ}{m^{\prime}}}$ for $i\in\{1,2\}$. By the assumption of (T-ODot), we have

[TABLE]

The case for $\Gamma^{\dagger}$ is similar.

• •

(T-Ternary, T-Index): by the induction hypothesis.

∎

D.1. Injectivity

We first prove that the type system maintains injectivity.

Lemma 0.

$\forall c,c^{\prime},pc,m^{\prime},m_{1}^{\prime},m_{2}^{\prime},\Gamma_{1},\Gamma_{2}.~{}pc\vdash{\Gamma_{1}}\{c\rightharpoonup c^{\prime}\}{\Gamma_{2}}\land\llbracket{c^{\prime}}\rrbracket_{m^{\prime}}{m_{1}^{\prime}}\not=0\land\llbracket{c^{\prime}}\rrbracket_{m^{\prime}}{m_{2}^{\prime}}\not=0$, then we have

[TABLE]

Proof.

By structural induction on $c$.

• •

Case $\mathtt{skip}$: trivial since it is non-probabilistic.

• •

Case $x:=e$: trivial since it is non-probabilistic.

• •

Case $c_{1};c_{2}$: Let $pc\vdash\Gamma_{1}\{c_{1}\rightharpoonup c_{1}^{\prime}\}\Gamma$, $pc\vdash\Gamma\{c_{2}\rightharpoonup c_{2}^{\prime}\}\Gamma_{2}$. There exists some $m_{3}^{\prime}$ and $m_{4}^{\prime}$ such that

[TABLE]

If $m_{3}^{\prime}=m_{4}^{\prime}$, results is true by the induction hypothesis on $c_{2}^{\prime}$. Otherwise, we have $\exists\eta.~{}\Gamma_{2}^{\star}m_{3}^{\prime}(\eta)\not=\Gamma_{2}^{\star}m_{4}^{\prime}(\eta)$. Hence, $\Gamma_{2}^{\star}m_{1}^{\prime}(\eta)\not=\Gamma_{2}^{\star}m_{2}^{\prime}(\eta)$; contradiction.

• •

Case $\mathtt{if}~{}{e}~{}\mathtt{then}~{}{c_{1}}~{}\mathtt{else}~{}{c_{2}}$: let $pc^{\prime}\vdash\Gamma_{1}\{c_{i}\rightharpoonup c_{i}^{\prime}\}\Gamma_{i}^{\prime}$. By typing rule, we have $\Gamma_{1}^{\prime}\sqcup\Gamma_{2}^{\prime}=\Gamma_{2}$. Given initial memory $m^{\prime}$, both executions take the same branch. Without loss of generality assume $c_{1}$ is executed. Let $\llbracket{c_{1}^{\prime}}\rrbracket_{m^{\prime}}{m_{3}^{\prime}}\not=0$, $\llbracket{c_{1}^{\prime\prime}}\rrbracket_{m_{3}^{\prime}}{m_{1}^{\prime}}\not=0$, $\llbracket{c_{1}^{\prime}}\rrbracket_{m^{\prime}}{m_{4}^{\prime}}\not=0$ and $\llbracket{c_{1}^{\prime\prime}}\rrbracket_{m_{4}^{\prime}}{m_{1}^{\prime}}\not=0$. There are two cases:

1. (1)

$m_{3}^{\prime}=m_{4}^{\prime}$: in this case, $c_{1}^{\prime\prime}$ only changes the value of $x^{\star}$ to ${\mathbb{n}}$ when $\Gamma_{2}(x)=*$ and $\Gamma_{1}^{\prime}(x)={\mathbb{n}}$. Moreover, we have $m_{1}^{\prime}(x^{\star})=\llbracket{{\mathbb{n}}}\rrbracket_{m_{3}^{\prime}}=\llbracket{{\mathbb{n}}}\rrbracket_{m_{4}^{\prime}}=m_{2}^{\prime}(x^{\star})$ for those variables. Hence, $m_{1}^{\prime}=m_{2}^{\prime}$. 2. (2)

$m_{3}^{\prime}\not=m_{4}^{\prime}$: by induction hypothesis, $\exists\eta.~{}m_{3}^{\prime}(\eta)\not=m_{4}^{\prime}(\eta)$. Hence, $m_{1}^{\prime}\not=m_{2}^{\prime}$, and $m_{1}^{\prime}(\eta)\not=m_{2}^{\prime}(\eta)$ for the same $\eta$.

When $pc=\top$, $c^{\prime}$ also includes $c^{\dagger}$. In this case, result still holds after $c^{\dagger}$ since $c^{\dagger}$ is deterministic by construction.

• •

Case $\mathtt{while}~{}{e}~{}\mathtt{do}~{}{c}$: let $pc^{\prime}\vdash\Gamma\sqcup\Gamma_{f}\{c\rightharpoonup c^{\prime}\}\Gamma_{f}$. We proceed by induction on the number of iterations:

1. (1)

$c$ is not executed: $m_{1}^{\prime}=m^{\prime}=m_{2}^{\prime}$. 2. (2)

$c$ is executed $n+1$ times: similar to the $c_{1};c_{2}$ case.

When $pc=\top$, $c^{\prime}$ also includes $c^{\dagger}$. In this case, result still holds after $c^{\dagger}$ since $c^{\dagger}$ is deterministic by construction.

• •

Case $(\eta:=\mathtt{Lap}~{}{~{}};\mathcal{S},{\mathbb{n}}_{\eta})$: if $m_{1}^{\prime}\not=m_{2}^{\prime}$, we know that $m_{1}^{\prime}(\eta)\not=m_{2}^{\prime}(\eta)$ since $c^{\prime}$ only modifies the value of $\eta$. In this case, it must be true that $\Gamma_{2}^{\star}m_{1}^{\prime}(\eta)\not=\Gamma_{2}^{\star}m_{2}^{\prime}(\eta)$: otherwise, $m_{1}^{\prime}=m_{2}^{\prime}$ by the injectivity check in rule (T-Laplace).

∎

Proof of Lemma 4

Proof.

Direct implication of Lemma 3. ∎

D.2. Instrumentation

Next, we show a property offered by the auxiliary function $\Gamma_{1},\Gamma_{2},pc\Rrightarrow c^{\prime}$ used in the typing rules. Intuitively, they allow us to freely switch from one typing environment to another by promoting some variables to star type.

Lemma 0 (Instrumentation).

$\forall pc,\Gamma_{1},\Gamma_{2},c^{\prime}$, if $(\Gamma_{1},\Gamma_{2},pc)\Rrightarrow c^{\prime}$, then for any memory $m_{1}^{\prime}$, there is a unique $m_{2}^{\prime}$ such that $\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})\not=0$ and

[TABLE]

Proof.

By construction, $c^{\prime}$ is deterministic. Hence, there is a unique $m_{2}^{\prime}$ such that $\llbracket{c}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})\not=0$.

Consider any variable $x\in\text{\em Vars}$. By the construction of $c^{\prime}$, we note that $m_{1}^{\prime}(x)=m_{2}^{\prime}(x)$ and $\widehat{x}^{\circ}$ differs in $m_{1}^{\prime}$ and $m_{2}^{\prime}$ only if $\Gamma_{1}^{\circ}(x)={\mathbb{n}}$ and $\Gamma_{2}^{\circ}(x)=*$. In this case, $\Gamma_{1}^{\circ}m_{1}^{\prime}(x)=m_{1}^{\prime}(x)+\llbracket{{\mathbb{n}}}\rrbracket_{m_{1}^{\prime}}=m_{2}^{\prime}(x)+m_{2}^{\prime}(\widehat{x}^{\circ})=\Gamma_{2}^{\circ}m_{2}^{\prime}(x)$. Otherwise, $\Gamma_{1}^{\circ}(x)=\Gamma_{2}^{\circ}(x)$ (since $\Gamma_{1}\sqsubseteq\Gamma_{2}$). When $\Gamma_{1}^{\circ}(x)=\Gamma_{2}^{\circ}(x)=*$, $\Gamma_{1}^{\circ}m_{1}^{\prime}(x)=m_{1}^{\prime}(x)+m_{1}^{\prime}(\widehat{x}^{\circ})=m_{2}^{\prime}(x)+m_{2}^{\prime}(\widehat{x}^{\circ})=\Gamma_{2}^{\circ}m_{2}^{\prime}(x)$. When $\Gamma_{1}^{\circ}(x)=\Gamma_{2}^{\circ}(x)={\mathbb{n}}$ for some ${\mathbb{n}}$, $\Gamma_{1}^{\circ}m_{1}^{\prime}(x)=m_{1}^{\prime}(x)+\llbracket{{\mathbb{n}}}\rrbracket_{m_{1}^{\prime}}=m_{2}^{\prime}(x)+\llbracket{{\mathbb{n}}}\rrbracket_{m_{2}^{\prime}}=\Gamma_{2}^{\circ}m_{2}^{\prime}(x)$.

When $pc=\bot$, the same argument applies to the case of $\Gamma_{1}^{\dagger}m_{1}^{\prime}=\Gamma_{2}^{\dagger}m_{2}^{\prime}$. ∎

D.3. Shadow Execution

Next, we show the main properties related to shadow execution.

Lemma 0.

$\forall e,\Gamma,m^{\prime}$, if $e$ is well-typed under $\Gamma$, we have

[TABLE]

Proof.

By structural induction on the $e$.

• •

$e$ is $r$, $\mathtt{true}$ or $\mathtt{false}$: trivial.

• •

$e$ is $x$: if $\Gamma^{\dagger}(x)=*$ (with base type of $\mathtt{num}$), $\llbracket{\llparenthesis{x,\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m^{\prime}}=m^{\prime}(x)+m^{\prime}(\widehat{x}^{\dagger})=\llbracket{x}\rrbracket_{\Gamma^{\dagger}m^{\prime}}$. When $\Gamma(x)=\mathtt{num}_{\langle{{\mathbb{d}}},{{\mathbb{n}}^{\dagger}}\rangle}$, we have $\llbracket{\llparenthesis{x,\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m^{\prime}}=\llbracket{x+{\mathbb{n}}^{\dagger}}\rrbracket_{m^{\prime}}=m^{\prime}(x)+\llbracket{{\mathbb{n}}^{\dagger}}\rrbracket_{m^{\prime}}=\llbracket{x}\rrbracket_{\Gamma^{\dagger}m^{\prime}}$ (by Lemma 1). Otherwise, $\llbracket{\llparenthesis{x,\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m^{\prime}}=m^{\prime}(x)=\Gamma^{\dagger}m^{\prime}(x)$.

• •

$e$ is $e_{1}~{}\mathtt{op}~{}e_{2}$: by induction hypothesis.

• •

$e$ is $e_{1}[e_{2}]$: By the typing rule (T-Index), $\Gamma\vdash e_{2}:\mathtt{num}_{\langle{0},{0}\rangle}$. Hence, $\llbracket{e_{2}}\rrbracket_{\Gamma^{\dagger}m^{\prime}}=\llbracket{e_{2}}\rrbracket_{m^{\prime}}$ by Lemma 1.

Let $\Gamma\vdash e_{1}:\mathtt{list}~{}\mathtt{num}_{\langle{{\mathbb{d}}},{{\mathbb{d}}^{\dagger}}\rangle}$. When $e_{1}=q$ and ${\mathbb{d}}^{\dagger}=*$, $\llbracket{\llparenthesis{q[e_{2}],\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m^{\prime}}=\llbracket{q[e_{2}]+\widehat{q}^{\dagger}[e_{2}]}\rrbracket_{m^{\prime}}=\llbracket{q[e_{2}]}\rrbracket_{\Gamma^{\dagger}m^{\prime}}$. When ${\mathbb{d}}=*$ and $e_{1}$ is not a variable, $\llbracket{\llparenthesis{e_{1}[e_{2}],\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m^{\prime}}$ is defined as $\llbracket{\llparenthesis{e_{1},\Gamma}\rrparenthesis^{\dagger}[e_{2}]}\rrbracket_{m^{\prime}}$. By induction hypothesis, this is the same as $\llbracket{e_{1}}\rrbracket_{\Gamma^{\dagger}m^{\prime}}\llbracket{[e_{2}]}\rrbracket_{m^{\prime}}=\llbracket{e_{1}[e_{2}]}\rrbracket_{\Gamma^{\dagger}m^{\prime}}$.

When ${\mathbb{d}}={\mathbb{n}}^{\dagger}$, $\llbracket{\llparenthesis{e_{1}[e_{2}],\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m^{\prime}}$ is defined as $\llbracket{e_{1}[e_{2}]+{\mathbb{n}}^{\dagger}}\rrbracket_{m^{\prime}}$, which is the same as $\llbracket{e_{1}[e_{2}]}\rrbracket_{\Gamma^{\dagger}m^{\prime}}$ (by Lemma 1).

Otherwise, result is true by Lemma 2.

• •

$e$ is $e_{1}::e_{2}$ and $\neg e$: by induction hypothesis.

• •

$e$ is $e_{1}?e_{2}\!:\!e_{3}$: by induction hypothesis, we have $\llbracket{\llparenthesis{e_{1},\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m^{\prime}}=\llbracket{e_{1}}\rrbracket_{\Gamma^{\dagger}m^{\prime}}$. Hence, the same element is selected on both ends. Result is true by induction hypothesis.

∎

Next, we show that shadow execution simulates two executions on $\Gamma^{\dagger}$-related memories via two program executions.

Lemma 0 (Shadow Execution).

$\forall c,c^{\dagger},\Gamma.~{}(\forall x\in\mathtt{Asgnd}(c).~{}\Gamma^{\dagger}(x)=*)~{}\land~{}\llparenthesis{c,\Gamma}\rrparenthesis^{\dagger}=c^{\dagger}$, we have

[TABLE]

Proof.

By structural induction on $c$. First, we note that the construction of shadow execution does not apply to sampling instructions. Hence, $c$ and $c^{\dagger}$ fall into the deterministic portion of programs. Therefore, we write $m_{2}=\llbracket{c}\rrbracket_{m_{1}}$ when $m_{2}$ is the unique memory such that $\llbracket{c}\rrbracket_{m_{1}}(m_{2})=1$, and likewise for $c^{\prime}$. Then this lemma can be stated as

[TABLE]

• •

$c$ is $\mathtt{skip}$: we have $m_{1}^{\prime}=m_{2}^{\prime}$ in this case. Hence, $\Gamma^{\dagger}m_{2}^{\prime}=\Gamma^{\dagger}m_{1}^{\prime}=\llbracket{\mathtt{skip}}\rrbracket_{\Gamma^{\dagger}m_{1}^{\prime}}$.

• •

$c$ is $(c_{1};c_{2})$: let $\llparenthesis{c_{1},\Gamma}\rrparenthesis^{\dagger}=c^{\dagger}_{1}$ and $\llparenthesis{c_{2},\Gamma}\rrparenthesis^{\dagger}=c^{\dagger}_{2}$ and $m^{\prime}=\llbracket{c^{\dagger}_{1}}\rrbracket_{m_{1}^{\prime}}$. By induction hypothesis, we have $\Gamma^{\dagger}m^{\prime}=\llbracket{c_{1}}\rrbracket_{\Gamma^{\dagger}m_{1}^{\prime}}$. By language semantics, $m_{2}^{\prime}=\llbracket{c^{\dagger}_{2}}\rrbracket_{m^{\prime}}$. By induction hypothesis, with $\Gamma^{\dagger}$ as both the initial and final environments, we have $\Gamma^{\dagger}m_{2}^{\prime}=\llbracket{c_{2}}\rrbracket_{\Gamma^{\dagger}m^{\prime}}=\llbracket{c_{1};c_{2}}\rrbracket_{\Gamma^{\dagger}m_{1}^{\prime}}$

• •

$c$ is $x:=e$: we have $c^{\dagger}=(\widehat{x}^{\dagger}:=\llparenthesis{e,\Gamma}\rrparenthesis^{\dagger}-x)$ in this case. Moreover, $m_{2}^{\prime}={m_{1}^{\prime}}\{{\llbracket{\llparenthesis{e,\Gamma}\rrparenthesis^{\dagger})-x}\rrbracket_{m_{1}^{\prime}}}/{\widehat{x}^{\dagger}}\}$. By Lemma 5, we have $\llbracket{\llparenthesis{e,\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m_{1}^{\prime}}=\llbracket{e}\rrbracket_{\Gamma^{\dagger}m_{1}^{\prime}}$.

For variable $x$, we know that $\Gamma(x)^{\dagger}=*$ by assumption. So $\Gamma^{\dagger}m_{2}^{\prime}(x)=m_{2}^{\prime}(x)+m_{2}^{\prime}(\widehat{x}^{\dagger})=m_{1}^{\prime}(x)+\llbracket{\llparenthesis{e,\Gamma_{2}}\rrparenthesis^{\dagger}-x}\rrbracket_{m_{1}^{\prime}}=\llbracket{e}\rrbracket_{\Gamma^{\dagger}m_{1}^{\prime}}=\llbracket{x:=e}\rrbracket_{\Gamma^{\dagger}m_{1}^{\prime}}(x)$. For a variable $y$ other than $x$, the result is true since both $c$ and $c^{\dagger}$ do not modify $y$ and $y^{\dagger}$, and $y$’s distances does not change due to the well-formedness check in typing rule (T-Asgn).

• •

$c$ is $\mathtt{if}~{}{e}~{}\mathtt{then}~{}{c_{1}}~{}\mathtt{else}~{}{c_{2}}$: let $\llparenthesis{c_{1},\Gamma}\rrparenthesis^{\dagger}=c_{1}^{\prime}$ and $\llparenthesis{c_{2},\Gamma}\rrparenthesis^{\dagger}=c_{2}^{\prime}$. In this case, $c^{\dagger}=\mathtt{if}~{}{\llparenthesis{e,\Gamma}\rrparenthesis^{\dagger}}~{}\mathtt{then}~{}{c_{1}^{\prime}}~{}\mathtt{else}~{}{c_{2}^{\prime}}$. By Lemma 5, we have $\llbracket{\llparenthesis{e,\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m_{1}}=\llbracket{e}\rrbracket_{\Gamma^{\dagger}m_{1}}$. Hence, both $c$ and $c^{\dagger}$ will take the same branch under $\Gamma^{\dagger}m_{1}^{\prime}$ and $m_{1}^{\prime}$ respectively. The desired results follow from induction hypothesis on $c_{1}$ or $c_{2}$.

• •

$c$ is $\mathtt{while}~{}{e}~{}\mathtt{do}~{}{c}$: again, since $\llbracket{\llparenthesis{e,\Gamma}\rrparenthesis^{\dagger}}\rrbracket_{m_{1}}=\llbracket{e}\rrbracket_{\Gamma^{\dagger}m_{1}}$. The desired result follows from induction on the number of loop iterations.

∎

Next, we show that when $pc=\top$ (i.e., when the shadow execution might diverge), the transformed code does not modify shadow variables and their distances.

Lemma 0 (High PC).

$\forall c,c^{\prime},\Gamma_{1},\Gamma_{2}.~{}\top\vdash{\Gamma_{1}}\{c\rightharpoonup c^{\prime}\}{\Gamma_{2}}$, then we have

1. (1)

$(\forall x\in\mathtt{Asgnd}(c).~{}\Gamma_{2}^{\dagger}(x)=*)\land(\Gamma^{\dagger}_{1}(x)=*\Rightarrow\Gamma_{2}^{\dagger}(x)=*)$** 2. (2)

$\forall m_{1}^{\prime},m_{2}^{\prime}.~{}\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})\not=0\implies\Gamma^{\dagger}_{1}m_{1}^{\prime}=\Gamma^{\dagger}_{2}m_{2}^{\prime}$**

Proof.

By structural induction on $c$.

• •

$c$ is $\mathtt{skip}$: trivial.

• •

$c$ is $x:=e$: When $pc=\top$, $\Gamma^{\dagger}_{2}(x)=*$ by the typing rule. $(\Gamma^{\dagger}_{1}(x)=*\Rightarrow\Gamma_{2}^{\dagger}(x)=*)$ since $\Gamma^{\dagger}_{2}(y)=\Gamma^{\dagger}_{1}(y)$ for $y\neq x$.

In this case, $c^{\prime}$ is defined as $(\widehat{x}^{\dagger}:=x+{\mathbb{n}}^{\dagger}-e;x:=e)$ where $\Gamma_{1}^{\dagger}\vdash x:{\mathbb{n}}^{\dagger}$. By the semantics, we have $m_{2}^{\prime}={{m_{1}^{\prime}}\{{\llbracket{x+{\mathbb{n}}^{\dagger}-e}\rrbracket_{m_{1}^{\prime}}}/{\widehat{x}^{\dagger}}\}}\{{\llbracket{e}\rrbracket_{m_{1}^{\prime}}}/{x}\}$. Hence, $\Gamma_{2}m_{2}^{\prime}(x)=m_{2}^{\prime}(x)+\llbracket{x+{\mathbb{n}}^{\dagger}-e}\rrbracket_{m_{1}^{\prime}}=\llbracket{e}\rrbracket_{m_{1}^{\prime}}+\llbracket{x+{\mathbb{n}}^{\dagger}}\rrbracket_{m_{1}^{\prime}}-\llbracket{e}\rrbracket_{m_{1}^{\prime}}=\Gamma_{1}m_{1}(x)$.

For any $y\not=x$, both its value and its shadow distance do not change (due to the wellformedness check in rule (T-Asgn)). Hence, $\Gamma^{\dagger}_{1}m_{1}^{\prime}(y)=\Gamma^{\dagger}_{2}m_{2}^{\prime}(y)$.

• •

$c$ is $c_{1};c_{2}$: by induction hypothesis.

• •

$c$ is $\mathtt{if}~{}{e}~{}\mathtt{then}~{}{c_{1}}~{}\mathtt{else}~{}{c_{2}}$: when $pc=\top$, we have $c^{\prime}=\mathtt{if}~{}{e}~{}\mathtt{then}~{}{(\mathtt{assert}~{}(e^{\circ});c_{1}^{\prime};c_{1}^{\prime\prime})}~{}\mathtt{else}~{}{(\mathtt{assert}~{}(\neg e^{\circ});c_{2}^{\prime};c_{2}^{\prime\prime}})$. By the induction hypothesis, we know that $c_{1}^{\prime}$ and $c_{2}^{\prime}$ does not modify any shadow variable and their ending typing environments, say $\Gamma_{1}^{\prime},\Gamma_{2}^{\prime}$, satisfy condition 1. Hence, the ending environment $\Gamma_{1}^{\prime}\sqcup\Gamma_{2}^{\prime}$ satisfies condition 1 too.

To show (2), we assume $c_{1}$ is executed without losing generality. Let $m_{3}^{\prime}$ be the memory state between $c_{1}^{\prime}$ and $c_{1}^{\prime\prime}$. By induction hypothesis, $\Gamma^{\dagger}_{1}m_{1}^{\prime}=(\Gamma_{1}^{\prime})^{\dagger}m_{3}^{\prime}$. By the definition of $\Gamma_{i},\Gamma_{1}\sqcup\Gamma_{2},\top\Rrightarrow c_{i}^{\prime\prime}$, $c_{1}^{\prime\prime}$ and $c_{2}^{\prime\prime}$ only modifies $\widehat{x}^{\circ},x\in\text{\em Vars}$. Hence, $\Gamma^{\dagger}_{2}m_{2}^{\prime}=(\Gamma_{1}^{\prime})^{\dagger}m_{3}^{\prime}=\Gamma^{\dagger}_{1}m_{1}^{\prime}$.

• •

$c$ is $\mathtt{while}~{}{e}~{}\mathtt{do}~{}{c^{\prime}}$: by the definition of $\sqcup$ and induction hypothesis, condition 1 holds.

Moreover, by the definition of $\Gamma,\Gamma\sqcup\Gamma_{f},\top\Rrightarrow c_{s}$, $c_{s}$ only modifies $\widehat{x}^{\circ},x\in\text{\em Vars}$. Hence, $\Gamma^{\dagger}_{2}m_{2}^{\prime}=\Gamma^{\dagger}_{1}m_{1}^{\prime}$ by induction on the number of iterations.

• •

$c$ is sampling instruction: does not apply since $pc=\bot$ in the typing rule.

∎

Lemma 0.

$\forall c,c^{\prime},c^{\dagger},\Gamma_{1},\Gamma_{2}.~{}(\forall x\in\mathtt{Asgnd}(c).~{}\Gamma_{2}^{\dagger}(x)=*)\land\llparenthesis{c,\Gamma_{2}}\rrparenthesis^{\dagger}=c^{\dagger}\land c^{\prime}$* is deterministic, and $(\forall m_{1}^{\prime},m_{2}^{\prime}.~{}\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})\not=0\implies\Gamma^{\dagger}m_{1}^{\prime}=\Gamma^{\dagger}m_{2}^{\prime})$, then we have*

[TABLE]

Proof.

$c$ and $c^{\prime}$ are deterministic. Hence, this lemma can be stated as

[TABLE]

Let $m_{3}^{\prime}=\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}$ and $m_{2}^{\prime}=\llbracket{c^{\dagger}}\rrbracket_{m_{3}^{\prime}}$. By assumption, we have $\Gamma^{\dagger}_{2}m_{3}^{\prime}=\Gamma^{\dagger}_{1}m_{1}^{\prime}$. Moreover, by Lemma 6, we have $\Gamma^{\dagger}_{2}m_{2}^{\prime}=\llbracket{c}\rrbracket_{\Gamma^{\dagger}_{2}m_{3}^{\prime}}$. Hence, $\Gamma^{\dagger}_{2}m_{2}^{\prime}=\llbracket{c}\rrbracket_{\Gamma^{\dagger}_{2}m_{3}^{\prime}}=\llbracket{c}\rrbracket_{\Gamma^{\dagger}_{1}m_{1}^{\prime}}$.

∎

D.4. Soundness

Finally, we prove the Pointwise Soundness Lemma.

Proof of Lemma 7

Proof.

By structural induction on $c$. Note that the desired inequalities are trivially true if $\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})=0$. Hence, in the proof we assume that $\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})>0$.

• •

Case $(\mathtt{skip})$: trivial.

• •

Case $(x:=e)$: by (T-Asgn), we have $\max({c^{\prime\prime}}\upharpoonright^{m_{2}^{\prime}}_{m_{1}^{\prime}})=0$. This command is deterministic in the sense that when $\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})\neq 0$, we have $\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})=1$ and $m_{2}^{\prime}={m_{1}^{\prime}}\{{\llbracket{e}\rrbracket_{m_{1}^{\prime}}}/{x}\}$. To prove (1) and (2a), it suffices to show that $\Gamma^{\dagger}_{2}m_{2}^{\prime}={\Gamma^{\dagger}_{1}m_{1}^{\prime}}\{{\llbracket{e}\rrbracket_{\Gamma_{1}^{\dagger}m_{1}^{\prime}}}/{x}\}$ and $\Gamma^{\circ}_{2}m_{2}^{\prime}={\Gamma^{\circ}_{1}m_{1}^{\prime}}\{{\llbracket{e}\rrbracket_{\Gamma^{\circ}_{1}m_{1}^{\prime}}}/{x}\}$. We prove the latter one as the other (given $pc=\bot$) can be shown by a similar argument.

First, we show $\Gamma^{\circ}_{2}m_{2}^{\prime}(x)={\Gamma^{\circ}_{1}m_{1}^{\prime}}\{{\llbracket{e}\rrbracket_{\Gamma^{\circ}_{1}m_{1}^{\prime}}}/{x}\}(x)$. Let $\Gamma_{1}\vdash e:\langle{{\mathbb{n}}^{\circ}},{{\mathbb{n}}^{\dagger}}\rangle$. By the typing rule, we have $\Gamma_{2}^{\circ}(x)={\mathbb{n}}^{\circ}$, and

[TABLE]

The third equality is due to well-formedness, and the forth equality is due to Lemma 1.

Second, we show that $\Gamma^{\circ}_{2}m_{2}^{\prime}(y)={\Gamma^{\circ}_{1}m_{1}^{\prime}}\{{\llbracket{e}\rrbracket_{\Gamma^{\circ}_{1}m_{1}^{\prime}}}/{x}\}(y)$ for $y\neq x$. First, by Rule (T-Asgn), $\Gamma^{\circ}_{2}(y)=\Gamma^{\circ}_{1}(y)$, $m_{1}^{\prime}(y)=m_{2}^{\prime}(y)$ and $m_{1}^{\prime}(\widehat{y}^{\circ})=m_{2}^{\prime}(\widehat{y}^{\circ})$. If $\Gamma^{\circ}_{2}(y)=\Gamma^{\circ}_{1}(y)=*$, $\Gamma^{\circ}_{2}m_{2}^{\prime}(y)=m_{2}^{\prime}(y)+m_{2}^{\prime}(\widehat{y}^{\circ})=m_{1}^{\prime}(y)+m_{1}^{\prime}(\widehat{y}^{\circ})=\Gamma^{\circ}_{1}m_{1}^{\prime}(y)$. If $\Gamma^{\circ}_{2}(y)=\Gamma^{\circ}_{1}(y)={\mathbb{n}}$, $\Gamma^{\circ}_{2}m_{2}^{\prime}(y)=m_{2}^{\prime}(y)+\llbracket{{\mathbb{n}}}\rrbracket_{m_{2}^{\prime}}=m_{1}^{\prime}(y)+\llbracket{{\mathbb{n}}}\rrbracket_{m_{1}^{\prime}}=\Gamma^{\circ}_{1}m_{1}^{\prime}(y)$, where $\llbracket{{\mathbb{n}}}\rrbracket_{m_{2}^{\prime}}=\llbracket{{\mathbb{n}}}\rrbracket_{m_{1}^{\prime}}$ due to well-formedness.

• •

Case $(c_{1};c_{2})$: For any $m_{2}^{\prime}$ such that $\llbracket{c_{1}^{\prime};c_{2}^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})\neq 0$, there exists some $m^{\prime}$ such that

[TABLE]

Let $pc\vdash\Gamma_{1}\{c_{1}\rightharpoonup c_{1}^{\prime}\}\Gamma$, $pc\vdash\Gamma\{c_{2}\rightharpoonup c_{2}^{\prime}\}\Gamma_{2}$ For (1), we have

[TABLE]

Here the second line is by induction hypothesis. The change of variable in the third line is due to Lemma 4.

For (2a) and (2b), let $\epsilon_{1}=\max({c_{1}^{\prime\prime}}\upharpoonright^{m^{\prime}}_{m_{1}^{\prime}})$, $\epsilon_{2}=\max({c_{2}^{\prime\prime}}\upharpoonright^{m_{2}^{\prime}}_{m^{\prime}})$ and $\epsilon=\max({c_{1}^{\prime\prime};c_{2}^{\prime\prime}}\upharpoonright^{m_{2}^{\prime}}_{m_{1}^{\prime}})$. Note that $\epsilon_{1}+\epsilon_{2}\leq\epsilon$ due to the fact that ${m_{2}^{\prime}}\uplus({\epsilon_{1}+\epsilon_{2}})\in\llbracket{c_{1}^{\prime\prime};c_{2}^{\prime\prime}}\rrbracket_{{m_{1}^{\prime}}\uplus({0})}$. By induction hypothesis we have one of the following two cases.

1. (1)

$\llbracket{c_{2}^{\prime}}\rrbracket_{m^{\prime}}(m_{2}^{\prime})\leq\exp(\epsilon_{2})\llbracket{c_{2}}\rrbracket_{\Gamma^{\dagger}m^{\prime}}(\Gamma^{\circ}_{2}m_{2}^{\prime})$. We have

[TABLE]

The first inequality is by induction hypothesis. The change of variable in the third line is again due to Lemma 4. The last line is because $\epsilon_{1}+\epsilon_{2}\leq\epsilon$. 2. (2)

$\llbracket{c_{2}^{\prime}}\rrbracket_{m^{\prime}}(m_{2}^{\prime})\leq\exp(\epsilon_{2})\llbracket{c_{2}}\rrbracket_{\Gamma^{\circ}m^{\prime}}(\Gamma^{\circ}_{2}m_{2}^{\prime})$. By induction hypothesis on $c_{1}$, we have two more cases:

1. (a)

$\llbracket{c_{1}^{\prime}}\rrbracket_{m_{1}^{\prime}}(m^{\prime})\leq\exp(\epsilon_{1})\llbracket{c_{1}}\rrbracket_{m_{1}^{\circ}}(m^{\circ})$. In this case,

[TABLE]

The second line is by induction hypothesis and the fact that $\epsilon_{1}+\epsilon_{2}\leq\epsilon$. The change of variable in the third line is due to Lemma 4. 2. (b)

$\llbracket{c_{1}^{\prime}}\rrbracket_{m_{1}^{\prime}}(m^{\prime})\leq\exp(\epsilon_{1})\llbracket{c_{1}}\rrbracket_{\Gamma^{\dagger}_{1}m_{1}^{\prime}}(\Gamma^{\circ}m^{\prime})$. We have

[TABLE]

by a similar argument as above.

• •

Case $(\mathtt{if}~{}{e}~{}\mathtt{then}~{}{c_{1}}~{}\mathtt{else}~{}{c_{2}})$: If $\Gamma_{1}\vdash e:\mathtt{bool}$, then by Lemma 2 we have $\llbracket{e}\rrbracket_{m_{1}^{\prime}}=\llbracket{e}\rrbracket_{\Gamma^{\circ}_{1}m_{1}^{\prime}}=\llbracket{e}\rrbracket_{\Gamma^{\dagger}_{1}m_{1}^{\prime}}$. Hence, the same branch is taken in all related executions. By rule (T-If), the transformed program is

[TABLE]

and $\Gamma_{1},\Gamma_{1}\sqcup\Gamma_{2},\bot\Rrightarrow c_{1}^{\prime\prime},\quad\Gamma_{2},\Gamma_{1}\sqcup\Gamma_{2},\bot\Rrightarrow c_{2}^{\prime\prime}$. Without loss of generality, suppose that $c_{1}$ is executed in all related executions. By Lemma 4, there is a unique $m^{\prime}$ such that $\llbracket{c_{1}^{\prime}}\rrbracket_{m_{1}^{\prime}}(m^{\prime})\not=0$. By induction hypothesis, we have

[TABLE]

Moreover, by Lemma 4, $\Gamma_{1}^{\dagger}{m}^{\prime}=\Gamma_{1}^{\dagger}{m}_{2}^{\prime}$ and

[TABLE]

Hence, we have

[TABLE]

(2a) or (2b) can be proved in a similar way.

When $\Gamma_{1}\not\vdash e:\mathtt{bool}$, the aligned execution will still take the same branch due to the inserted assertions. Hence, the argument above still holds for (2a) or (2b).

For the shadow execution, we need to prove (1). By rule (T-If), $pc^{\prime}=\top$, and the transformed program is

[TABLE]

By Lemma 7 and the definition of $\Rrightarrow$ under high pc, we have that $\forall m_{1}^{\prime},m_{2}^{\prime}.~{}\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})\neq 0\Rightarrow\Gamma^{\dagger}_{2}m_{1}^{\prime}=\Gamma^{\dagger}_{1}m_{1}^{\prime}$, and $\Gamma_{1}\sqcup\Gamma_{2}(x)=*~{}\forall x\in\mathtt{Asgnd}(c_{1};c_{2})$. Furthermore, the program is deterministic since it type-checks under $\top$. Therefore, $\max({W^{\prime\prime}}\upharpoonright^{m_{2}}_{m_{1}})=0$ and (1) holds by Lemma 8.

• •

Case $(\mathtt{while}~{}{e}~{}\mathtt{do}~{}{c})$: Let $W=\mathtt{while}~{}{e}~{}\mathtt{do}~{}{c}$. If $\Gamma_{1}\vdash e:\mathtt{bool}$, then $\llbracket{e}\rrbracket_{m_{1}^{\prime}}=\llbracket{e}\rrbracket_{\Gamma^{\circ}_{2}m_{1}^{\prime}}=\llbracket{e}\rrbracket_{\Gamma_{2}^{\dagger}m_{1}^{\prime}}$. By rule (T-While) we have $pc^{\prime}=\bot$, $\Gamma_{2}=\Gamma\sqcup\Gamma_{f}$ and the transformed program is

[TABLE]

where $\bot\vdash\Gamma_{1}\sqcup\Gamma_{f}~{}\{c\rightharpoonup c^{\prime}\}~{}\Gamma_{f}$, $(\Gamma_{1},\Gamma_{1}\sqcup\Gamma_{f},\bot)\Rrightarrow c_{s}$ and $(\Gamma_{f},\Gamma_{1}\sqcup\Gamma_{f},\bot)\Rrightarrow c^{\prime\prime}$. We proceed by natural induction on the number of loop iterations (denoted by $i$).

When $i=0$, we have $\llbracket{e}\rrbracket_{m_{1}^{\prime}}=\mathtt{false}$. By the semantics, we have $\llbracket{W^{\prime}}\rrbracket_{m_{1}^{\prime}}=\mathtt{unit}~{}(\llbracket{c_{s}}\rrbracket_{m_{1}^{\prime}})$, $\llbracket{W}\rrbracket_{\Gamma^{\circ}_{1}m_{1}^{\prime}}=\mathtt{unit}~{}(\Gamma^{\circ}_{1}m_{1}^{\prime})$, and $\llbracket{W}\rrbracket_{\Gamma^{\dagger}_{1}m_{1}^{\prime}}=\mathtt{unit}~{}(\Gamma^{\dagger}_{1}m_{1}^{\prime})$. Furthermore, $\max({W^{\prime\prime}}\upharpoonright^{m_{2}}_{m_{1}})=0$. By Lemma 4, $(\Gamma^{\circ}_{1}m_{1}^{\prime})=(\Gamma^{\circ}_{2}(\llbracket{c_{s}}\rrbracket_{m_{1}^{\prime}}))$ and $(\Gamma^{\dagger}_{1}m_{1}^{\prime})=(\Gamma^{\dagger}_{2}(\llbracket{c_{s}}\rrbracket_{m_{1}^{\prime}}))$. So desired result holds.

When $i=j+1>0$, we have $\llbracket{e}\rrbracket_{m_{1}^{\prime}}=\mathtt{true}$. By the semantics, we have $\llbracket{W^{\prime}}\rrbracket_{m_{1}^{\prime}}=\llbracket{c_{s};\underbrace{c^{\prime};c^{\prime\prime};}_{j}c^{\prime};c^{\prime\prime}}\rrbracket_{m_{1}^{\prime}}$ and $\llbracket{W}\rrbracket_{\Gamma_{1}^{\star}m_{1}^{\prime}}=\llbracket{c_{s};\underbrace{c^{\prime};c^{\prime\prime};}_{j}c^{\prime};c^{\prime\prime}}\rrbracket_{\Gamma_{1}^{\star}m_{1}^{\prime}},\star\in\{\circ,\dagger\}$. For any $m^{\prime}$ such that $\llbracket{c_{s};\underbrace{c^{\prime};c^{\prime\prime};}_{j}}\rrbracket_{m_{1}^{\prime}}(m^{\prime})=k_{1}\not=0$ and $\llbracket{c^{\prime};c^{\prime\prime}}\rrbracket_{m^{\prime}}(m_{2}^{\prime})=k_{2}\not=0$, we know that $\llbracket{\underbrace{c}_{j}}\rrbracket_{\Gamma_{1}^{\star}m_{1}^{\prime}}(\Gamma_{2}^{\star}m^{\prime})=k_{1}$. Moreover, there is a unique $m_{3}^{\prime}$ such that $\llbracket{c^{\prime}}\rrbracket_{m^{\prime}}(m_{3}^{\prime})=k_{2}\land\llbracket{c^{\prime\prime}}\rrbracket_{m_{3}^{\prime}}(m_{2}^{\prime})=1$ by Lemma 4. By structural induction on $c$, we have $k_{1}\leq\llbracket{c}\rrbracket_{\Gamma^{\dagger}_{2}m^{\prime}}(\Gamma^{\dagger}_{f}m_{3}^{\prime})$ and either $k_{1}\leq\exp(\max({c^{\prime}}\upharpoonright^{m_{2}^{\prime}}_{m_{1}^{\prime}}))\llbracket{c}\rrbracket_{\Gamma^{\circ}_{2}m^{\prime}}(\Gamma^{\circ}_{f}m_{3}^{\prime})$ or $k_{1}\leq\exp(\max({c^{\prime\prime}}\upharpoonright^{m_{2}^{\prime}}_{m_{1}^{\prime}}))\llbracket{c}\rrbracket_{\Gamma^{\dagger}_{2}m^{\prime}}(\Gamma^{\circ}_{f}m_{3}^{\prime})$. By Lemma 4, $\Gamma_{f}^{\star}m_{3}^{\prime}=\Gamma_{2}^{\star}m_{2}^{\prime}$. Hence, we can replace $\Gamma_{f}$ with $\Gamma_{2}$ in the inequalities. Finally, the desired result holds following the same argument as in the composition case.

Otherwise, by rule (T-While) we have $pc^{\prime}=\top$, $\Gamma_{2}=\Gamma\sqcup\Gamma_{f}$ and the transformed program is $W^{\prime}=c_{s};W^{\prime\prime}$ where

[TABLE]

and $\top\vdash\Gamma_{1}\sqcup\Gamma_{f}~{}\{c\rightharpoonup c^{\prime}\}~{}\Gamma_{f}$, $(\Gamma_{1},\Gamma_{1}\sqcup\Gamma_{f},\top)\Rrightarrow c_{s}$ and $(\Gamma_{f},\Gamma\sqcup\Gamma_{f},\top)\Rrightarrow c^{\prime\prime}$. Since we do not have sampling instructions in this case, the program is deterministic, thus $\max({W^{\prime\prime}}\upharpoonright^{m_{2}}_{m_{1}})=0$. Note that by rule (T-Asgn), $\forall x\in\mathtt{Asgnd}(c)$, $\Gamma^{\dagger}_{f}(x)=*$. Hence, $\Gamma^{\dagger}_{2}(x)=*$ for $x\in\mathtt{Asgnd}(c)$. Morevoer, let $m^{\prime}$ be the unique memory such that $\llbracket{c_{s}}\rrbracket_{m_{1}^{\prime}}(m^{\prime})\not=0$, we have $\Gamma^{\dagger}_{1}m_{1}^{\prime}=\Gamma^{\dagger}_{2}m^{\prime}$ by Lemma 4. Therefore, by Lemmas 7 and 8, we have

[TABLE]

• •

Case $(\eta:=\mathtt{Lap}~{}{~{}};\mathcal{S},{\mathbb{n}}_{\eta})$: let $\mu_{r}$ be the probability density (resp. mass) function of the Laplace (resp. discrete Laplace) distribution with zero mean and scale $r$. Since $\mu_{r}(v)\propto\exp(-|v|/r)$ we have

[TABLE]

When $\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})\neq 0$, we have $m_{2}^{\prime}={m_{1}^{\prime}}\{{\mathtt{v}}/{\eta}\}$ for some constant $\mathtt{v}$, and $\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})=\mu_{r}(\mathtt{v}).$

We first consider the case $\mathcal{S}=\circ$. By (T-Laplace), we have ${\Gamma_{2}}(x)={\Gamma_{1}}(x)$ for $x\neq\eta$, and ${\Gamma_{2}}(\eta)=\langle{{\mathbb{n}}_{\eta}},{0}\rangle$. Therefore, for $x\neq\eta$, we have

[TABLE]

In the second equation, we have $m_{2}^{\prime}(x)=m_{1}^{\prime}(x)$ because $m_{2}={m_{1}}\{{\mathtt{v}}/{\eta}\}$ and $x\neq\eta$. The third equation is due to the well-formedness assumption. Also, $\Gamma^{\dagger}_{2}{m_{2}^{\prime}}(\eta)=m_{2}^{\prime}(\eta)=\mathtt{v}$ since $\Gamma_{2}^{\dagger}(\eta)=0$. Therefore, we have $\Gamma^{\dagger}_{2}{m_{2}^{\prime}}={\Gamma^{\dagger}_{1}{m_{1}^{\prime}}}\{{\mathtt{v}}/{\eta}\}$ and thus $\llbracket{c}\rrbracket_{\Gamma^{\dagger}_{1}{m_{1}^{\prime}}}(\Gamma^{\dagger}_{2}{m_{2}^{\prime}})=\mu_{r}(\mathtt{v})=\llbracket{c^{\prime}}\rrbracket_{m_{1}^{\prime}}(m_{2}^{\prime})$.

Similarly, we can show that $\Gamma^{\circ}_{2}{m_{2}^{\prime}}={\Gamma^{\circ}_{1}{m_{1}^{\prime}}}\{{\mathtt{v}+\mathtt{d}}/{\eta}\}$ and therefore $\llbracket{c}\rrbracket_{\Gamma^{\circ}_{1}{m_{1}^{\prime}}}(\Gamma^{\circ}_{2}{m_{2}^{\prime}})=\mu_{r}(\mathtt{v}+\mathtt{d})$. Furthermore, since ${\mathbf{v}_{{\epsilon}}}:={\mathbf{v}_{{\epsilon}}}+|{\mathbb{n}}_{\eta}|/r$, the set $({c^{\prime\prime}}\upharpoonright^{m_{2}}_{m_{1}})$ contains a single element $\llbracket{|{\mathbb{n}}_{\eta}|/r}\rrbracket_{m_{2}}=|\mathtt{d}|/r$, and thus $\max({c^{\prime\prime}}\upharpoonright^{m_{2}}_{m_{1}})=|\mathtt{d}|/r$. Therefore, we have

[TABLE]

The second inequality is due to (4). Thus (1) and (2a) hold.

Next consider the case $\mathcal{S}=\dagger$. By the typing rule, we have $\Gamma_{2}^{\circ}(x)=\Gamma_{2}^{\dagger}(x)=\Gamma_{1}^{\dagger}(x)$ for $x\neq\eta$, and ${\Gamma_{2}}(\eta)=\langle{{\mathbb{n}}_{\eta}},{0}\rangle$. By a similar argument we have $\Gamma^{\dagger}_{2}{m_{2}^{\prime}}={\Gamma^{\dagger}_{1}{m_{1}^{\prime}}}\{{\mathtt{v}}/{\eta}\}$ and $\Gamma^{\circ}_{2}{m_{2}^{\prime}}={\Gamma^{\dagger}_{1}{m_{1}^{\prime}}}\{{\mathtt{v}+\mathtt{d}}/{\eta}\}$. Furthermore, since ${\mathbf{v}_{{\epsilon}}}:=0+|{\mathbb{n}}_{\eta}|/r$, we have $\max({c^{\prime\prime}}\upharpoonright^{m_{2}^{\prime}}_{m_{1}^{\prime}})=|\mathtt{d}|/r$. Therefore, we have

[TABLE]

Thus (1) and (2b) hold.

Finally, consider $\mathcal{S}=e\ ?\ \mathcal{S}_{1}:\mathcal{S}_{2}$. For any $m_{1}^{\prime}$, we have $\mathcal{S}=\mathcal{S}_{1}$ if $\llbracket{e}\rrbracket_{m_{1}^{\prime}}=\mathtt{true}$ and $\mathcal{S}=\mathcal{S}_{2}$ if $\llbracket{e}\rrbracket_{m_{1}^{\prime}}=\mathtt{false}$. By induction, $\mathcal{S}$ evaluates to either $\circ$ or $\dagger$ under $m_{1}^{\prime}$. Thus the proof follows from the the two base cases above.

∎

Appendix E Formal Semantics for the Target Language

The denotational semantics interprets a command $c$ in the target language as a function $\llbracket{c}\rrbracket:\mathcal{M}\rightarrow\mathcal{P}(\mathcal{M})$. The semantics of commands are formalized as follows.

[TABLE]