skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Checking δ-Satisfiability of Reals with Integrals
Many synthesis and verification problems can be reduced to determining the truth of formulas over the real numbers. These formulas often involve constraints with integrals in them. To this end, we extend the framework of δ-decision procedures with techniques for handling integrals of user-specified real functions. We implement this decision procedure in the tool ∫dReal, which is built on top of dReal. We evaluate ∫dReal on a suite of problems that include formulas verifying the fairness of algorithms and the privacy and the utility of privacy mechanisms and formulas that synthesize parameters for the desired utility of privacy mechanisms. The performance of the tool in these experiments demonstrates the effectiveness of ∫dReal.  more » « less
Award ID(s):
1900924 1901069 2007428
PAR ID:
10642031
Author(s) / Creator(s):
; ; ; ;
Publisher / Repository:
Association for Computing Machinery (ACM)
Date Published:
Journal Name:
Proceedings of the ACM on Programming Languages
Volume:
9
Issue:
OOPSLA1
ISSN:
2475-1421
Format(s):
Medium: X Size: p. 704-729
Size(s):
p. 704-729
Sponsoring Org:
National Science Foundation
More Like this
  1. Abstract LetGbe a linear real reductive Lie group. Orbital integrals define traces on the group algebra ofG. We introduce a construction of higher orbital integrals in the direction of higher cyclic cocycles on the Harish-Chandra Schwartz algebra ofG. We analyze these higher orbital integrals via Fourier transform by expressing them as integrals on the tempered dual ofG. We obtain explicit formulas for the pairing between the higher orbital integrals and theK-theory of the reduced group$$C^{*}$$-algebra, and we discuss their application toK-theory. 
    more » « less
  2. Local Differential Privacy (LDP) has been widely recognized as a powerful tool for providing a strong theoretical guarantee of data privacy to data contributors against an untrusted data collector. Under a typical LDP scheme, each data contributor independently randomly perturbs their data before submitting them to the data collector, which in turn infers valuable statistics about the original data from received perturbed data. Common to existing LDP mechanisms is an inherent trade-off between the level of privacy protection and data utility in the sense that strong data privacy often comes at the cost of reduced data utility. Frequency estimation based on Randomized Response (RR) is a fundamental building block of many LDP mechanisms. In this paper, we propose a novel Joint Randomized Response (JRR) mechanism based on correlated data perturbations to achieve locally differentially private frequency estimation. JRR divides data contributors into disjoint groups of two members and lets those in the same group jointly perturb their binary data to improve frequency-estimation accuracy and achieve the same level of data privacy by hiding the group membership information in contrast to the classical RR mechanism. Theoretical analysis and detailed simulation studies using both real and synthetic datasets show that JRR achieves the same level of data privacy as the classical RR mechanism while improving the frequency-estimation accuracy in the overwhelming majority of the cases by up to two orders of magnitude. 
    more » « less
  3. null (Ed.)
    Spam phone calls have been rapidly growing from nuisance to an increasingly effective scam delivery tool. To counter this increasingly successful attack vector, a number of commercial smartphone apps that promise to block spam phone calls have appeared on app stores, and are now used by hundreds of thousands or even millions of users. However, following a business model similar to some online social network services, these apps often collect call records or other potentially sensitive information from users’ phones with little or no formal privacy guarantees. In this paper, we study whether it is possible to build a practical collaborative phone blacklisting system that makes use of local differential privacy (LDP) mechanisms to provide clear privacy guarantees. We analyze the challenges and trade-offs related to using LDP, evaluate our LDP-based system on real-world user-reported call records collected by the FTC, and show that it is possible to learn a phone blacklist using a reasonable overall privacy budget and at the same time preserve users’ privacy while maintaining utility for the learned blacklist. 
    more » « less
  4. Dynamic spectrum sharing between licensed incumbent users (IUs) and unlicensed wireless industries has been well recognized as an efficient approach to solving spectrum scarcity as well as creating spectrum markets. Recently, both U.S. and European governments called a ruling on opening up spectrum that was initially licensed to sensitive military/federal systems. However, this introduces serious concerns on operational privacy (e.g., location, time and frequency of use) of IUs for national security concerns. Although several works have proposed obfuscation methods to address this problem, these techniques only rely on syntactic privacy models, lacking rigorous privacy guarantee. In this paper, we propose a comprehensive framework to provide real-time differential location privacy for sensitive IUs. We design a utility-optimal differentially private mechanism to reduce the loss in spectrum efficiency while protecting IUs from harmful interference. Furthermore, we strategically combine differential privacy with another privacy notion, expected inference error, to provide double shield protection for IU’s location privacy. Extensive simulations are conducted to validate our design and demonstrate significant improvements in utility and location privacy compared with other existing mechanisms. 
    more » « less
  5. To quantify trade-offs between increasing demand for open data sharing and concerns about sensitive information disclosure, statistical data privacy (SDP) methodology analyzes data release mechanisms that sanitize outputs based on confidential data. Two dominant frameworks exist: statistical disclosure control (SDC) and the more recent differential privacy (DP). Despite framing differences, both SDC and DP share the same statistical problems at their core. For inference problems, either we may design optimal release mechanisms and associated estimators that satisfy bounds on disclosure risk measures, or we may adjust existing sanitized output to create new statistically valid and optimal estimators. Regardless of design or adjustment, in evaluating risk and utility, valid statistical inferences from mechanism outputs require uncertainty quantification that accounts for the effect of the sanitization mechanism that introduces bias and/or variance. In this review, we discuss the statistical foundations common to both SDC and DP, highlight major developments in SDP, and present exciting open research problems in private inference. 
    more » « less