279 citations · 1.1k across the 46 of their papers we have counts for
50 papers
Leaf: An Instrumentation-based Dynamic Analysis Framework for Rust
Mohammad Omidvar Tehrani, Marco Gaboardi, Nick Sumner +1
This paper presents LEAF, an instrumentation-based dynamic analysis framework for Rust. Although Rust has grown rapidly in recent years, the landscape of program analysis tools for…
The Complexity of Verifying Boolean Programs as Differentially Private
Mark Bun, Marco Gaboardi, Ludmila Glinskih
We study the complexity of the problem of verifying differential privacy for while-like programs working over boolean values and making probabilistic choices. Programs in this clas…
Continual Release of Differentially Private Synthetic Data from Longitudinal Data Collections
Mark Bun, Marco Gaboardi, Marcel Neunhoeffer +1
Motivated by privacy concerns in long-term longitudinal studies in medical and social science research, we study the problem of continually releasing differentially private synthet…
A Formal Model for Secure Multiparty Computation
Amy Rathore, Marina Blanton, Marco Gaboardi +1
Although Secure Multiparty Computation (SMC) has seen considerable development in recent years, its use is challenging, resulting in complex code which obscures whether the securit…
Stability is Stable: Connections between Replicability, Privacy, and Adaptive Generalization
Mark Bun, Marco Gaboardi, Max Hopkins +5
The notion of replicable algorithms was introduced in Impagliazzo et al. [STOC '22] to describe randomized algorithms that are stable under the resampling of their inputs. More pre…
Differentially Private Confidence Intervals for Proportions under Stratified Random Sampling
Shurong Lin, Mark Bun, Marco Gaboardi +2
Confidence intervals are a fundamental tool for quantifying the uncertainty of parameters of interest. With the increase of data privacy awareness, developing a private version of…
Bunched Fuzz: Sensitivity for Vector Metrics
june wunder, Arthur Azevedo de Amorim, Patrick Baillot +1
Program sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and opt…
A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi, Justin Hsu +1
Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elemen…
On Incorrectness Logic and Kleene Algebra with Top and Tests
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compile…
Multiclass versus Binary Differentially Private PAC Learning
Mark Bun, Marco Gaboardi, Satchit Sivakumar
We show a generic reduction from multiclass differentially private PAC learning to binary private PAC learning. We apply this transformation to a recently proposed binary private P…
Higher-order probabilistic adversarial computations: Categorical semantics and program logics
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi +3
Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with pri…
Covariance-Aware Private Mean Estimation Without Private Covariance Estimation
Gavin Brown, Marco Gaboardi, Adam Smith +2
We present two sample-efficient differentially private mean estimators for -dimensional (sub)Gaussian distributions with unknown covariance. Informally, given …
Empirical Risk Minimization in the Non-interactive Local Model of Differential Privacy
Di Wang, Marco Gaboardi, Adam Smith +1
In this paper, we study the Empirical Risk Minimization (ERM) problem in the non-interactive Local Differential Privacy (LDP) model. Previous research on this problem \citep{smith2…
Coupled Relational Symbolic Execution for Differential Privacy
Gian Pietro Farina, Stephen Chong, Marco Gaboardi
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…
Controlling Privacy Loss in Sampling Schemes: an Analysis of Stratified and Cluster Sampling
Mark Bun, Jörg Drechsler, Marco Gaboardi +2
Sampling schemes are fundamental tools in statistics, survey design, and algorithm design. A fundamental result in differential privacy is that a differentially private mechanism r…
Graded Hoare Logic and its Categorical Semantics
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard +1
Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend o…
The Complexity of Verifying Loop-Free Programs as Differentially Private
Marco Gaboardi, Kobbi Nissim, David Purser
We study the problem of verifying differential privacy for loop-free programs with probabilistic choice. Programs in this class can be seen as randomized Boolean circuits, which we…
Facility Location Problem in Differential Privacy Model Revisited
Yunus Esencayi, Marco Gaboardi, Shi Li +1
In this paper we study the uncapacitated facility location problem in the model of differential privacy (DP) with uniform facility cost. Specifically, we first show that, under the…
A Programming Framework for Differential Privacy with Accuracy Concentration Bounds
Elisabet Lobo-Vesga, Alejandro Russo, Marco Gaboardi
Differential privacy offers a formal framework for reasoning about privacy and accuracy of computations on private data. It also offers a rich set of building blocks for constructi…
Privacy Amplification by Mixing and Diffusion Mechanisms
Borja Balle, Gilles Barthe, Marco Gaboardi +1
A fundamental result in differential privacy states that the privacy guarantees of a mechanism are preserved by any post-processing of its output. In this paper we investigate unde…
Hypothesis Testing Interpretations and Renyi Differential Privacy
Borja Balle, Gilles Barthe, Marco Gaboardi +2
Differential privacy is a de facto standard in data privacy, with applications in the public and private sectors. A way to explain differential privacy, which is particularly appea…
Bidirectional Type Checking for Relational Properties
Ezgi Çiçek, Weihao Qu, Gilles Barthe +2
Relational type systems have been designed for several applications including information flow, differential privacy, and cost analysis. In order to achieve the best results, these…
Relational Cost Analysis for Functional-Imperative Programs
Weihao Qu, Marco Gaboardi, Deepak Garg
Relational cost analysis aims at formally establishing bounds on the difference in the evaluation costs of two programs. As a particular case, one can also use relational cost anal…
Locally Private Mean Estimation: Z-test and Tight Confidence Intervals
Marco Gaboardi, Ryan Rogers, Or Sheffet
This work provides tight upper- and lower-bounds for the problem of mean estimation under -differential privacy in the local model, when the input is composed of i.i.d. draw…