Publications (31)
WYS*: A DSL for Verified Secure Multi-party Computations
Aseem Rastogi, Nikhil Swamy, Michael Hicks
Secure multi-party computation (MPC) enables a set of mutually distrusting parties to cooperatively compute, using a cryptographic protocol, a function over their private data. Thi…
C to Checked C by 3C
Aravind Machiry, John Kastner, Matt McCutchen +3
Owing to the continued use of C (and C++), spatial safety violations (e.g., buffer overflows) still constitute one of today's most dangerous and prevalent security vulnerabilities.…
A Formal Model of Checked C
Liyi Li, Yiyun Liu, Deena L. Postol +3
We present a formal model of Checked C, a dialect of C that aims to enforce spatial memory safety. Our model pays particular attention to the semantics of dynamically sized, potent…
Build It, Break It, Fix It: Contesting Secure Development
Andrew Ruef, Michael Hicks, James Parker +3
Typical security contests focus on breaking or mitigating the impact of buggy systems. We present the Build-it Break-it Fix-it BIBIFI contest which aims to assess the ability to se…
Build It, Break It, Fix It: Contesting Secure Development
James Parker, Michael Hicks, Andrew Ruef +5
Typical security contests focus on breaking or mitigating the impact of buggy systems. We present the Build-it, Break-it, Fix-it (BIBIFI) contest, which aims to assess the ability…
LWeb: Information Flow Security for Multi-tier Web Applications
James Parker, Niki Vazou, Michael Hicks
This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enfor…
Quantitative Robustness Analysis of Quantum Programs (Extended Version)
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu +3
Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing w…
How We Built Cedar: A Verification-Guided Approach
Craig Disselkoen, Aaron Eline, Shaobo He +10
This paper presents verification-guided development (VGD), a software engineering process we used to build Cedar, a new policy language for expressive, fast, safe, and analyzable a…
Fat Pointers for Temporal Memory Safety of C
Jie Zhou, John Criswell, Michael Hicks
Temporal memory safety bugs, especially use-after-free and double free bugs, pose a major security threat to C programs. Real-world exploits utilizing these bugs enable attackers t…
Verified Optimization in a Quantum Intermediate Representation
Kesha Hietala, Robert Rand, Shih-Han Hung +2
We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum…
Incremental Computation with Names
Matthew A. Hammer, Jana Dunfield, Kyle Headley +4
Over the past thirty years, there has been significant progress in developing general-purpose, language-based approaches to incremental computation, which aims to efficiently updat…
Proving Quantum Programs Correct
Kesha Hietala, Robert Rand, Shih-Han Hung +2
As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? Thi…
Polymonadic Programming
Michael Hicks, Gavin Bierman, Nataliya Guts +2
Monads are a popular tool for the working functional programmer to structure effectful computations. This paper presents polymonads, a generalization of monads. Polymonads give the…
Garbage Collection Makes Rust Easier to Use: A Randomized Controlled Trial of the Bronze Garbage Collector
Michael Coblenz, Michelle Mazurek, Michael Hicks
Rust is a general-purpose programming language that is both type- and memory-safe. Rust does not use a garbage collector, but rather achieves these properties through a sophisticat…
A Counterexample-guided Approach to Finding Numerical Invariants
ThanhVu Nguyen, Timos Antopoulos, Andrew Ruef +1
Numerical invariants, e.g., relationships among numerical variables in a program, represent a useful class of properties to analyze programs. General polynomial invariants represen…
Quantifying vulnerability of secret generation using hyper-distributions (extended version)
Mário S. Alvim, Piotr Mardziel, Michael Hicks
Traditional approaches to Quantitative Information Flow (QIF) represent the adversary's prior knowledge of possible secret values as a single probability distribution. This represe…
Verified Compilation of Quantum Oracles
Liyi Li, Finn Voichick, Kesha Hietala +3
Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the l…
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)
Joseph W. Cutler, Craig Disselkoen, Aaron Eline +12
Cedar is a new authorization policy language designed to be ergonomic, fast, safe, and analyzable. Rather than embed authorization logic in an application's code, developers can wr…
A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm
Yuxiang Peng, Kesha Hietala, Runzhou Tao +4
Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful if computed answers are correct. While hardware-level…
Hybrid physics-AI outperforms numerical weather prediction for extreme precipitation nowcasting
Puja Das, August Posch, Nathan Barber +6
Precipitation nowcasting, critical for flood emergency and river management, has remained challenging for decades, although recent developments in deep generative modeling (DGM) su…
Morpheus: Safe and Flexible Dynamic Updates for SDNs
Karla Saur, Joseph Collard, Nate Foster +3
SDN controllers must be periodically modified to add features, improve performance, and fix bugs, but current techniques for implementing dynamic updates are inadequate. Simply hal…
Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
Finn Voichick, Liyi Li, Robert Rand +1
We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical computing. Qunity presents a unified syntax whe…
Composition of Near-Earth Asteroid 2008 EV5: Potential target for Robotic and Human Exploration
Vishnu Reddy, Lucille Le Corre, Michael Hicks +5
We observed potentially hazardous asteroid (PHA) 2008 EV5 in the visible (0.30-0.92 microns) and near-IR (0.75-2.5 microns) wavelengths to determine its surface composition. This a…
Summoning Demons: The Pursuit of Exploitable Bugs in Machine Learning
Rock Stevens, Octavian Suciu, Andrew Ruef +3
Governments and businesses increasingly rely on data analytics and machine learning (ML) for improving their competitive edge in areas such as consumer satisfaction, threat intelli…
Symphony: Expressive Secure Multiparty Computation with Coordination
Ian Sweet, David Darais, David Heath +3
Context: Secure Multiparty Computation (MPC) refers to a family of cryptographic techniques where mutually untrusting parties may compute functions of their private inputs while re…
A Language for Probabilistically Oblivious Computation
David Darais, Ian Sweet, Chang Liu +1
An oblivious computation is one that is free of direct and indirect information leaks, e.g., due to observable differences in timing and memory access patterns. This paper presents…
A Verified Optimizer for Quantum Circuits
Kesha Hietala, Robert Rand, Shih-Han Hung +2
We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level l…
What's the Over/Under? Probabilistic Bounds on Information Leakage
Ian Sweet, Jose Manuel Calderon Trilla, Chad Scherrer +2
Quantitative information flow (QIF) is concerned with measuring how much of a secret is leaked to an adversary who observes the result of a computation that uses it. Prior work has…
Evolving NoSQL Databases Without Downtime
Karla Saur, Tudor DumitraÅ, Michael Hicks
NoSQL databases like Redis, Cassandra, and MongoDB are increasingly popular because they are flexible, lightweight, and easy to work with. Applications that use these databases wil…
Evaluating Fuzz Testing
George Klees, Andrew Ruef, Benji Cooper +2
Fuzz testing has enjoyed great success at discovering security critical bugs in real software. Recently, researchers have devoted significant effort to devising new fuzzing techniq…
Evaluating Design Tradeoffs in Numeric Static Analysis for Java
Shiyi Wei, Piotr Mardziel, Andrew Ruef +2
Numeric static analysis for Java has a broad range of potentially useful applications, including array bounds checking and resource usage estimation. However, designing a scalable…