Showing 1–12 of 12 results for author: Mitchell, J C

De-amplifying Bias from Differential Privacy in Language Model Fine-tuning

Authors: Sanjari Srivastava, Piotr Mardziel, Zhikhun Zhang, Archana Ahlawat, Anupam Datta, John C Mitchell

Abstract: Fairness and privacy are two important values machine learning (ML) practitioners often seek to operationalize in models. Fairness aims to reduce model bias for social/demographic sub-groups. Privacy via differential privacy (DP) mechanisms, on the other hand, limits the impact of any individual's training data on the resulting model. The trade-offs between privacy and fairness goals of trustworth… ▽ More Fairness and privacy are two important values machine learning (ML) practitioners often seek to operationalize in models. Fairness aims to reduce model bias for social/demographic sub-groups. Privacy via differential privacy (DP) mechanisms, on the other hand, limits the impact of any individual's training data on the resulting model. The trade-offs between privacy and fairness goals of trustworthy ML pose a challenge to those wishing to address both. We show that DP amplifies gender, racial, and religious bias when fine-tuning large language models (LLMs), producing models more biased than ones fine-tuned without DP. We find the cause of the amplification to be a disparity in convergence of gradients across sub-groups. Through the case of binary gender bias, we demonstrate that Counterfactual Data Augmentation (CDA), a known method for addressing bias, also mitigates bias amplification by DP. As a consequence, DP and CDA together can be used to fine-tune models while maintaining both fairness and privacy. △ Less

Submitted 6 February, 2024; originally announced February 2024.

Serberus: Protecting Cryptographic Code from Spectres at Compile-Time

Authors: Nicholas Mosier, Hamed Nemati, John C. Mitchell, Caroline Trippel

Abstract: We present Serberus, the first comprehensive mitigation for hardening constant-time (CT) code against Spectre attacks (involving the PHT, BTB, RSB, STL and/or PSF speculation primitives) on existing hardware. Serberus is based on three insights. First, some hardware control-flow integrity (CFI) protections restrict transient control-flow to the extent that it may be comprehensively considered by s… ▽ More We present Serberus, the first comprehensive mitigation for hardening constant-time (CT) code against Spectre attacks (involving the PHT, BTB, RSB, STL and/or PSF speculation primitives) on existing hardware. Serberus is based on three insights. First, some hardware control-flow integrity (CFI) protections restrict transient control-flow to the extent that it may be comprehensively considered by software analyses. Second, conformance to the accepted CT code discipline permits two code patterns that are unsafe in the post-Spectre era. Third, once these code patterns are addressed, all Spectre leakage of secrets in CT programs can be attributed to one of four classes of taint primitives--instructions that can transiently assign a secret value to a publicly-typed register. We evaluate Serberus on cryptographic primitives in the OpenSSL, Libsodium, and HACL* libraries. Serberus introduces 21.3% runtime overhead on average, compared to 24.9% for the next closest state-of-the-art software mitigation, which is less secure. △ Less

Submitted 10 September, 2023; originally announced September 2023.

Comments: Authors' version; to appear in the Proceedings of the IEEE Symposium on Security and Privacy (S&P) 2024

Insights for post-pandemic pedagogy across one CS department

Authors: Maxwell Bigman, Yosefa Gilon, Jenny Han, John C Mitchell

Abstract: Adaptive remote instruction has led to important lessons for the future, including rediscovery of known pedagogical principles in new contexts and new insights for supporting remote learning. Studying one computer science department that serves residential and remote undergraduate and graduate students, we conducted interviews with stakeholders in the department (n=26) and ran a department-wide st… ▽ More Adaptive remote instruction has led to important lessons for the future, including rediscovery of known pedagogical principles in new contexts and new insights for supporting remote learning. Studying one computer science department that serves residential and remote undergraduate and graduate students, we conducted interviews with stakeholders in the department (n=26) and ran a department-wide student survey (n=102) during the four academic quarters from spring 2020 to spring 2021. Our case study outlines what the instructors did, summarizes what instructors and students say about courses during this period, and provides recommendations for CS departments with similar scope going forward. Specific insights address: (1) how instructional components are best structured for students; (2) how students are assessed for their learning; and (3) how students are supported in student-initiated components of learning. The institution is a large U.S. research university that has a history of online programs including online enrollment in regular on-campus courses and large-scale open enrollment courses. Our recommendations to instructors across the scope of this department may also be applicable to other institutions that provide technology-supported in-person instruction, remote enrollment, and hybrid courses combining both modalities. △ Less

