arXiv subjects

Joseph P. Near

Publications and source records attributed to Joseph P. Near.

31 records · Page 2Linked to original sources

arXiv2024

We Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values

Concurrent distributed systems are notoriously difficult to construct and reason about. Choreographic programming is a recent paradigm that describes a distributed system in a single global program called a choreography. Choreographies simplify reasoning about distributed systems and can ensure deadlock freedom by static analysis. In previous choreographic programming languages, each value is located at a single party, and the programmer is expected to insert special untyped "select" operations to ensure that all parties follow the same communication pattern. We present He-Lambda-Small, a new choreographic programming language with Multiply Located Values. He-Lambda-Small allows multicasting to a set of parties, and the resulting value will be located at all of them. This approach enables a simple and elegant alternative to "select": He-Lambda-Small requires that the guard for a conditional be located at all of the relevant parties. In He-Lambda-Small, checking that a choreography is well-typed suffices to show that it is deadlock-free. We present several case studies that demonstrate the use of multiply-located values to concisely encode tricky communication patterns described in previous work without the use of "select" or redundant communication.

cs.PL↗

arXiv2022

Improving Utility for Privacy-Preserving Analysis of Correlated Columns using Pufferfish Privacy

Surveys are an important tool for many areas of social science research, but privacy concerns can complicate the collection and analysis of survey data. Differentially private analyses of survey data can address these concerns, but at the cost of accuracy - especially for high-dimensional statistics. We present a novel privacy mechanism, the Tabular DDP Mechanism, designed for high-dimensional statistics with incomplete correlation. The Tabular DDP Mechanism satisfies dependent differential privacy, a variant of Pufferfish privacy; it works by building a causal model of the sensitive data, then calibrating noise to the level of correlation between statistics. An empirical evaluation on survey data shows that the Tabular DDP Mechanism can significantly improve accuracy over the Laplace mechanism.

cs.CR↗

arXiv2022

Backpropagation Clipping for Deep Learning with Differential Privacy

We present backpropagation clipping, a novel variant of differentially private stochastic gradient descent (DP-SGD) for privacy-preserving deep learning. Our approach clips each trainable layer's inputs (during the forward pass) and its upstream gradients (during the backward pass) to ensure bounded global sensitivity for the layer's gradient; this combination replaces the gradient clipping step in existing DP-SGD variants. Our approach is simple to implement in existing deep learning frameworks. The results of our empirical evaluation demonstrate that backpropagation clipping provides higher accuracy at lower values for the privacy parameter $ε$ compared to previous work. We achieve 98.7% accuracy for MNIST with $ε= 0.07$ and 74% accuracy for CIFAR-10 with $ε= 3.64$.

cs.LG↗

arXiv2022

Prediction Sensitivity: Continual Audit of Counterfactual Fairness in Deployed Classifiers

As AI-based systems increasingly impact many areas of our lives, auditing these systems for fairness is an increasingly high-stakes problem. Traditional group fairness metrics can miss discrimination against individuals and are difficult to apply after deployment. Counterfactual fairness describes an individualized notion of fairness but is even more challenging to evaluate after deployment. We present prediction sensitivity, an approach for continual audit of counterfactual fairness in deployed classifiers. Prediction sensitivity helps answer the question: would this prediction have been different, if this individual had belonged to a different demographic group -- for every prediction made by the deployed model. Prediction sensitivity can leverage correlations between protected status and other features and does not require protected status information at prediction time. Our empirical results demonstrate that prediction sensitivity is effective for detecting violations of counterfactual fairness.

cs.LG↗

arXiv2021

Solo: A Lightweight Static Analysis for Differential Privacy

All current approaches for statically enforcing differential privacy in higher order languages make use of either linear or relational refinement types. A barrier to adoption for these approaches is the lack of support for expressing these "fancy types" in mainstream programming languages. For example, no mainstream language supports relational refinement types, and although Rust and modern versions of Haskell both employ some linear typing techniques, they are inadequate for embedding enforcement of differential privacy, which requires "full" linear types a la Girard. We propose a new type system that enforces differential privacy, avoids the use of linear and relational refinement types, and can be easily embedded in mainstream richly typed programming languages such as Scala, OCaml and Haskell. We demonstrate such an embedding in Haskell, demonstrate its expressiveness on case studies, and prove that our type-based enforcement of differential privacy is sound.

cs.PL↗

arXiv2021

Chorus: a Programming Framework for Building Scalable Differential Privacy Mechanisms

Differential privacy is fast becoming the gold standard in enabling statistical analysis of data while protecting the privacy of individuals. However, practical use of differential privacy still lags behind research progress because research prototypes cannot satisfy the scalability requirements of production deployments. To address this challenge, we present Chorus, a framework for building scalable differential privacy mechanisms which is based on cooperation between the mechanism itself and a high-performance production database management system (DBMS). We demonstrate the use of Chorus to build the first highly scalable implementations of complex mechanisms like Weighted PINQ, MWEM, and the matrix mechanism. We report on our experience deploying Chorus at Uber, and evaluate its scalability on real-world queries.

cs.CR↗

arXiv2020

PrivFramework: A System for Configurable and Automated Privacy Policy Compliance

Today's massive scale of data collection coupled with recent surges of consumer data leaks has led to increased attention towards data privacy and related risks. Conventional data privacy protection systems focus on reducing custodial risk and lack features empowering data owners. As an end user there are limited options available to specify and enforce one's own privacy preferences over their data. To address these concerns we present PrivFramework, a user-configurable frame-work for automated privacy policy compliance. PrivFramework allows data owners to write powerful privacy policies to protect their data and automatically enforces these policies against analysis programs written in Python. Using static-analysis PrivFramework automatically checks authorized analysis programs for compliance to user-defined policies.

