Adrià Gascón

dblp:90/3256 · DBLP profile ↗
← Back
48ranked-venue papers
13as first author
14since 2021 · last 2026
0000-0002-1807-8311ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Security and privacy · 22 · 2 first-author · 11 since 2021Theory of computation · 16 · 10 first-authorArtificial intelligence and machine learning · 9 · 1 first-author · 3 since 2021Software engineering, systems software and programming languages · 3 · 2 first-authorApplied, interdisciplinary, general and emerging computing · 2Human-computer interaction and ubiquitous computing · 1
YearPublicationVenuePosition
2026 SNPeek: Side-Channel Analysis for Privacy Applications on Confidential VMs
Ruiyi Zhang 0001, Albert Cheu, Adrià Gascón, Daniel Moghimi, Phillipp Schoppmann, Michael Schwarz 0001, Octavian Suciu
NDSS3
2026 TDXRay: Microarchitectural Side-Channel Analysis of Intel TDX for Real-World Workloads
Tristan Hornetz, Hosein Yavarzadeh, Albert Cheu, Adrià Gascón, Lukas Gerlach 0001, Daniel Moghimi, Phillipp Schoppmann, Michael Schwarz 0001, Ruiyi Zhang 0001
SP4
2025 Founding Zero-Knowledge Proof of Training on Optimum Vicinity
abstract
Zero-knowledge proofs of training (zkPoT) allow a party to prove that a model is trained correctly on a committed dataset without revealing any additional information about the model or the dataset. Existing zkPoT protocols prove the entire training process in zero knowledge; i.e., they prove that the final model was obtained in an iterative fashion starting from the training data and a random seed (and potentially other parameters) and applying the correct algorithm at each iteration. This approach inherently requires the prover to perform work linear to the number of iterations.
Gefei Tan, Adrià Gascón, Sarah Meiklejohn, Mariana Raykova 0001, Xiao Wang 0012, Ning Luo 0002
CCS2
2025 Willow: Secure Aggregation with One-Shot Clients
James Bell-Clark, Adrià Gascón, Baiyu Li, Mariana Raykova 0001, Phillipp Schoppmann
CRYPTO (8)2
2025 Privacy Reasoning in Ambiguous Contexts
abstract
We study the ability of language models to reason about appropriate information disclosure - a central aspect of the evolving field of agentic privacy. Whereas previous works have focused on evaluating a model's ability to align with human decisions, we examine the role of ambiguity and missing context on model performance when making information-sharing decisions. We identify context ambiguity as a crucial barrier for high performance in privacy assessments. By designing Camber, a framework for context disambiguation, we show that model-generated decision rationales can reveal ambiguities and that systematically disambiguating context based on these rationales leads to significant accuracy improvements (up to 13.3% in precision and up to 22.3% in recall) as well as reductions in prompt sensitivity. Overall, our results indicate that approaches for context disambiguation are a promising way forward to enhance agentic privacy reasoning.
Ren Yi, Octavian Suciu, Adrià Gascón, Sarah Meiklejohn, Eugene Bagdasarian, Marco Gruteser
NeurIPS3
2025 Hash-Prune-Invert: Improved Differentially Private Heavy-Hitter Detection in the Two-Server Model
abstract
Differentially private (DP) heavy-hitter detection is an important primitive for data analysis. Given a threshold$t$and a dataset of$n$items from a domain of size$d$, such detection algorithms ignore items occurring fewer than$t$times while identifying items occurring more than$t+\Delta$times; we call$\Delta$the error margin. In the central model where a curator holds the entire dataset,$(\varepsilon, \delta)$-DP algorithms can achieve error margin$\Theta\left(\frac{1}{\varepsilon} \log \frac{1}{\delta}\right)$, which is optimal when$d\gg 1/\delta$. Several works, e.g., Poplar (S&P 2021), have proposed protocols in which two or more non-colluding servers jointly compute the heavy hitters from inputs held by$n$clients. Unfortunately, existing protocols suffer from an undesirable dependence on Iog$d$in terms of both server efficiency (computation, communication, and round complexity) and accuracy (i.e., error margin), making them unsuitable for large domains (e.g., when items are kB-long strings, log$d\approx 10^{4}$). We present hash-prune-invert (HPI), a technique for compiling any heavy-hitter protocol with the log$d$dependencies mentioned above into a new protocol with improvements across the board: computation, communication, and round complexity depend (roughly) on log$n$rather than log$d$, and the error margin is independent of$d$. Our transformation preserves privacy against an active adversary corrupting at most one of the servers and any number of clients. We apply HPI to an improved version of Poplar, also introduced in this work, that improves Poplar's error margin by roughly a factor of$\sqrt{n}$(regardless of$d)$. Our experiments confirm that the resulting protocol improves efficiency and accuracy for large$d$.
Borja Balle, James Bell-Clark, Albert Cheu, Adrià Gascón, Jonathan Katz, Mariana Raykova 0001, Phillipp Schoppmann, Thomas Steinke 0002
SP4
2024 Computationally Secure Aggregation and Private Information Retrieval in the Shuffle Model
abstract
The shuffle model has recently emerged as a popular setting for differential privacy, where clients can communicate with a central server using anonymous channels or an intermediate message shuffler. This model was also explored in the context of cryptographic tasks such as secure aggregation and private information retrieval (PIR). However, this study was almost entirely restricted to the stringent notion of information-theoretic security.
Adrià Gascón, Yuval Ishai, Mahimna Kelkar, Baiyu Li, Yiping Ma 0001, Mariana Raykova 0001
CCS1
2023 Amplification by Shuffling without Shuffling
abstract
Motivated by recent developments in the shuffle model of differential privacy, we propose a new approximate shuffling functionality called Alternating Shuffle, and provide a protocol implementing alternating shuffling in a single-server threat model where the adversary observes all communication. Unlike previous shuffling protocols in this threat model, the per-client communication of our protocol only grows sub-linearly in the number of clients. Moreover, we study the concrete efficiency of our protocol and show it can improve per-client communication by one or more orders of magnitude with respect to previous (approximate) shuffling protocols. We also show a differential privacy amplification result for alternating shuffling analogous to the one for uniform shuffling, and demonstrate that shuffling-based protocols for secure summation based a construction of Ishai et al. remain secure under the Alternating Shuffle. In the process we also develop a protocol for exact shuffling in single-server threat model with amortized logarithmic communication per-client which might be of independent interest.
Borja Balle, James Bell-Clark, Adrià Gascón
CCS3
2023 Federated Heavy Hitter Recovery under Linear Sketching
abstract
Motivated by real-life deployments of multi-round federated analytics with secure aggregation, we investigate the fundamental communication-accuracy tradeoffs of the heavy hitter discovery and approximate (open-domain) histogram problems under a linear sketching constraint. We propose efficient algorithms based on local subsampling and invertible bloom look-up tables (IBLTs). We also show that our algorithms are information-theoretically optimal for a broad class of interactive schemes. The results show that the linear sketching constraint does increase the communication cost for both tasks by introducing an extra linear dependence on the number of users in a round. Moreover, our results also establish a separation between the communication cost for heavy hitter discovery and approximate histogram in the multi-round setting. The dependence on the number of rounds $R$ is at most logarithmic for heavy hitter discovery whereas that of approximate histogram is $\Theta(\sqrt{R})$. We also empirically demonstrate our findings.
Adrià Gascón, Peter Kairouz, Ziteng Sun, Ananda Theertha Suresh
ICML1
2023 ACORN: Input Validation for Secure Aggregation
James Bell-Clark, Adrià Gascón, Tancrède Lepoint, Baiyu Li, Sarah Meiklejohn, Mariana Raykova 0001, Cathie Yun
USENIX Security Symposium2
2022 Distributed, Private, Sparse Histograms in the Two-Server Model
abstract
We consider the computation of sparse, (ε, ϑ)-differentially private~(DP) histograms in the two-server model of secure multi-party computation~(MPC), which has recently gained traction in the context of privacy-preserving measurements of aggregate user data. We introduce protocols that enable two semi-honest non-colluding servers to compute histograms over the data held by multiple users, while only learning a private view of the data. Our solution achieves the same asymptotic l∞-error of O(log(1/ϑoverε) as in the central model of DP, but without relying on a trusted curator. The server communication and computation costs of our protocol are independent of the number of histogram buckets, and are linear in the number of users, while the client cost is independent of the number of users, ε, and ϑ. Its linear dependence on the number of users lets our protocol scale well, which we confirm using microbenchmarks: for a billion users, ε = 0.5, and ϑ = 10-11, the per-user cost of our protocol is only 1.08 ms of server computation and 339 bytes of communication. In contrast, a baseline protocol using garbled circuits only allows up to 106 users, where it requires 600 KB communication per user.
James Bell-Clark, Adrià Gascón, Badih Ghazi, Ravi Kumar 0001, Pasin Manurangsi, Mariana Raykova 0001, Phillipp Schoppmann
CCS2
2022 Towards Sparse Federated Analytics: Location Heatmaps under Distributed Differential Privacy with Secure Aggregation
abstract
We design a scalable algorithm to privately generate location heatmaps over decentralized data from millions of user devices. It aims to ensure differential privacy before data becomes visible to a service provider while maintaining high data accuracy and minimizing resource consumption on users’ devices. To achieve this, we revisit distributed differential privacy based on recent results in secure multiparty computation, and we design a scalable and adaptive distributed differential privacy approach for location analytics. Evaluation on public location datasets shows that this approach successfully generates metropolitan-scale heatmaps from millions of user samples with a worstcase client communication overhead that is significantly smaller than existing state-of-the-art private protocols of similar accuracy.
Eugene Bagdasarian, Peter Kairouz, Stefan Mellem, Adrià Gascón, Kallista A. Bonawitz, Deborah Estrin, Marco Gruteser
Proc. Priv. Enhancing Technol.4
2021 MPC-Friendly Commitments for Publicly Verifiable Covert Security
abstract
We address the problem of efficiently verifying a commitment in a two-party computation. This addresses the scenario where a party P1 commits to a value x to be used in a subsequent secure computation with another party P2 that wants to receive assurance that P1 did not cheat, i.e. that x was indeed the value inputted into the secure computation. Our constructions operate in the publicly verifiable covert (PVC) security model, which is a relaxation of the malicious model of MPC, appropriate in settings where P1 faces a reputational harm if caught cheating.
Nitin Agrawal 0002, James Bell-Clark, Adrià Gascón, Matt J. Kusner
CCS3
2021 Formalising $\varSigma$-Protocols and Commitment Schemes Using CryptHOL
abstract
Machine-checked proofs of security are important to increase the rigour of provable security. In this work we present a formalised theory of two fundamental two party cryptographic primitives: Σ-protocols and Commitment Schemes. Σ-protocols allow a prover to convince a verifier that they possess some knowledge without leaking information about the knowledge. Commitment schemes allow a committer to commit to a message and keep it secret until revealing it at a later time. We use CryptHOL (Lochbihler in Archive of formal proofs, 2017) to formalise both primitives and prove secure multiple examples namely; the Schnorr, Chaum-Pedersen and Okamoto Σ-protocols as well as a construction that allows for compound (AND and OR) Σ-protocols and the Pedersen and Rivest commitment schemes. A highlight of the work is a formalisation of the construction of commitment schemes from Σ-protocols (Damgard in Lecture notes, 2002). We formalise this proof at an abstract level using the modularity available in Isabelle/HOL and CryptHOL. This way, the proofs of the instantiations come for free.
David Butler 0002, Andreas Lochbihler, David Aspinall 0001, Adrià Gascón
J. Autom. Reason.4
2020 Private Protocols for U-Statistics in the Local Model and Beyond
abstract
In this paper, we study the problem of computing $U$-statistics of degree $2$, i.e., quantities that come in the form of averages over pairs of data points, in the local model of differential privacy (LDP). The class of $U$-statistics covers many statistical estimates of interest, including Gini mean difference, Kendall’s tau coefficient and Area under the ROC Curve (AUC), as well as empirical risk measures for machine learning problems such as ranking, clustering and metric learning. We first introduce an LDP protocol based on quantizing the data into bins and applying randomized response, which guarantees an $\epsilon$-LDP estimate with a Mean Squared Error (MSE) of $O(1/\sqrt{n}\epsilon)$ under regularity assumptions on the $U$-statistic or the data distribution. We then propose a specialized protocol for AUC based on a novel use of hierarchical histograms that achieves MSE of $O(\alpha^3/n\epsilon^2)$ for arbitrary data distribution. We also show that 2-party secure computation allows to design a protocol with MSE of $O(1/n\epsilon^2)$, without any assumption on the kernel function or data distribution and with total communication linear in the number of users $n$. Finally, we evaluate the performance of our protocols through experiments on synthetic and real datasets.
James Bell-Clark, Aurélien Bellet, Adrià Gascón, Tejas Kulkarni
AISTATS3
2020 Data Generation for Neural Programming by Example
abstract
Programming by example is the problem of synthesizing a program from a small set of input / output pairs. Recent works applying machine learning methods to this task show promise, but are typically reliant on generating synthetic examples for training. A particular challenge lies in generating meaningful sets of inputs and outputs, which well-characterize a given program and accurately demonstrate its behavior. Where examples used for testing are generated by the same method as training data then the performance of a model may be partly reliant on this similarity. In this paper we introduce a novel approach using an SMT solver to synthesize inputs which cover a diverse set of behaviors for a given program. We carry out a case study comparing this method to existing synthetic data generation procedures in the literature, and find that data generated using our approach improves both the discriminatory power of example sets and the ability of trained machine learning models to generalize to unfamiliar data.
Judith Clymo, Adrià Gascón, Brooks Paige, Nathanaël Fijalkow, Haik Manukian
AISTATS2
2020 Private Summation in the Multi-Message Shuffle Model
abstract
The shuffle model of differential privacy (Erlingsson et al. SODA 2019; Cheu et al. EUROCRYPT 2019) and its close relative encode-shuffle-analyze (Bittau et al. SOSP 2017) provide a fertile middle ground between the well-known local and central models. Similarly to the local model, the shuffle model assumes an untrusted data collector who receives privatized messages from users, but in this case a secure shuffler is used to transmit messages from users to the collector in a way that hides which messages came from which user. An interesting feature of the shuffle model is that increasing the amount of messages sent by each user can lead to protocols with accuracies comparable to the ones achievable in the central model. In particular, for the problem of privately computing the sum of n bounded real values held by n different users, Cheu et al. showed that O(sqrtn ) messages per user suffice to achieve O(1) error (the optimal rate in the central model), while Balle et al. (CRYPTO 2019) recently showed that a single message per user leads to Theta(n^1/3 ) MSE (mean squared error), a rate strictly in-between what is achievable in the local and central models. This paper introduces two new protocols for summation in the shuffle model with improved accuracy and communication trade-offs. Our first contribution is a recursive construction based on the protocol from Balle et al. mentioned above, providing poly(log log n) error with O(log log n) messages per user. The second contribution is a protocol with O(1) error and O(1) messages per user based on a novel analysis of the reduction from secure summation to shuffling introduced by Ishai et al. (FOCS 2006) (the original reduction required O(log n) messages per user). We also provide a numerical evaluation showing that our protocols provide good trade-offs between privacy, accuracy and communication for realistic values of n.
Borja Balle, James Bell-Clark, Adrià Gascón, Kobbi Nissim
CCS3
2020 Secure Single-Server Aggregation with (Poly)Logarithmic Overhead
abstract
Secure aggregation is a cryptographic primitive that enables a server to learn the sum of the vector inputs of many clients. Bonawitz et al. (CCS 2017) presented a construction that incurs computation and communication for each client linear in the number of parties. While this functionality enables a broad range of privacy preserving computational tasks, scaling concerns limit its scope of use. We present the first constructions for secure aggregation that achieve polylogarithmic communication and computation per client. Our constructions provide security in the semi-honest and the semi-malicious settings where the adversary controls the server and a δ-fraction of the clients, and correctness with up to δ-fraction dropouts among the clients. Our constructions show how to replace the complete communication graph of Bonawitz et al., which entails the linear overheads, with a k-regular graph of logarithmic degree while maintaining the security guarantees. Beyond improving the known asymptotics for secure aggregation, our constructions also achieve very efficient concrete parameters. The semi-honest secure aggregation can handle a billion clients at the per-client cost of the protocol of Bonawitz et al. for a thousand clients. In the semi-malicious setting with 10 4 clients, each client needs to communicate only with 3% of the clients to have a guarantee that its input has been added together with the inputs of at least 5000 other clients, while withstanding up to 5% corrupt clients and 5% dropouts. We also show an application of secure aggregation to the task of secure shuffling which enables the first cryptographically secure instantiation of the shuffle model of differential privacy.
James Bell-Clark, Kallista A. Bonawitz, Adrià Gascón, Tancrède Lepoint, Mariana Raykova 0001
CCS3
2020 Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL
abstract
Multi-Party Computation (MPC) allows multiple parties to compute a function together while keeping their inputs private. Large scale implementations of MPC protocols are becoming practical thus it is important to have strong guarantees for the whole development process, from the underlying cryptography to the implementation. Computer aided proofs are a way to provide such guarantees.
David Butler 0002, David Aspinall 0001, Adrià Gascón
CPP3
2020 Reconstructing Genotypes in Private Genomic Databases from Genetic Risk Scores
Brooks Paige, James Bell-Clark, Aurélien Bellet, Adrià Gascón, Daphne Ezer
RECOMB4
2020 Grammar-Based Compression of Unranked Trees
Adrià Gascón, Markus Lohrey, Sebastian Maneth, Carl Philipp Reh, Kurt Sieber
Theory Comput. Syst.1
2020 Secure and Scalable Document Similarity on Distributed Databases: Differential Privacy to the Rescue
abstract
Abstract Privacy-preserving collaborative data analysis enables richer models than what each party can learn with their own data. Secure Multi-Party Computation (MPC) offers a robust cryptographic approach to this problem, and in fact several protocols have been proposed for various data analysis and machine learning tasks. In this work, we focus on secure similarity computation between text documents, and the application to k-nearest neighbors (k-NN) classification. Due to its non-parametric nature, k-NN presents scalability challenges in the MPC setting. Previous work addresses these by introducing non-standard assumptions about the abilities of an attacker, for example by relying on non-colluding servers. In this work, we tackle the scalability challenge from a different angle, and instead introduce a secure preprocessing phase that reveals differentially private (DP) statistics about the data. This allows us to exploit the inherent sparsity of text data and significantly speed up all subsequent classifications.
Phillipp Schoppmann, Lennart Vogelsang, Adrià Gascón, Borja Balle
Proc. Priv. Enhancing Technol.3
2020 PrivEdge: From Local to Distributed Private Training and Prediction
abstract
Machine Learning as a Service (MLaaS) operators provide model training and prediction on the cloud. MLaaS applications often rely on centralised collection and aggregation of user data, which could lead to significant privacy concerns when dealing with sensitive personal data. To address this problem, we propose PrivEdge, a technique for privacy-preserving MLaaS that safeguards the privacy of users who provide their data for training, as well as users who use the prediction service. With PrivEdge, each user independently uses their private data to locally train a one-class reconstructive adversarial network that succinctly represents their training data. As sending the model parameters to the service provider in the clear would reveal private information, PrivEdge secret-shares the parameters among two non-colluding MLaaS providers, to then provide cryptographically private prediction services through secure multi-party computation techniques. We quantify the benefits of PrivEdge and compare its performance with state-of-the-art centralised architectures on three privacy-sensitive image-based tasks: individual identification, writer identification, and handwritten letter recognition. Experimental results show that PrivEdge has high precision and recall in preserving privacy, as well as in distinguishing between private and non-private images. Moreover, we show the robustness of PrivEdge to image compression and biased training data. The source code is available at https://github.com/smartcameras/PrivEdge.
Ali Shahin Shamsabadi, Adrià Gascón, Hamed Haddadi 0001, Andrea Cavallaro
IEEE Trans. Inf. Forensics Secur.2
2019 QUOTIENT: Two-Party Secure Neural Network Training and Prediction
abstract
Recently, there has been a wealth of effort devoted to the design of secure protocols for machine learning tasks. Much of this is aimed at enabling secure prediction from highly-accurate Deep Neural Networks (DNNs). However, as DNNs are trained on data, a key question is how such models can be also trained securely. The few prior works on secure DNN training have focused either on designing custom protocols for existing training algorithms, or on developing tailored training algorithms and then applying generic secure protocols. In this work, we investigate the advantages of designing training algorithms alongside a novel secure protocol, incorporating optimizations on both fronts. We present QUOTIENT, a new method for discretized training of DNNs, along with a customized secure two-party protocol for it. QUOTIENT incorporates key components of state-of-the-art DNN training such as layer normalization and adaptive gradient methods, and improves upon the state-of-the-art in DNN training in two-party computation. Compared to prior work, we obtain an improvement of 50X in WAN time and 6% in absolute accuracy.
Nitin Agrawal 0002, Ali Shahin Shamsabadi, Matt J. Kusner, Adrià Gascón
CCS4
2019 PPML '19: Privacy Preserving Machine Learning
abstract
The area of privacy preserving machine learning has been of growing importance in practice, which has lead to an increased interest in this topic in both academia and industry. We have witnessed this through numerous papers and systems published and developed in the recent years to address challenges in this area. The solutions proposed in this space leverage many different approaches and techniques coming from machine learning, cryptography, and security. Thus, the workshop aims to be a forum to unify different perspectives and start a discussion about the relative merits of each approach. It will also serve as a venue for networking people from different communities interested in this problem, and hopefully foster fruitful long-term collaboration.
Borja Balle, Adrià Gascón, Olga Ohrimenko, Mariana Raykova 0001, Phillipp Schoppmann, Carmela Troncoso
CCS2
2019 Make Some ROOM for the Zeros: Data Sparsity in Secure Distributed Machine Learning
abstract
Exploiting data sparsity is crucial for the scalability of many data analysis tasks. However, while there is an increasing interest in efficient secure computation protocols for distributed machine learning, data sparsity has so far not been considered in a principled way in that setting.
Phillipp Schoppmann, Adrià Gascón, Mariana Raykova 0001, Benny Pinkas
CCS2
2019 Distributed Vector-OLE: Improved Constructions and Implementation
abstract
We investigate concretely efficient protocols for distributed oblivious linear evaluation over vectors (Vector-OLE). Boyle et al. (CCS 2018) proposed a protocol for secure distributed pseudorandom Vector-OLE generation using sublinear</>communication, but they did not provide an implementation. Their construction is based on a variant of the LPN assumption and assumes a distributed key generation protocol for single-point Function Secret Sharing (FSS), as well as an efficient batching scheme to obtain multi-point FSS. We show that this requirement can be relaxed, resulting in a weaker variant of FSS, for which we give an efficient protocol. This allows us to use efficient probabilistic batch codes that were also recently used for batched PIR by Angel et al. (S&P 2018). We construct a full Vector-OLE generator from our protocols, and compare it experimentally with alternative approaches. Our implementation parallelizes very well, and has low communication overhead in practice. For generating a VOLE of size $2^20 $, our implementation only takes $0.52$s on 32 cores.
Phillipp Schoppmann, Adrià Gascón, Leonie Reichert, Mariana Raykova 0001
CCS2
2019 The Privacy Blanket of the Shuffle Model
Borja Balle, James Bell-Clark, Adrià Gascón, Kobbi Nissim
CRYPTO (2)3
2018 Blind Justice: Fairness with Encrypted Sensitive Attributes
abstract
Recent work has explored how to train machine learning models which do not discriminate against any subgroup of the population as determined by sensitive attributes such as gender or race. To avoid disparate treatment, sensitive attributes should not be considered. On the other hand, in order to avoid disparate impact, sensitive attributes must be examined, e.g., in order to learn a fair model, or to check if a given model is fair. We introduce methods from secure multi-party computation which allow us to avoid both. By encrypting sensitive attributes, we show how an outcome-based fair model may be learned, checked, or have its outputs verified and held to account, without users revealing their sensitive attributes.
Niki Kilbertus, Adrià Gascón, Matt J. Kusner, Michael Veale, Krishna P. Gummadi, Adrian Weller
ICML2
2018 TAPAS: Tricks to Accelerate (encrypted) Prediction As a Service
abstract
Machine learning methods are widely used for a variety of prediction problems. Prediction as a service is a paradigm in which service providers with technological expertise and computational resources may perform predictions for clients. However, data privacy severely restricts the applicability of such services, unless measures to keep client data private (even from the service provider) are designed. Equally important is to minimize the nature of computation and amount of communication required between client and server. Fully homomorphic encryption offers a way out, whereby clients may encrypt their data, and on which the server may perform arithmetic computations. The one drawback of using fully homomorphic encryption is the amount of time required to evaluate large machine learning models on encrypted data. We combine several ideas from the machine learning literature, particularly work on quantization and sparsification of neural networks, together with algorithmic tools to speed-up and parallelize computation using encrypted data.
Amartya Sanyal, Matt J. Kusner, Adrià Gascón, Varun Kanade
ICML3
2017 Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis
Adrià Gascón, Ashish Tiwari 0001, Brent Carmer, Umang Mathur 0001
CAV (2)1
2017 How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation
David Butler 0002, David Aspinall 0001, Adrià Gascón
ITP3
2017 Privacy-Preserving Distributed Linear Regression on High-Dimensional Data
abstract
Abstract We propose privacy-preserving protocols for computing linear regression models, in the setting where the training dataset is vertically distributed among several parties. Our main contribution is a hybrid multi-party computation protocol that combines Yao’s garbled circuits with tailored protocols for computing inner products. Like many machine learning tasks, building a linear regression model involves solving a system of linear equations. We conduct a comprehensive evaluation and comparison of different techniques for securely performing this task, including a new Conjugate Gradient Descent (CGD) algorithm. This algorithm is suitable for secure computation because it uses an efficient fixed-point representation of real numbers while maintaining accuracy and convergence rates comparable to what can be obtained with a classical solution using floating point numbers. Our technique improves on Nikolaenko et al.’s method for privacy-preserving ridge regression (S&P 2013), and can be used as a building block in other analyses. We implement a complete system and demonstrate that our approach is highly scalable, solving data analysis problems with one million records and one hundred features in less than one hour of total running time.
Adrià Gascón, Phillipp Schoppmann, Borja Balle, Mariana Raykova 0001, Jack Doerner, Samee Zahur, David Evans 0001
Proc. Priv. Enhancing Technol.1
2016 Revisiting Square-Root ORAM: Efficient Random Access in Multi-party Computation
abstract
Hiding memory access patterns is required for secure computation, but remains prohibitively expensive for many interesting applications. Prior work has either developed custom algorithms that minimize the need for data-dependant memory access, or proposed the use of Oblivious RAM (ORAM) to provide a general-purpose solution. However, most ORAMs are designed for client-server scenarios, and provide only asymptotic benefits in secure computation. Even the best prior schemes show concrete benefits over naïve linear scan only for array sizes greater than 100. This immediately implies each ORAM access is 100 times slower than a single access at a known location. Even then, prior evaluations ignore the substantial initialization cost of existing schemes. We show how the classical square-root ORAM of Goldreich and Ostrovsky can be modified to overcome these problems, even though it is asymptotically worse than the best known schemes. Specifically, we show a design that has over 100x lower initialization cost, and provides benefits over linear scan for just 8 blocks of data. For all benchmark applications we tried, including Gale-Shapley stable matching and the scrypt key derivation function, our scheme outperforms alternate approaches across a wide range of parameters, often by several orders of magnitude.
Samee Zahur, Xiao Wang 0012, Mariana Raykova 0001, Adrià Gascón, Jack Doerner, David Evans 0001, Jonathan Katz
IEEE Symposium on Security and Privacy4
2016 The HOM Problem is EXPTIME-Complete
abstract
We define a new class of tree automata with constraints and prove decidability of the emptiness problem for this class in exponential time. As a consequence, we obtain several EXPTIME-completeness results for problems on images of regular tree languages under tree homomorphisms, like set inclusion, regularity (HOM problem), and finiteness of set difference. Our result also has implications in term rewriting, since the set of reducible terms of a term rewrite system can be described as the image of a tree homomorphism. In particular, we prove that inclusion of sets of normal forms of term rewrite systems can be decided in exponential time. Analogous consequences arise in the context of XML typechecking, since types are defined by tree automata and some type transformations are homomorphic.
Carles Creus, Adrià Gascón, Guillem Godoy, Lander Ramos
SIAM J. Comput.2
2015 Program Synthesis Using Dual Interpretation
Ashish Tiwari 0001, Adrià Gascón, Bruno Dutertre
CADE2
2015 Two-Restricted One Context Unification is in Polynomial Time
abstract
One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.
Adrià Gascón, Manfred Schmidt-Schauß, Ashish Tiwari 0001
CSL1
2015 One Context Unification Problems Solvable in Polynomial Time
abstract
One context unification extends first-order unification by introducing a single context variable, possibly with multiple occurrences. One context unification is known to be in NP, but it is not known to be solvable in polynomial time. In this paper, we present a polynomial time algorithm for certain interesting classes of the one context unification problem. Our algorithm is presented as an inference system that non-trivially extends the usual inference rules for first-order unification. The algorithm is of independent value as it can be used, with slight modifications, to solve other problems, such as the first-order unification problem that tolerates one clash.
Adrià Gascón, Ashish Tiwari 0001, Manfred Schmidt-Schauß
LICS1
2014 Template-based circuit understanding
abstract
When verifying or reverse-engineering digital circuits, one often wants to identify and understand small components in a larger system. A possible approach is to show that the sub-circuit under investigation is functionally equivalent to a reference implementation. In many cases, this task is difficult as one may not have full information about the mapping between input and output of the two circuits, or because the equivalence depends on settings of control inputs. We propose a template-based approach that automates this process. It extracts a functional description for a low-level combinational circuit by showing it to be equivalent to a reference implementation, while synthesizing an appropriate mapping of input and output signals and setting of control signals. The method relies on solving an exists/forall problem using an SMT solver, and on a pruning technique based on signature computation.
Adrià Gascón, Pramod Subramanyan, Bruno Dutertre, Ashish Tiwari 0001, Dejan Jovanovic, Sharad Malik
FMCAD1
2013 Emptiness and Finiteness for Tree Automata with Global Reflexive Disequality Constraints
Carles Creus, Adrià Gascón, Guillem Godoy
J. Autom. Reason.2
2012 The HOM Problem is EXPTIME-Complete
abstract
The HOM problem questions whether the image of a given regular tree language through a given tree homomorphism is also regular. Decidability of HOM is an important theoretical question which was open for a long time. Recently, HOM has been proved decidable with a triple exponential time algorithm. In this paper we obtain an exponential time algorithm for this problem, and conclude that it is EXPTIME-complete. The proof builds upon previous results and techniques on tree automata with constraints.
Carles Creus, Adrià Gascón, Guillem Godoy, Lander Ramos
LICS2
2012 One-context Unification with STG-Compressed Terms is in NP
abstract
One-context unification is an extension of first-order term unification in which a variable of arity one standing for a context may occur in the input terms. This problem arises in areas like program analysis, term rewriting and XML processing and is known to be solvable in nondeterministic polynomial time. We prove that this problem can be solved in nondeterministic polynomial time also when the input is compressed using Singleton Tree Grammars (STG's). STG's are a grammar-based compression method for terms that generalizes the directed acyclic graph representation. They have been recently considered as an efficient in-memory representation for large terms, since several operations on terms can be performed efficiently on their STG representation without a prior decompression.
Carles Creus, Adrià Gascón, Guillem Godoy
RTA2
2011 Learning Theory through Videos - A Teaching Experience in a Theoretical Course based on Self-learning Videos and Problem-solving Sessions
Marta Arias, Carles Creus, Adrià Gascón, Guillem Godoy
CSEDU (2)3
2011 First-Order Unification on Compressed Terms
abstract
Singleton Tree Grammars (STGs) have recently drawn considerable attention. They generalize the sharing of subtrees known from DAGs to sharing of connected subgraphs. This allows to obtain smaller in-memory representations of trees than with DAGs. In the past years some important tree algorithms were proved to perform efficiently (without decompression) over STGs; e.g., type checking, equivalence checking, and unification. We present a tool that implements an extension of the unification algorithm for STGs. This algorithm makes extensive use of equivalence checking. For the latter we implemented two variants, the classical exact one and a recent randomized one. Our experiments show that the randomized algorithm performs better. The running times are also compared to those of unification over uncompressed trees.
Adrià Gascón, Sebastian Maneth, Lander Ramos
RTA1
2011 Unification and matching on compressed terms
abstract
Term unification plays an important role in many areas of computer science, especially in those related to logic. The universal mechanism of grammar-based compression for terms, in particular the so-calledsingleton tree grammars (STGAs), have recently drawn considerable attention. Using STGs, terms of exponential size and height can be represented in linear space. Furthermore, the term representation by directed acyclic graphs (dags) can be efficiently simulated. The present article is the result of an investigation on term unification and matching when the terms given as input are represented using different compression mechanisms for terms such as dags and singleton tree grammars. We describe a polynomial time algorithm for context matching with dags, when the number of different context variables is fixed for the problem. For the same problem, NP-completeness is obtained when the terms are represented using the more general formalism of singleton tree grammars. For first-order unification and matching polynomial time algorithms are presented, each of them improving previous results for those problems.
Adrià Gascón, Guillem Godoy, Manfred Schmidt-Schauß
ACM Trans. Comput. Log.1
2010 Context unification with one context variable
Adrià Gascón, Guillem Godoy, Manfred Schmidt-Schauß, Ashish Tiwari 0001
J. Symb. Comput.1
2009 Unification with Singleton Tree Grammars
Adrià Gascón, Guillem Godoy, Manfred Schmidt-Schauß
RTA1
2008 Context Matching for Compressed Terms
abstract
This paper is an investigation of the matching problem for term equations s = t where s contains context variables and first-order variables, and both terms s and t are given using some kind of compressed representation. The main result is a polynomial time algorithm for context matching with dags, when the number of different context variables is fixed for the problem. NP-completeness is obtained when the terms are represented using the more general formalism of singleton tree grammars. As an ingredient of this proof, we also show that the special case of first-order matching with singleton tree grammars is decidable in polynomial time.
Adrià Gascón, Guillem Godoy, Manfred Schmidt-Schauß
LICS1