Submitted 16 March, 2022; originally announced March 2022.

Model Checking Bitcoin and other Proof-of-Work Consensus Protocols

Authors: Max DiGiacomo-Castillo, Yiyun Liang, Advay Pal, John C. Mitchell

Abstract: The Bitcoin Backbone Protocol [GKL15] is an abstraction of the bitcoin proof-of-work consensus protocol. We use a model-checking tool (UPPAALSMC) to examine the concrete security of proof-ofwork consensus by varying protocol parameters and using an adversary that leverages the selfish mining strategy introduced in [GKL15]. We provide insights into modeling proof-of-work protocols and demonstrate t… ▽ More The Bitcoin Backbone Protocol [GKL15] is an abstraction of the bitcoin proof-of-work consensus protocol. We use a model-checking tool (UPPAALSMC) to examine the concrete security of proof-ofwork consensus by varying protocol parameters and using an adversary that leverages the selfish mining strategy introduced in [GKL15]. We provide insights into modeling proof-of-work protocols and demonstrate tradeoffs between operating parameters. Applying this methodology to protocol design options, we show that the uniform tie-breaking rule from [ES18] decreases the failure rate of the chain quality property, but increases the failure rate of the common prefix property. This tradeoff illustrates how design decisions affect protocol properties, within a range of concrete operating conditions, in a manner that is not evident from prior asymptotic analysis. △ Less

Submitted 16 July, 2020; originally announced July 2020.

Resources: A Safe Language Abstraction for Money

Authors: Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar

Abstract: Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract programming languages must allow users to write expressive programs that manage and transfer assets, yet provide strong protection against sophisticated attacks. Addressing this need, we present flexible and reliable abstr… ▽ More Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract programming languages must allow users to write expressive programs that manage and transfer assets, yet provide strong protection against sophisticated attacks. Addressing this need, we present flexible and reliable abstractions for programming with digital currency in the Move language [Blackshear et al. 2019]. Move uses novel linear [Girard 1987] resource types with semantics drawing on C++11 [Stroustrup 2013] and Rust [Matsakis and Klock 2014]: when a resource value is assigned to a new memory location, the location previously holding it must be invalidated. In addition, a resource type can only be created or destroyed by procedures inside its declaring module. We present an executable bytecode language with resources and prove that it enjoys resource safety, a conservation property for program values that is analogous to conservation of mass in the physical world. △ Less

Submitted 23 July, 2020; v1 submitted 10 April, 2020; originally announced April 2020.

Privacy-Preserving Shortest Path Computation

Authors: David J. Wu, Joe Zimmerman, Jérémy Planul, John C. Mitchell

Abstract: Navigation is one of the most popular cloud computing services. But in virtually all cloud-based navigation systems, the client must reveal her location and destination to the cloud service provider in order to learn the fastest route. In this work, we present a cryptographic protocol for navigation on city streets that provides privacy for both the client's location and the service provider's rou… ▽ More Navigation is one of the most popular cloud computing services. But in virtually all cloud-based navigation systems, the client must reveal her location and destination to the cloud service provider in order to learn the fastest route. In this work, we present a cryptographic protocol for navigation on city streets that provides privacy for both the client's location and the service provider's routing data. Our key ingredient is a novel method for compressing the next-hop routing matrices in networks such as city street maps. Applying our compression method to the map of Los Angeles, for example, we achieve over tenfold reduction in the representation size. In conjunction with other cryptographic techniques, this compressed representation results in an efficient protocol suitable for fully-private real-time navigation on city streets. We demonstrate the practicality of our protocol by benchmarking it on real street map data for major cities such as San Francisco and Washington, D.C. △ Less

Submitted 10 January, 2016; originally announced January 2016.

Comments: Extended version of NDSS 2016 paper

A Symbolic Logic with Concrete Bounds for Cryptographic Protocols

