An official website of the United States government
Differential privacy is a de facto standard for statistical computations over databases that contain private data. Its main and rather surprising strength is to guarantee individual privacy and yet allow for accurate statistical results. Thanks to its mathematical definition, differential privacy is also a natural target for formal analysis. A broad line of work develops and uses logical methods for proving privacy. A more recent and complementary line of work uses statistical methods for finding privacy violations. Although both lines of work are practically successful, they elide the fundamental question of decidability. This paper studies the decidability of differential privacy. We first establish that checking differential privacy is undecidable even if one restricts to programs having a single Boolean input and a single Boolean output. Then, we define a non-trivial class of programs and provide a decision procedure for checking the differential privacy of a program in this class. Our procedure takes as input a program P parametrized by a privacy budget ϵ and either establishes the differential privacy for all possible values of ϵ or generates a counter-example. In addition, our procedure works for both to ϵ-differential privacy and (ϵ, δ)-differential privacy. Technically, the decision procedure is based on a novel and judicious encoding of the semantics of programs in our class into a decidable fragment of the first-order theory of the reals with exponentiation. We implement our procedure and use it for (dis)proving privacy bounds for many well-known examples, including randomized response, histogram, report noisy max and sparse vector.
more »
« less
Witnessability of Undecidable Problems
Many problems in programming language theory and formal methods are undecidable, so they cannot be solved precisely. Practical techniques for dealing with undecidable problems are often based on decidable approximations. Undecidability implies that those approximations are always imprecise. Typically, practitioners use heuristics andad hocreasoning to identify imprecision issues and improve approximations, but there is a lack of computability-theoretic foundations about whether those efforts can succeed. This paper shows a surprising interplay between undecidability and decidable approximations: there exists a class of undecidable problems, such that it is computable to transform any decidable approximation to a witness input demonstrating its imprecision. We call those undecidable problemswitnessable problems. For example, if a program propertyPis witnessable, then there exists a computable functionfP, such thatfPtakes as input the code of any program analyzer targetingPand produces an input programwon which the program analyzer is imprecise. An even more surprising fact is that the class of witnessable problems includes almost all undecidable problems in programming language theory and formal methods. Specifically, we prove the diagonal halting problemKis witnessable, and the class of witnessable problems is closed under complements and many-one reductions. In particular, all “non-trivial semantic properties of programs” mentioned in Rice’s theorem are witnessable. We also explicitly construct a problem in the non-witnessable (and undecidable) class and show that both classes have cardinality 2ℵ0. Our results offer a new perspective on the understanding of undecidability: for witnessable problems, although it is impossible to solve them precisely, it is always possible to improve any decidable approximation to make it closer to the precise solution. This fact formally demonstrates that research efforts on such approximations are promising and shows there exist universal ways to identify precision issues of program analyzers, program verifiers, SMT solvers, etc., because their essences are decidable approximations of witnessable problems.
more »
« less
- Award ID(s):
- 1917924
- PAR ID:
- 10472620
- Publisher / Repository:
- ACM
- Date Published:
- Journal Name:
- Proceedings of the ACM on Programming Languages
- Volume:
- 7
- Issue:
- POPL
- ISSN:
- 2475-1421
- Page Range / eLocation ID:
- 982 to 1002
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Differential privacy is a mathematical framework for developing statistical computations with provable guarantees of privacy and accuracy. In contrast to the privacy component of differential privacy, which has a clear mathematical and intuitive meaning, the accuracy component of differential privacy does not have a generally accepted definition; accuracy claims of differential privacy algorithms vary from algorithm to algorithm and are not instantiations of a general definition. We identify program discontinuity as a common theme in existingad hocdefinitions and introduce an alternative notion of accuracy parametrized by, what we call, — the of an inputxw.r.t. a deterministic computationfand a distanced, is the minimal distanced(x,y) over allysuch thatf(y)≠f(x). We show that our notion of accuracy subsumes the definition used in theoretical computer science, and captures known accuracy claims for differential privacy algorithms. In fact, our general notion of accuracy helps us prove better claims in some cases. Next, we study the decidability of accuracy. We first show that accuracy is in general undecidable. Then, we define a non-trivial class of probabilistic computations for which accuracy is decidable (unconditionally, or assuming Schanuel’s conjecture). We implement our decision procedure and experimentally evaluate the effectiveness of our approach for generating proofs or counterexamples of accuracy for common algorithms from the literature.more » « less
-
Many program analyses need to reason about pairs of matching actions, such as call/return, lock/unlock, or set-field/get-field. The family of Dyck languages {Dk}, whereDkhaskkinds of parenthesis pairs, can be used to model matching actions as balanced parentheses. Consequently, many program-analysis problems can be formulated as Dyck-reachability problems on edge-labeled digraphs.Interleaved Dyck-reachability(InterDyck-reachability), denoted byDk⊙Dk-reachability, is a natural extension of Dyck-reachability that allows one to formulate program-analysis problems that involvemultiplekinds of matching-action pairs. Unfortunately, the general InterDyck-reachability problem is undecidable. In this paper, we study variants of InterDyck-reachability onbidirected graphs, where for each edge ⟨p,q⟩ labeled by an open parenthesis ”(a”, there is an edge ⟨q,p⟩ labeled by the corresponding close parenthesis ”)a”, andvice versa. Language-reachability on a bidirected graph has proven to be useful both (1) in its own right, as a way to formalize many program-analysis problems, such as pointer analysis, and (2) as arelaxationmethod that uses a fast algorithm to over-approximate language-reachability on a directed graph. However, unlike its directed counterpart, the complexity of bidirected InterDyck-reachability still remains open. We establish the first decidable variant (i.e.,D1⊙D1-reachability) of bidirected InterDyck-reachability. InD1⊙D1-reachability, each of the two Dyck languages is restricted to have only a single kind of parenthesis pair. In particular, we show that the bidirectedD1⊙D1problem is in PTIME. We also show that when one extends each Dyck language to involvekdifferent kinds of parentheses (i.e.,Dk⊙Dk-reachability withk≥ 2), the problem is NP-hard (and therefore much harder). We have implemented the polynomial-time algorithm for bidirectedD1⊙D1-reachability.Dk⊙Dk-reachability provides a new over-approximation method for bidirectedDk⊙Dk-reachability in the sense thatDk⊙Dk-reachability can first be relaxed to bidirectedD1⊙D1-reachability, and then the resulting bidirectedD1⊙D1-reachability problem is solved precisely. We compare thisD1⊙D1-reachability-based approach against another known over-approximatingDk⊙Dk-reachability algorithm. Surprisingly, we found that the over-approximation approach based on bidirectedD1⊙D1-reachability computesmore precisesolutions, even though theD1⊙D1formalism is inherently less expressive than theDk⊙Dkformalism.more » « less
-
Hermenegildo, Manuel; Morales, José (Ed.)Context-free language reachability is an important program analysis framework, but the exact analysis problems can be intractable or undecidable, where CFL-reachability approximates such problems. For the same problem, there could be many over-approximations based on different CFLs \(C_1,\ldots ,C_n\). Suppose the reachability result of each \(C_i\) produces a set \(P_i\) of reachable vertex pairs. Is it possible to achieve better precision than the straightforward intersection \(\bigcap _{i=1}^n P_i\)? This paper gives an affirmative answer: although CFLs are not closed under intersections, in CFL-reachability we can “intersect” graphs. Specifically, we propose mutual refinement to combine different CFL-reachability-based over-approximations. Our key insight is that the standard CFL-reachability algorithm can be slightly modified to trace the edges that contribute to the reachability results of \(C_1\), and \(C_2\)-reachability only need to consider contributing edges of \(C_1\), which can, in turn, trace the edges that contribute to \(C_2\)-reachability, etc. We prove that there exists a unique optimal refinement result (fix-point). Experimental results show that mutual refinement can achieve better precision than the straightforward intersection with reasonable extra cost.more » « less
-
Abstract We analyze an algorithmic question about immersion theory: for which $$m$$, $$n$$, and $$CAT=\textbf{Diff}$$ or $$\textbf{PL}$$ is the question of whether an $$m$$-dimensional $CAT$-manifold is immersible in $$\mathbb{R}^{n}$$ decidable? We show that PL immersibility is decidable in all cases except for codimension 2, whereas smooth immersibility is decidable in all odd codimensions and undecidable in many even codimensions. As a corollary, we show that the smooth embeddability of an $$m$$-manifold with boundary in $$\mathbb{R}^{n}$$ is undecidable when $n-m$ is even and $$11m \geq 10n+1$$.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1145/3571227