cs.CR↗

arXiv2020

Towards Auditability for Fairness in Deep Learning

Group fairness metrics can detect when a deep learning model behaves differently for advantaged and disadvantaged groups, but even models that score well on these metrics can make blatantly unfair predictions. We present smooth prediction sensitivity, an efficiently computed measure of individual fairness for deep learning models that is inspired by ideas from interpretability in deep learning. smooth prediction sensitivity allows individual predictions to be audited for fairness. We present preliminary experimental results suggesting that smooth prediction sensitivity can help distinguish between fair and unfair predictions, and that it may be helpful in detecting blatantly unfair predictions from "group-fair" models.

cs.LG↗

arXiv2020

DuetSGX: Differential Privacy with Secure Hardware

Differential privacy offers a formal privacy guarantee for individuals, but many deployments of differentially private systems require a trusted third party (the data curator). We propose DuetSGX, a system that uses secure hardware (Intel's SGX) to eliminate the need for a trusted data curator. Data owners submit encrypted data that can be decrypted only within a secure enclave running the DuetSGX system, ensuring that sensitive data is never available to the data curator. Analysts submit queries written in the Duet language, which is specifically designed for verifying that programs satisfy differential privacy; DuetSGX uses the Duet typechecker to verify that each query satisfies differential privacy before running it. DuetSGX therefore provides the benefits of local differential privacy and central differential privacy simultaneously: noise is only added to final results, and there is no trusted third party. We have implemented a proof-of-concept implementation of DuetSGX and we release it as open-source.

cs.CR↗

arXiv2020

Towards a Measure of Individual Fairness for Deep Learning

Deep learning has produced big advances in artificial intelligence, but trained neural networks often reflect and amplify bias in their training data, and thus produce unfair predictions. We propose a novel measure of individual fairness, called prediction sensitivity, that approximates the extent to which a particular prediction is dependent on a protected attribute. We show how to compute prediction sensitivity using standard automatic differentiation capabilities present in modern deep learning frameworks, and present preliminary empirical results suggesting that prediction sensitivity may be effective for measuring bias in individual predictions.

cs.AI↗

arXiv2019

Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy

During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by an expert in the field. Language-based techniques have been proposed for fully automating proofs of differential privacy via type system design, however these results have lagged behind advances in differentially-private algorithms, leaving a noticeable gap in programs which can be automatically verified while also providing state-of-the-art bounds on privacy. We propose Duet, an expressive higher-order language, linear type system and tool for automatically verifying differential privacy of general-purpose higher-order programs. In addition to general purpose programming, Duet supports encoding machine learning algorithms such as stochastic gradient descent, as well as common auxiliary data analysis tasks such as clipping, normalization and hyperparameter tuning - each of which are particularly challenging to encode in a statically verified differential privacy framework. We present a core design of the Duet language and linear type system, and complete key proofs about privacy for well-typed programs. We then show how to extend Duet to support realistic machine learning applications and recent variants of differential privacy which result in improved accuracy for many practical differentially private algorithms. Finally, we implement several differentially private machine learning algorithms in Duet which have never before been automatically verified by a language-based tool, and we present experimental results which demonstrate the benefits of Duet's language design in terms of accuracy of trained machine learning models.

cs.PL↗

arXiv2019

Data Capsule: A New Paradigm for Automatic Compliance with Data Privacy Regulations

The increasing pace of data collection has led to increasing awareness of privacy risks, resulting in new data privacy regulations like General data Protection Regulation (GDPR). Such regulations are an important step, but automatic compliance checking is challenging. In this work, we present a new paradigm, Data Capsule, for automatic compliance checking of data privacy regulations in heterogeneous data processing infrastructures. Our key insight is to pair up a data subject's data with a policy governing how the data is processed. Specified in our formal policy language: PrivPolicy, the policy is created and provided by the data subject alongside the data, and is associated with the data throughout the life-cycle of data processing (e.g., data transformation by data processing systems, data aggregation of multiple data subjects' data). We introduce a solution for static enforcement of privacy policies based on the concept of residual policies, and present a novel algorithm based on abstract interpretation for deriving residual policies in PrivPolicy. Our solution ensures compliance automatically, and is designed for deployment alongside existing infrastructure. We also design and develop PrivGuard, a reference data capsule manager that implements all the functionalities of Data Capsule paradigm.

cs.CY↗

arXiv2018

Towards Practical Differential Privacy for SQL Queries

Differential privacy promises to enable general data analytics while protecting individual privacy, but existing differential privacy mechanisms do not support the wide variety of features and databases used in real-world SQL-based analytics systems. This paper presents the first practical approach for differential privacy of SQL queries. Using 8.1 million real-world queries, we conduct an empirical study to determine the requirements for practical differential privacy, and discuss limitations of previous approaches in light of these requirements. To meet these requirements we propose elastic sensitivity, a novel method for approximating the local sensitivity of queries with general equijoins. We prove that elastic sensitivity is an upper bound on local sensitivity and can therefore be used to enforce differential privacy using any local sensitivity-based mechanism. We build FLEX, a practical end-to-end system to enforce differential privacy for SQL queries using elastic sensitivity. We demonstrate that FLEX is compatible with any existing database, can enforce differential privacy for real-world SQL queries, and incurs negligible (0.03%) performance overhead.

cs.CR↗