Authors: Anupam Datta, Joseph Y. Halpern, John C. Mitchell, Arnab Roy, Shayak Sen

Abstract: We present a formal logic for quantitative reasoning about security properties of network protocols. The system allows us to derive concrete security bounds that can be used to choose key lengths and other security parameters. We provide axioms for reasoning about digital signatures and random nonces, with security properties based on the concrete security of signature schemes and pseudorandom num… ▽ More We present a formal logic for quantitative reasoning about security properties of network protocols. The system allows us to derive concrete security bounds that can be used to choose key lengths and other security parameters. We provide axioms for reasoning about digital signatures and random nonces, with security properties based on the concrete security of signature schemes and pseudorandom number generators (PRG). The formal logic supports first-order reasoning and reasoning about protocol invariants, taking concrete security bounds into account. Proofs constructed in our logic also provide conventional asymptotic security guarantees because of the way that concrete bounds accumulate in proofs. As an illustrative example, we use the formal logic to prove an authentication property with concrete bounds of a signature-based challenge-response protocol. △ Less

Submitted 23 November, 2015; originally announced November 2015.

ACM Class: F.3.1; C.2.2

Data Representation and Compression Using Linear-Programming Approximations

Authors: Hristo S. Paskov, John C. Mitchell, Trevor J. Hastie

