key: cord-0060420-h3iqf7ee authors: Farina, Gian Pietro; Chong, Stephen; Gaboardi, Marco title: Coupled Relational Symbolic Execution for Differential Privacy date: 2021-03-23 journal: Programming Languages and Systems DOI: 10.1007/978-3-030-72019-3_8 sha: f08eb1a0d6242028583600db4d0406f36d81ef75 doc_id: 60420 cord_uid: h3iqf7ee Differential privacy is a de facto standard in data privacy with applications in the private and public sectors. Most of the techniques that achieve differential privacy are based on a judicious use of randomness. However, reasoning about randomized programs is difficult and error prone. For this reason, several techniques have been recently proposed to support designer in proving programs differentially private or in finding violations to it. In this work we propose a technique based on symbolic execution for reasoning about differential privacy. Symbolic execution is a classic technique used for testing, counterexample generation and to prove absence of bugs. Here we use symbolic execution to support these tasks specifically for differential privacy. To achieve this goal, we design a relational symbolic execution technique which supports reasoning about probabilistic coupling, a formal notion that has been shown useful to structure proofs of differential privacy. We show how our technique can be used to both verify and find violations to differential privacy. Differential Privacy [8] has become a de facto gold standard definition of privacy for statistical analysis. This success is mostly due to the generality of the definition, its robustness and compositionality. However, getting differential privacy right in practice is a hard task. Even privacy experts have released fragile code subject to attacks [13, 17] and published incorrect algorithms [16] . This challenge has motivated the development of techniques to support programmers to show their algorithms differentially private. Among the techniques that have been proposed there are type systems [12, 18, 20, 24, 26] , methods based on model checking and program analysis [2, 15, 22, 23] , and program logics [3, 4, 21] . Several works have also focused on developing techniques to find violations to differential privacy [2, 5, 6, 23, 27] . Most of these works focus only on either verifying a program differentially private or finding violations. Exceptions are the recent works by Barthe et al. [2] and Wang et al. [23] (developed concurrently to our work) which propose method that can instead address both. Motivated by this picture, we propose a new technique named Coupled Relational Symbolic Execution (CRSE), which supports proving and finding violation to differential privacy. Our technique is based on two essential ingredients: relational symbolic execution [10] and approximate probabilistic couplings [3] . Symbolic execution is a classic technique used for bug finding, testing and proving. In symbolic execution an evaluator executes the program which consumes symbolic inputs instead of concrete ones. The evaluator follows, potentially, all the execution paths the program could take and collects constraints over the symbolic values, corresponding to these paths. Similarly, in relational symbolic execution [10] (RSE) one is concerned with bug finding, testing, or proving for relational properties. These are properties about two executions of two potentially different programs. RSE executes two potentially different programs in a symbolic fashion and exploits relational assumptions about the inputs or the programs in order to reduce the number of states to analyze. This is effective when the codes of the two programs share some similarities, and when the property under consideration is relational in nature, as in the case of differential privacy. Probabilistic coupling is a proof technique useful to lift a relation over the support of a joint distribution to a relation over the two probability marginals of the joint. This allows one to reason about relations between probability distributions by reasoning about relations on their support, which can be usually done in a symbolic way. In this approach the actual probabilistic reasoning is confined to the soundness of the verification system, rather than being spread everywhere in the verification effort. A relaxation of the notion of coupling, called approximate probabilistic coupling [3, 4] , has been designed to reason about differential privacy. This can be seen as a regular probabilistic coupling with some additional parameters describing how close the two probability distribution are. In this work, we combine these two approaches in a framework called Coupled Relational Symbolic Execution. In this framework, a program is executed in a relational and symbolic way. When some probabilistic primitive is executed, CRSE introduces constraints corresponding to the existence of an approximate probabilistic coupling on the output. These constraints are combined with the constraints on the execution traces generated by symbolically and relationally executing other non-probabilistic commands. These combined constraints can be exploited to reduce the number of states to analyze. When the execution is concluded CRSE checks whether there is a coupling between the two outputs, or whether there is some violation to the coupling. We show the soundness of this approach for both proving and refuting differential privacy. However, for finding violations, one cannot reason only symbolically, and since checking a coupling directly can be computationally expensive, we devise several heuristics which can be used to facilitate this task. Using these techniques, CRSE allows one to verify differential privacy for an interesting class of programs, including programs working on countable input and output domains, and to find violations to programs that are not differentially private. CRSE is not a replacement for other techniques that have been proposed for the same task, it should be seen as an additional method to put in the set of tools of the privacy developer which provides a high level of generality. Indeed, by being a totally symbolic technique, it can leverage a plethora of current technologies such as SMT solvers, algebraic solvers, and numeric solvers. Summarizing, the contribution of our work are: -We combine relational symbolic execution and approximate probabilistic coupling in a new technique: Coupled Relational Symbolic Execution. -We show CRSE sound for proving programs differentially private -We devise a set of heuristic -one of them sound, and the others useful -that can help a programmer in finding violations to differential privacy. -We show how CRSE can help in proving and refuting differential privacy for an interesting class of programs Most of the proofs are omitted here, more details can be found in [9, 11] . We will introduce CRSE through three examples of programs showing potential errors in implementations of differentially private algorithms. Informally, a randomized function A over a set of databases D is -differential privacy ( -DP) if it maps two databases D 1 and D 2 that differ for the data of one single individual (denoted D 1 ∼ D 2 ) to output distributions that are indistinguishable up to some value -usually referred to as the privacy budget. This is formalized by requiring that for every D 1 ∼ D 2 and for every u: The smaller the , the more privacy is guaranteed. Input: ∈ R + , x1, x2 ∈ {true, f alse} Precondtion: x1 = x2 Postcondition: o1 = o2 ∧ c ≤ 1: o ← RR (x) 2: return o A standard primitive to achieve differential privacy when the data is a single boolean is randomized response [25] . We will use this (simplified) primitive to give an idea of how CRSE works. This primitive can be actually reduced to the primitives that CRSE uses and so it won't be included in later sections. The primitive RR p (b) takes in input p ∈ ( 1 2 , 1) and a boolean b and it outputs b with probability p, andb with probability 1 − p. By unfolding the definition of differential privacy it is easy to see that this primitive is log[−p/(p − 1)]-DP. This is internalized in CRSE thanks to the the existence of an log[−p/(p−1)]-approximate lifting (Definition 2) of the equality relation = between the distributions RR p (b) and RR p (b). When CRSE executes line 1, it assumes that o 1 = o 2 and it sets a counter c , representing the privacy budget required by the primitive, to log[− −1 ]. In order to check whether this program is actually -DP it will then try to check whether this set of conditions implies the postcondition Ψ ≡ o 1 = o 2 ∧ c ≤ . This implication will fail. Indeed, there are value of , say = 0.7, which give a value of c which is actually greater than . This shows that the user may have confused the parameter with the parameter p that the randomized response primitive takes in input. If the user substituted line 1 with the following p← e 1+e ;o $ ← −RR p (x), then CRSE would have considered the following conditions instead: These conditions would then imply the postcondition Ψ proving the correcteness of the program. The intuition behind this proof is that everytime CRSE executes a random assignment of the form o $ ← −RR p (x), it is allowed to assume that o 1 = o 2 as long as it spends a certain amount of privacy budget, i.e. log[− p p−1 ]. These assumptions are recorded in a set of constraints which is then used to see if it implies the condition that two output variables are equal and the budget spent does not exceed . As a consequence of the definition of approximate lifting, this implies differential privacy (Lemma 2). If this fails, CRSE will provide a counterexample in the form of values for the inputs x 1 , x 2 , , p. Such counterexamples to the postcondition do not necessarily denote a counterxampled to the privacy of the algorithm (as we will see later the logic of couplings which CRSE is based on is not complete w.r.t the differential privacy notion) but only potential candidates, and hence need to be further checked. [7, 14] . Given a numeric threshold, an array of numeric queries of length n, and a dataset, this algorithm returns the index of the first query whose result exceeds the threshold -and potentially it should also return the value of that query. This should be done in a way that preserves differential privacy. To do this in the right way, a program should add noise to the threshold, even if it is not sensitive data, add noise to each query, compare the values, and return the index of the first query for which this comparison succeed. The noise that is usually added is sampled from the Laplace distribution, one of the main primitive in differential privacy. The analysis of this algorithm is rather complex: it uses the noise on the threshold as a way to pay only once for all the queries that are below the threshold, and the noise on the queries to pay for the first and only query that is above the threshold, if any. Due to this complex analysis [16] , this algorithm has been a benchmark for tools for reasoning about differential privacy [2, 3, 26] . Input:t, ∈ R, D ∈ D, q[i] : D → N Output: o : [⊥ i , z, ⊥ n−i−1 ] Precondition: D 1 ∼ D2 ⇒ |q[i](D1) − q[i](D2)| ≤ 1 Postcondition: o1 = o2 ∧ c ≤ 1: o ← ⊥ n ; r ← n + 1 2:t $ ← −lap 2 (t) 3: for (i in 1:n) do 4:ŝ $ ← −lap 4 (q[i](D)) 5: ifŝ >t ∧ r = n + 1 then 6: o[i] ←ŝ; r ← i 7: return o Algorithm 2 has a bug making the (whole) program not differentially private, for values of n greater than 4. The program initializes an array of outputs o to all bottom values, and a variable r to n + 1 which will be used as guard in the main loop. It then adds noise to the threshold, and iterates over all the queries adding noise to their results. If one of the noised-results is above the noisy threshold it saves the value in the array of outputs and updates the value of the guard variable, causing it to exit the main loop. Otherwise it keeps iterating. The bug is returning the value of the noisy query that is above the threshold and not only its index, as done by the instruction in red in line 6 -this is indeed not enough for guaranteeing differential privacy. For n < 5 this program can be shown -differentially private by using the composition property of differential privacy that says that the k-fold composition of -DP programs is k -differentially private (Section 3). However, for n ≥ 5 the more sophisticated analysis we described above fails. The proof principle CRSE will use to try to show this programdifferentially private is to prove the assertion o 1 = ι =⇒ o 2 = ι ∧ c ≤ , for every ι ≤ n -the soundness of this principle has been proved in [3] . That is, CRSE will try to prove the following assertions (which would prove the program -differentially private): While proving the first assertion, CRSE will first couple at line 3 the threshold ast 1 + k 0 =t 2 , for k 0 > 1 where 1 is the sensitivity of the queries, which is needed to guarantee that all the query results below the threshold in one run stay below the threshold in the other run, then, it will increase appropriately the privacy budget by k 0 2 . As a second step it will coupleŝ 1 + k 1 =ŝ 2 in line 4. Now, the only way for the assertion o 1 = [ŝ 1 , ⊥, ⊥] =⇒ o 2 = [ŝ 1 , ⊥, ⊥] to hold, is guaranteeing that bothŝ 1 =ŝ 2 andŝ 1 ≥ t 1 =⇒ŝ 2 ≥ t 2 hold. But these two assertions are not consistent with each other because k 0 ≥ 1. That is, the only way, using these coupling rules, to guarantee that the run on the right follows the same branches of the run on the left (this being necessary for proving the postcondition) is to couple the samplesŝ 1 andŝ 2 so that they are different, this necessarily implying the negation of the postcondition. This would not be the case if we were returning only the index of the query, since we can have that both the queries are above the threshold but return different values. Indeed, by substituting line 7 with o[i] $ ← − the program can be proven -differentially private. So the refuting principle CRSE will use here is the one that finds a trace on the left run such that the only way the right run can be forced to follow it is by making the output variables different. A second example with bug of the above threshold algorithm is shown in Figure 3 . In this example, in the body of the loop, the test is performed between the noisy threshold and the actual value of the query on the database -that is, we don't add noise to the query. CRSE will use for this example another refuting principle based on reachability. In particular, it will vacuously couple the two thresholds at line 1. That is it will not introduce any relation betweent 1 , andt 2 . CRSE will then search for a trace which is satisfiable in the first run but not in the second one. This translates in an output event which has positive probability on the first run but 0 probability in the second one leading to an unbounded privacy loss, and making the algorithm not -differentially private for all finite . Interestingly this unbounded privacy loss can be achieved with just 2 iterations. Let A be a denumerable set, a subdistribution over A is a function μ : A → [0, 1] with weight a∈A μ(a) less or equal than 1. We denote the set of subdistributions over A as sdistr(A). When a subdistribution has weight equal to 1, then we call it a distribution. We denote the set of distributions over A by distr(A). The null subdistribution μ 0 : A → [0, 1] assigns to every element of A mass 0. The Dirac's distribution unit(a) : A → [0, 1], defined for a ∈ A as unit(a)(x) ≡ 1 if x = a, and unit(a)(x) ≡ 0, otherwise. The set of subprobability distributions can be given the structure of a monad, with unit the function unit. We have also a function bind ≡ λμ.λf.λa. b∈O μ(b) · f (b)(a) allowing us to compose subdistributions (as we compose monads). We will use the notion of -divergence Δ (μ 1 , μ 2 ) between two subdistributions μ 1 , μ 2 ∈ sdistr(A) to define approximate coupling, this is defined as: Formally, differential privacy is a property of a probabilistic program: The adjacency relation ∼ over the set of databases D models which pairs of input databases should be indistinguishable to an adversary. In its most classical definition, ∼ relates databases that differ in one record in terms of hamming distance. Differentially private programs can be composed [8] : given programs A 1 and A 2 , respectively 1 and 2 differentially private, their sequential composition The notion of approximate probabilistic coupling is internalized by the notion of approximate lifting [3] . ∈ R, we say that μ 1 , μ 2 are related by the approximate lifting of Ψ , denoted Approximate lifting satisfies the following fundamental property [3] : [3] , finally, casts the Laplace mechanisms in terms of couplings: A is -differentially private w.r.t to ∼ iff A(D 1 )(=) A(D 2 ) for all D 1 ∼ D 2 . The next lemmaLemma 3. Let L v1,b , L v2,b two Laplace random variables with mean v 1 , and v 2 respectively, and scale b. Then L v1,b {(z 1 , z 2 ) | z 1 + k = z 2 ∈ Z × Z} |k+v1−v2| L v2,b , for all k ∈ Z, ≥ 0. In this section we sketch the two CRSE concrete languages, the unary one PFOR and the relational one RPFOR. These will be the basis on which we will design our symbolic languages in the next section. PFOR is a basic FOR-like language with arrays, to represent databases and other data structures, and probabilistic sampling from the Laplace distribution. The full syntax is pretty standard and we fully present it in the extended version [11] . In the following we have a simplified syntax: The set of commands C includes assignments, the skip command, sequencing, branching, and (not showed) array assignments and looping construct. Finally, we also include a primitive instruction x $ ← −lap e2 (e 1 ) to model random sampling from the Laplace distribution. Arithmetic expressions e ∈ E are built out of integers, array accesses and lengths, and elements in X p . The set X p contains values denoting random expressions, that is values coming from a random assignment or arithmetic expressions involving such values. We will use capital letters such as X, Y, . . . to range over X p . The set of values is V ≡ Z ∪ X p . In Figure 2 , we introduce a grammar of constraints for random expressions, where X ranges over X p and n, n 1 , n 2 ∈ Z. The simple constraints in the syntactic categories ra and re record that a random value is either associated with a specific distribution, or that the computation is conditioned on some random expression being greater than 0 or less than or equal than 0. The former constraints, as we will see, come from branching instructions. We treat constraint lists p, p , in Figure 2 as lists of simple constraints and hence, from now on, we will use the infix operators :: and @, respectively, for appending a simple constraint to a constraint and for concatenating two constraints. The symbol [] denotes the empty list of probabilistic constraints. Environments in the set M, or probabilistic memories, map program variables to values in V, and array names to elements in Array ≡ i V i , so the type of a memory m ∈ M is V → V ∪ A → Array. We will distinguish between probabilistic concrete memories in M and concrete memories in the set Probabilistic concrete memories are meant to denote subdistributions over the set of concrete memories M c . The judgments reads as: expression e reduces to the value v and probabilistic constraints p in an environment m with probabilistic concrete constraints p. We omit the rules for this judgment here, but we will present similar rules for the symbolic languages in the next section. Commands are given Figure ( 3) shows a selection of the rules defining this judgment. Most of the rules are self-explanatory so we only describe the ones which are non standard. Rule lap-ass handles the random assignment. It evaluates the mean e 1 and the scale e 2 of the distribution and checks that e 2 actually denotes a positive number. The semantic predicate fresh asserts that the first argument is drawn nondeterministically from the second argument and that it was never used before in the computation. Notice that if one of these two expressions reduces to a probabilistic symbolic value the computation halts. Rule if-true-prob (and if-false-prob) reduces the guard of a branching instruction to a value. If the value is a probabilistic symbolic constraint then it will nondeterministically choose one of the two branches recording the choice made in the list of probabilistic constraints. If instead the value of the guard is a numerical constant it will choose the right branch deterministically using the rules if-false and if-true (not showed). We call a probabilistic concrete configuration of the form m, skip, p final. A set of concrete configurations D is called final and we denote it by Final(D) if all its concrete configurations are final. We will use this predicate even for sets of sets of concrete configurations with the obvious lifted meaning. As clear from the rules a run of a PFOR program can generate many different final concrete configurations. A different judgment of the form D ⇒ c D , where D, D ∈ P(M× C × P ), and in particular its transitive and reflexive closure ( ⇒ * c ), will help us in collecting all the possible final configurations stemming from a computation. We have only one rule that defines this judgment: Rule Sub-distr-step nondeterministically selects a configuration s = m, c, p from D, removes s from it, and adds to D all the configurations s that are reachable from s. In section 3 we defined the notions of lifting, coupling and differential privacy using subdistributions in the form of functions from a set of atomic events to the interval [0, 1]. The semantics of the languages proposed so far though only deal with subdistributions represented as set of concrete probabilistic configurations. We now show how to map the latter to the former. In Figure 4 we define a translation function ( ·; · mp ) and, auxiliary functions as well, between a single probabilistic concrete configuration and a subdistribution defined using the unit(·)/bind(·, ·) constructs. We make use of the constant subdistribution μ 0 which maps every element to mass 0, and is usually referred to as the null subdistribution, also by lap n2 (n 1 )(z) we denote the mass of (discrete version of) the Laplace distribution centered in n 1 with scale n 2 at the point z. The idea of the translation is that we can transform a probabilistic concrete memory m s ∈ M into a distribution over fully concrete memories in M c by ms; p mp = bind( p p , (λso.unit(so(ms)))) [] p = unit([]) X = re :: p p = bind( p p , λso.bind( re re so , λzo.unit(X = zo :: so))) re > 0 :: p p = bind( p p , λso.bind( re re so , λzo.if (zo > 0) then unit(zo) else μ0)) re ≤ 0 :: sampling from the distributions of the probabilistic variables defined in m s in the order they were declared which is specified by the probabilistic path constraints. To do this we first build a substitution for the probabilistic variable which maps them into integers and then we perform the substitution on m s . Given a set of probabilistic concrete memories we can then turn them in a subdistribution by summing up all the translations of the single probabilistic configurations. Indeed, given two subdistributions μ 1 , μ 2 defined over the same set we can always define the subdistribution μ 1 + μ 2 by the mapping (μ 1 + μ 2 )(a) = μ 1 (a) + μ 2 (a). The following Lemma states an equivalence between these two representations of probability subdistributions. The hypothesis of the theorem involve a well-formedness judgment, m p, which has not been specified for lack of space but can be found in the extended version [11] , it deals with well-formedness of the probabilistic path constraint p with respect to the concrete probabilistic memory m. In order to be able to reason about differential privacy we will build on top of PFOR a relational language called RPFOR with a relational semantics dealing with pair of traces. Intuitively, an execution of a single RPFOR program represents the execution of two PFOR programs. Inspired by the approach of [ where v ∈ V r , e, e 1 , e 2 ∈ E, c, c 1 , c 2 ∈ C. Values can now be also pairs of unary values, that is V r ≡ V ∪ V 2 . To define the semantics for RPFOR, we first extend memories to allow program variables to map to pairs of integers, and array variables to map to pairs of arrays. In the following we will use the following projection functions · i for i ∈ {1, 2}, which project, respectively, the first (left) and second (right) elements of a pair construct (i.e., c 1 , and are homomorphic for other constructs. The semantics of expressions in RPFOR is specified through the following judgment m 1 , m 2 , e, p 1 , p 2 ↓ rc v, p 1 , p 2 , where m 1 , m 2 ∈ M, p 1 , p 2 , p 1 , p 2 ∈ P, e ∈ E r , v ∈ V r . Similarly, for commands, we have the following judgment m 1 , m 2 , c, p 1 , p 2 → rc m 1 , m 2 , c , p 1 , p 2 . Again, we use the predicate Final(·) for configurations m 1 , m 2 , c, p 1 , p 2 such that c = skip, and lift the predicate to sets of configurations as well. Intuitively a relational probabilistic concrete configuration m 1 , m 2 , c, p 1 , p 2 denotes a pair of probabilistic concrete states, that is a pair of subdistributions over the space of concrete memories. In Figure 5 a selection of the rules defining the judgments is presented. Most of the rules are quite natural. Notice how branching instructions combine both probabilistic and relational nondeterminism. So, as in the case of PFOR, we collect sets of relational configurations using the judgment R ⇒ rc R with R, R ∈ P(M × M × C r × P × P ), defined by only one rule: This rule picks and remove non deterministically one relational configuration from a set and adds to it all those configurations that are reachable from it. As mentioned before a run of a program in RPFOR corresponds to the execution of two runs the program in PFOR. Before making this precise we extend projection functions to relational configurations in the following way: . Projection functions extend in the obvious way also to sets of relational configurations. We are now ready to state the following lemma relating the execution in RPFOR to the one in PFOR: In this section we lift the concrete languages, presented in the previous section, to their symbolic versions (respectively, SPFOR and SRPFOR) by extending them with symbolic values X ∈ X . We use intentionally the same metavariables for symbolic values in X and X p since they both represent symbolic values of some sort. However, we assume X p ∩ X = ∅ -this is because we want symbolic values in X to denote only unknown sets of integers, rather than sets of probability distributions. So, the meaning of X should then be clear from the context. SPFOR expressions extend PFOR expressions with symbolic values X ∈ X Commands in SPFOR are the same as in PFOR but now symbolic values can appear in expressions. In order to collect constraints on symbolic values we extend configurations with set of constraints over integer values, drawn from the set S (Figure 6a) , not to be confused with probabilistic path constraints (Figure 6b ). The former express constraints over integer values, for instance parameters of the distributions. In particular constraint expressions include standard arithmetic expressions with values being symbolic or integer constants, and array selection. Probabilistic path constraints now can also contain symbolic integer values. Hence, Se e ::= n | X | i | e ⊕ e | |e| store(e, e, e) | select(e, e) S s ::= | e • e | s ∧ s | ¬s | ∀i.s (a) Symbolic constraints. X ∈ X , n ∈ V. sra ::= Y $ ← −lapc e (ce) sre ::= n | X | Y | re ⊕ re SP ::= Y = re | re > 0 | re ≤ 0 | ra (b) Prob. constraints. ce ∈ S, X ∈ X , Y ∈ Xp Fig. 6 : Grammar of constraints probabilistic path constraints now can be symbolic. This is needed to address examples branching on probabilistic values, such as the Above Threshold algorithm we discussed in Section 2. Memories can now contain symbolic values and we represent arrays in memory as pairs (X, v), where v is a (concrete or symbolic) integer value representing the length of the array, and X is a symbolic value representing the array content. The content of the arrays is kept and refined in the set of constraints by means of the select(·, ·) and store(·, ·, ·) operations. The semantics of expressions is captured by the judgment (m, e, p, s) ↓ SP (v, p , s ) including now a set of constraints over integers. The rules of the judgment are fully described in the extended version [11] . We briefly describe a selection of the rules. Rule S-P-Op-2 applies when an arithmetic operation has both of its operands that reduce respectively to elements in X p . Appropriately it updates the set of probabilistic constraints. Rules S-P-Op-5 instead fires when one of them is an integer and the other is a symbolic value. In this case only the list of symbolic constraints needs to be updated. Finally, in rule S-P-Op-6 one of the operands reduces to an element in X p and the other to an element in X . We only update the list of probabilistic constraints appropriately, as integer constraints cannot contain symbols in X p . The semantics of commands of SPFOR is described by small step semantics judgments of the form: (m, c, p, s) → SP (m , c , p , s ), including a set of constraints over integers. We provide a selection of the rules in Figure 7 . Rule S-P-If-sym-true fires when a branching instruction is to be executed and the guard is reduced to either an integer or a value in X , denoted by the set V is . In this case we can proceed with the true branch recording in the set of integer constraints the fact that the guard is greater than 0. Rule S-P-If-prob-false handles a branching instruction which has a guard reducing to a value in X p . In this case we can proceed in both branches, even though here we only show one of the two rules, by recording the conditioning fact on the list of probabilistic constraints. Finally, rule S-P-Lap-Ass handles probabilistic assignment. After having reduced both the expression for the mean and the expression for the scale to values we check that those are both either integers or symbolic integers, if that's the case we make sure that the scale is greater than 0 and we add a probabilistic constraints recording the fact that the modified variable now points to a probabilistic symbolic value related to a Laplace distribution. The semantics of SPFOR has two sources of nondeterminism, from guards which reduce to symbolic values, and from guards which reduce to a probabilistic symbolic value. The collecting semantics of SPFOR, specified by judgments as , that we are using to make the step. Intuitively, s-p-collect starts from a set of configurations and reaches all of those that are reachable from it -all the configurations that have a satisfiable set of constraints and are reachable from one of the original configurations with only one step of the symbolic semantics. Notice that in a set of constraints we can have constraints involving probabilistic symbols, e.g. if the i-th element of an array is associated with a random expression. Nevertheless, the predicate SAT(·) does not need to take into consideration relations involving probabilistic symbolic constraints but only relations involving symbolic values denoting integers. The following lemma of coverage connects PFOR with SPFOR ensuring that a concrete execution is covered by a symbolic one. (m, ea, p, s) ↓SP (va, p , s ) (m, e b , p , s ) ↓SP (v b , p , s ) X fresh(Xp) va, v b ∈ Vis s = s ∪ {v b > 0} p = p @[X $ ← −lapv b (va)] (m, x $ ← −lape b (ea), p, s) →SP (m[x → X], skip, p , s ) The language presented in this section is the the symbolic extension of the concrete language RPFOR. It can also be seen as the relational extension of SPFOR. The key part of this language's semantics will be the handling of the probabilistic assignment. For that construct we will provide 2 rules instead of one. The first one is the obvious one which carries on a standard symbolic probabilistic assignment. The second one will implement a coupling semantics. The syntax of the SRPFOR, presented in Figure 8 , extends the syntax of RPFOR by adding symbolic values. The main change is in the grammar of expressions, while the syntax for commands is almost identical to that of RPFOR. As in the case of RPFOR, only unary symbolic expressions and commands are admitted in the pairing construct. This invariant is maintained by the semantics rules. As for the other languages, we provide a big-step evaluation semantics for expressions whose judgments are of the form (m 1 , m 2 , e, p 1 , p 2 , s) ↓ SRP (v, p 1 , p 2 , s ). The only rule defining the judgment ↓ SRP is S-R-P-Lift and it is presented in the extended version [11] . The rule projects the symbolic relational expression first on the left and evaluates it to a unary symbolic value, potentially updating the probabilistic symbolic constraints and the symbolic constraints. It then does the same projecting the expression on the right but starting from the potentially previously updated constraints. Now, the only case when the value returned is unary is when both the previous evaluation returned equal integers, in all the other cases a pair of values is returned. So, the relational symbolic semantics leverages the unary semantics. For the semantics of commands we use the following evaluation contexts to simplify the exposition: CT X ::= [ · ] | CT X ;c P ::= ·;c|· | ·| · ;c | ·|· | ·;c| · ;c Notice how P gets saturated by pairs of commands. Moreover, we separate commands in two classes. We call synchronizing all the commands in C rs with the following shapes x , since they allow synchronization of two runs using coupling rules. We call non synchronizing all the other commands. We consider judgments of the form (m 1 , m 2 , c, p 1 , p 2 , s) → SRP (m 1 , m 2 , c , p 1 , p 2 , s ) and a selection of the rules is given in Figure 9 . An explanation of the rules follows. Rule s-r-if-prob-probtrue-false fires when evaluating a branching instruction. In particular, it fires when the guard evaluates on both side to a probabilistic symbolic value. In this case the semantics can continue with the true branch on the left run and s-r-if-prob-prob-true-false (m1, m2, e, p1, p2, s) m2, if e then ctt else c ff , p1, p2, s) →SRP (m1, m2, ctt , p 1 , p 2 , s ) m2, skip|skip , p 1 , p2, s ) m2, P(c1, c2) with the false branch on the right one. Notice that commands are projected to avoid pairing commands appearing in a nested form. Rule s-r-if-prob-symtrue-false applies when the guard of a branching instruction evaluates to a probabilistic symbolic value on the left run and a symbolic integer value on the right one. The rule allows to continue on the true branch on the left run and on the false branch on the right one. Notice that in one case the probabilistic list of constraints is updated, while on the other the symbolic set of constraints. Rule s-r-pair-lap-skip handles the pairing command where on the left hand side we have a probabilistic assignment and on the right a skip instruction. In this case, there is no hope for synchronization between the two runs and hence we can just perform the left probabilistic assignment relying on the unary symbolic semantics. Rule s-r-pair-lapleft-sync instead applies when on the left we have a probabilistic assignment and on the right we have another arbitrary command. In this case we can hope to reach a situation where on the right run another probabilistic assignment appears. Hence, it makes sense to continue the computation in a unary way on the right side. Again → SRP is a nondeterministic semantics. The nondeterminism comes from the use of probabilistic symbols and symbolic values as guards, and by the relational approach. So, in order to collect all the possible traces stemming from such nondeterminism we define a collecting semantics relating set of configurations to set of configurations. (m1, x $ ← −lape b (ea), p1, s) →SP (m 1 , skip, p 1 , s ) (m1, m2, x $ ← −lape b (ea)|skip , p1, p2, s) →SRP (m 1 , The semantics is specified through a judgment of the form: SR ⇒ srp SR , with SR, SR ∈ P(M SP × M SP × C rs × SP × SP × S). The only rule defining the judgment is the following natural lifting of the one for the unary semantics. The rule, and the auxiliary notation R [s] , is pretty similar to that of SPFOR, the only difference is that here sets of symbolic relational probabilistic configurations are considered instead of symbolic (unary) probabilistic configurations. We define a new judgment with form G G , with G, G ∈ P(P(M SP × M SP × C rs × SP × SP × S)). In Figure 10 , we give a selection of the rules. Rule Proof-Step-No-Sync applies when no synchronizing commands are involved, and hence there is no possible coupling rule to be applied. In the other rules, we use the variable c to symbolically count the privacy budget in the current relational execution. The variable gets increased when the rule Proof-Step-Lap-Gen fires. This symbolic counter variable is useful when trying to prove equality of certain variables without spending more than a specific budget. This rule is the one we can use in most cases when we need to reason about couplings on the Laplace distributions. In the set of sets of configurations G, a set of configurations, SR, is nondeterministically chosen. Among elements in SR a configuration is also nondeterministically chosen. Using contexts we check that in the selected configuration the next command to execute is the probabilistic assignment. After reducing to values both the mean and scale expression, and verified (that is, assumed in the set of constraints) that in the two runs the scales have the same value, the rule adds to the set of constraints a new element, that is, where K, K , E are fresh symbols denoting integers and E is the symbolic integer to which the budget variable c maps to. Notice that c needs to point to the same symbol in both memories. This is because it is a shared variable tracking the privacy budget spent so far in both runs. This new constraint increases the budget spent. The other constraint added is the real coupling relation, that is X 1 + K = X 2 . Where X 1 , X 2 are fresh in X . Later, K will be existentially quantified in order to search for a proof of -indistinguishability. Rule Proof-Step-Avoc does not use any coupling rule but treats the samples in a purely symbolic manner. It intuitively asserts that the two samples are drawn from the distributions and assigns to them arbitrary integers free to vary on the all domain of the Laplace distribution. Finally, rule Proof-Step-No-Coup applies to synchronizing commands as well. It does not add any relational constraints to the samples. This rules intuitively means that we are not correlating in any way the two samples. Notice that since we are not using any coupling rule we don't need to check that the scale value is the same in the two runs as it is requested in the previous rule. We could think of this as a way to encode the relational semantics of the program in an expression which later can be fed in input to other tools. The main difference with the previous rule is that here we treat the sampling instruction symbolically and that is why the fresh symbols are in X p , denoting subdistributions, rather than in X , denoting sampled integers. When the program involves a synchronizing command we basically fork the execution when it is time to execute it. The set of configurations allow us to explore different paths, one for every rule applicable. The coverage lemma can be extended also to the relational setting. ). This can also be extended to if we consider only the fragment that only uses the rules Proof-Step-No-Sync, and Proof-Step-No-Coupl. The language of relational assertions Φ, Ψ . . . is defined using first order predicate logic formulas involving relational program expressions and logical variables in LogVar. The interpretation of a relational assertions is naturally defined as a subset of M c × M c , the set of pairs of memories modeling the assertion. We will denote by · · the substitution function mapping the variables in an assertion to the values they have in a memory (unary or relational). More details are in [10] . Let Φ, Ψ be relational assertions, c ∈ C r , I : LogVar → R be an interpretation defined on . We say that, Φ yields Ψ through c within under I (and we write I c : , and m I2 are fully symbolic memories, and k = k 1 , k 2 , . . . are the symbols generated by the rules for synchronizing commands. The idea of this definition is to make the proof search automated. When proving differential privacy we will usually consider Ψ as being equality of the output variables in the two runs and Φ as being our preconditions. We can now prove the soundness of our approach. Let c ∈ C r . If I c : We can also prove the soundness of refutations obtained by the semantics. {{{ m 1 , m 2 , c, [] , [], Φ m1|m2 }}} G, and Hs ∈ H ∈ G and, ∃σ |= Z s such that Δ ( c 1 C (σ(m 1 )), c 2 C (σ(m 2 ))) > 0 then c is not differentially private. Lemma 9 is hard to use to find counterexamples in practice. For this reasons we will now describe three strategies that can help in reducing the effort in counterexample finding. These strategies help in isolating traces that could potentially lead to violations. For this we need first some notation. Given a set of constraints s we define the triple Ω = Ω 1 , Ω 2 , C( k) ≡ s 1 , s 2 , s \ ( s 1 ∪ s 2 ) . We sometimes abuse notation and consider Ω also as a set of constraints given by the union of its first, second and third projection, and we will also consider a set of constraints as a single proposition given by the conjunction of its elements. The set C( k) contains relational constraints coming from either preconditions or invariants or, from the rule Proof-Step-Lap-Gen. The potentially empty vector k = K 1 , . . . K n is the set of fresh symbols K generated by that rule. In the rest of the paper we will assume the following simplifying assumption. This assumption allow us to consider only programs for which it is necessary for the output variable on both runs to assume the same value, that the two runs follow the same branches. That is, if the two output differ then the two executions must have, at some point, taken different branches. The following definition will be used to distinguish relational traces which are reachable on one run but not on the other. We call these traces orthogonal. The next definition, instead, will be used to isolate relational traces for which it is not possible that the left one is executed but the right one is not. We call these traces specular. The constraint Ω 1 ∧ C( k) includes all the constraints coming from the left projection's branching of the symbolic execution and all the relational assumptions such as the adjacency condition, and all constraints added by the potentially fired Proof-Step-Lap-Gen rule. A specular trace is such that its left projection constraints plus the relational assumptions imply the right projection constraints. We will now describe our three strategies. Strategy A In this strategy CRSE uses only the rule Proof-Step-Avoc for sampling instructions, also this strategy searches for orthogonal relational traces. Under assumption 1, if this happens for a program then it must be the case that the program can output one value on one run with some probability but the same value has 0 probability of being output on the second run. This implies that for some input the program has an unbounded privacy loss. To implement this strategy CRSE looks for orthogonal relational traces m 1 , m 2 , skip, p 1 , p 2 , Ω such that: ∃σ.σ |= Ω 1 ∧ C( k) but σ |= Ω 2 . Notice that using this strategy k will always be empty, as the rule used for samplings does not introduce any coupling between the two samples. This strategy symbolically executes the program in order to find a specular trace for which no matter how we relate, within the budget, the various pairs of samples X i 1 , X i 2 in the two runs -using the relational schema X i 1 +K i = X i 2 -the postcondition is always false. That is CRSE looks for specular relational traces m 1 , m 2 , skip, p 1 , p 2 , Ω such that: Strategy C This strategy looks for relational traces for which the output variable takes the same value on the two runs but too much of the budget was spent. That is CRSE looks for traces m 1 , m 2 , skip, p 1 , p 2 , Ω such that: Of the presented strategies only strategy A is sound with respect to counterexample finding, while the other two apply when the algorithm cannot be proven differentially private by any combination of the rules. In this second case though, CRSE provides counterexamples which agree with other refutation oriented results in literature. This strategies are hence termed useful because they amount to heuristics that can be applied in some situations. In this section we will review the examples presented in Section 2 and variations thereof to show how CRSE works. Unsafe Laplace mechanism: Algorithm 4. This algorithm is not -d.p because the noise is a constant and it is not calibrated to the sensitivity r of the query q. This translates in any attempt based on coupling rules to use too much of the budget. This program has only one possible final relational trace: m 1 , m 2 , skip, p 1 , p 2 , Ω 1 , C( k, Ω 2 ) . Since there are no branching instructions Intuitively, given this set of constraints, if it has to be the case that can be R and hence, E c is at least R. So, if we want to equate the two output we need to spend r times the budget. Any relational input satisfying the precondition will give us a counterexample, provided the two projections are different. A safe Laplace mechanism. By substituting line 2 in Algorithm 4 with ρ $ ← −lap r * (0) we get an -DP algorithm. Indeed when executing that line CRSE would generate the following constraint Unsafe sparse vector implementation: Algorithm 2. We already discussed why this algorithm is not -differentially private. Algorithm 2 satisfies Assumption 1 because it outputs the whole array o which takes values of the form ⊥ i , t or ⊥ n for 1 ≤ i ≤ n and t ∈ R. The array, hence, encodes the whole trace. So if two runs of the algorithm output the same value it must be the case that they followed the same branching instructions. Let's first notice that the algorithm is trivially differentially private, for any , when the number of iterations n is less than or equal to 4. Indeed it is enough to apply the sequential composition theorem and get the obvious bound CRSE can prove this by applying the rule Proof-Step-Lap-Gen n times, and then choosing K 1 , . . . , K n all equal to 0. This would imply the statement of equality of the output variables spending less than . A potential counterexample can be found in 5 iterations. If we apply strategy B to this algorithm and follow the relational symbolic trace that applies the rule Proof-Step-Lap-Gen for all the samplings we can isolate the relational specular trace shown in Figure 11 , which corresponds to the left execution following the false branch for the first four iterations and then following the true with k j = q[j](D 2 ) − q[j](D 1 ), spending |k j + q[j](D 2 ) − q[j](D 1 )| = 0. So, at the i-th iteration the samples are coupledŝ 1 + k i =ŝ 2 , with k i = 1. So ifŝ 1 ≥t 1 then alsoŝ 2 ≥t 2 , and also, ifŝ 1