Abstract: We propose `Dracula', a new framework for unsupervised feature selection from sequential data such as text. Dracula learns a dictionary of $n$-grams that efficiently compresses a given corpus and recursively compresses its own dictionary; in effect, Dracula is a `deep' extension of Compressive Feature Learning. It requires solving a binary linear program that may be relaxed to a linear program. Bo… ▽ More We propose `Dracula', a new framework for unsupervised feature selection from sequential data such as text. Dracula learns a dictionary of $n$-grams that efficiently compresses a given corpus and recursively compresses its own dictionary; in effect, Dracula is a `deep' extension of Compressive Feature Learning. It requires solving a binary linear program that may be relaxed to a linear program. Both problems exhibit considerable structure, their solution paths are well behaved, and we identify parameters which control the depth and diversity of the dictionary. We also discuss how to derive features from the compressed documents and show that while certain unregularized linear models are invariant to the structure of the compressed dictionary, this structure may be used to regularize learning. Experiments are presented that demonstrate the efficacy of Dracula's features. △ Less

Submitted 2 May, 2016; v1 submitted 20 November, 2015; originally announced November 2015.

IFC Inside: Retrofitting Languages with Dynamic Information Flow Control (Extended Version)

Authors: Stefan Heule, Deian Stefan, Edward Z. Yang, John C. Mitchell, Alejandro Russo

Abstract: Many important security problems in JavaScript, such as browser extension security, untrusted JavaScript libraries and safe integration of mutually distrustful websites (mash-ups), may be effectively addressed using an efficient implementation of information flow control (IFC). Unfortunately existing fine-grained approaches to JavaScript IFC require modifications to the language semantics and its… ▽ More Many important security problems in JavaScript, such as browser extension security, untrusted JavaScript libraries and safe integration of mutually distrustful websites (mash-ups), may be effectively addressed using an efficient implementation of information flow control (IFC). Unfortunately existing fine-grained approaches to JavaScript IFC require modifications to the language semantics and its engine, a non-goal for browser applications. In this work, we take the ideas of coarse-grained dynamic IFC and provide the theoretical foundation for a language-based approach that can be applied to any programming language for which external effects can be controlled. We then apply this formalism to server- and client-side JavaScript, show how it generalizes to the C programming language, and connect it to the Haskell LIO system. Our methodology offers design principles for the construction of information flow control systems when isolation can easily be achieved, as well as compositional proofs for optimized concrete implementations of these systems, by relating them to their isolated variants. △ Less

Submitted 16 January, 2015; originally announced January 2015.

Comments: Extended version of POST'15 paper; 31 pages

Flexible Dynamic Information Flow Control in the Presence of Exceptions

Authors: Deian Stefan, Alejandro Russo, John C. Mitchell, David Mazières

Abstract: We describe a new, dynamic, floating-label approach to language-based information flow control. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality. The current label floats to exceed the labels of all data observed and restricts what can be modified. Unlike other language-based work, LIO also bounds the current label with a current clearance t… ▽ More We describe a new, dynamic, floating-label approach to language-based information flow control. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality. The current label floats to exceed the labels of all data observed and restricts what can be modified. Unlike other language-based work, LIO also bounds the current label with a current clearance that provides a form of discretionary access control. Computations may encapsulate and pass around the results of computations with different labels. In addition, the LIO monad offers a simple form of labeled mutable references and exception handling. We give precise semantics and prove confidentiality and integrity properties of a call-by-name λ-calculus and provide an implementation in Haskell. △ Less

Submitted 5 July, 2012; originally announced July 2012.

ACM Class: D.4.6; D.1.1; D.3.3

Driving magnetic order in a manganite by ultrafast lattice excitation

Authors: M. Först, R. I. Tobey, S. Wall, H. Bromberger, V. Khanna, A. L. Cavalieri, Y. -D. Chuang, W. S. Lee, R. Moore, W. F. Schlotter, J. J. Turner, O. Krupin, M. Trigo, J. C. Mitchell, S. S. Dhesi, J. P. Hill, A. Cavalleri

Abstract: Optical control of magnetism, of interest for high-speed data processing and storage, has only been demonstrated with near-infrared excitation to date. However, in absorbing materials, such high photon energies can lead to significant dissipation, making switch back times long and miniaturization challenging. In manganites, magnetism is directly coupled to the lattice, as evidenced by the response… ▽ More Optical control of magnetism, of interest for high-speed data processing and storage, has only been demonstrated with near-infrared excitation to date. However, in absorbing materials, such high photon energies can lead to significant dissipation, making switch back times long and miniaturization challenging. In manganites, magnetism is directly coupled to the lattice, as evidenced by the response to external and chemical pressure, or to ferroelectric polarization. Here, femtosecond mid-infrared pulses are used to excite the lattice in La0.5Sr1.5MnO4 and the dynamics of electronic order are measured by femtosecond resonant soft x-ray scattering with an x-ray free electron laser. We observe that magnetic and orbital orders are reduced by excitation of the lattice. This process, which occurs within few picoseconds, is interpreted as relaxation of the complex charge-orbital-spin structure following a displacive exchange quench - a prompt shift in the equilibrium value of the magnetic and orbital order parameters after the lattice has been distorted. A microscopic picture of the underlying unidirectional lattice displacement is proposed, based on nonlinear rectification of the directly-excited vibrational field, as analyzed in the specific lattice symmetry of La0.5Sr1.5MnO4. Control of magnetism through ultrafast lattice excitation has important analogies to the multiferroic effect and may serve as a new paradigm for high-speed optomagnetism. △ Less

Submitted 19 May, 2011; originally announced May 2011.

Comments: 10 pages manuscript, 4 figures

Journal ref: Physical Review B, Vol. 84, 241104(R) (2011)

A Learning-Based Approach to Reactive Security

Authors: Adam Barth, Benjamin I. P. Rubinstein, Mukund Sundararajan, John C. Mitchell, Dawn Song, Peter L. Bartlett

Abstract: Despite the conventional wisdom that proactive security is superior to reactive security, we show that reactive security can be competitive with proactive security as long as the reactive defender learns from past attacks instead of myopically overreacting to the last attack. Our game-theoretic model follows common practice in the security literature by making worst-case assumptions about the at… ▽ More Despite the conventional wisdom that proactive security is superior to reactive security, we show that reactive security can be competitive with proactive security as long as the reactive defender learns from past attacks instead of myopically overreacting to the last attack. Our game-theoretic model follows common practice in the security literature by making worst-case assumptions about the attacker: we grant the attacker complete knowledge of the defender's strategy and do not require the attacker to act rationally. In this model, we bound the competitive ratio between a reactive defense algorithm (which is inspired by online learning theory) and the best fixed proactive defense. Additionally, we show that, unlike proactive defenses, this reactive strategy is robust to a lack of information about the attacker's incentives and knowledge. △ Less

Submitted 21 December, 2009; v1 submitted 6 December, 2009; originally announced December 2009.

Comments: 22 pages, 4 figures; full version of paper to be published in Financial Cryptography and Data Security 2010 (FC'10)