Complete List of Publications

A state-of-the-art, fully automated red-teaming tool that turns prompt diversity into an efficient black-box jailbreak strategy, exposing 5× more safety failures across leading LLMs with 10× fewer queries.

RAIDAR introduced divergence under rewriting, an interpretable signal that generalizes across domains and requires only black-box LLM access. Ask another LLM to rewrite the text: AI-generated text changes less because it lies closer to the rewriter’s statistical norm. The idea later extended to AI-generated video and audio.

TREX is a transfer-learning-based framework that automates learning execution semantics explicitly from functions' micro-traces (a form of under-constrained dynamic traces) and transfer the learned knowledge to match semantically similar functions. Evaluation on 1,472,066 function binaries from 13 popular software projects compiled with 4 optimizations (O0-O3) and 5 obfuscations for four archiectures (x86, x64, ARM, and MIPS) shows that TREX outperforms prior art by 7.8%, 7.2%, and 14.3% in matching accuracy and is 8x faster.

Applications often have fast-paced release schedules, but adoption of software dependency updates can lag by years, leaving applications susceptible to security risks and unexpected breakage.Upgradvisor is a system that largely automates software dependency updates a novel co-designed static analysis and dynamic tracing mechanism to gauge the scope and effect of dependency updates on an application.

With the emergence of microsecond-scale NVMe storage devices, the Linux kernel storage stack overhead has become significant, almost doubling access times. XRP is a framework that allows applications to execute user-defined storage functions, such as index lookups or aggregations, from an eBPF hook in the NVMe driver, safely bypassing most of the kernel’s storage stack.

Full-precision deep learning models are typically compressed, pruned, or quantized to run on edge devices. DIVA is a new evasive attack that exploits these differences in edge adaptation to trick the adapted model running on the edge, but will be virtually undetectable by the original model, which typically serves as the authoritative model version, used for validation, debugging and retraining.

Horizontal sharding is a decades-old technique to scale production databases. Neuroshard is the first system that learns shard assignments directly from the workload using reinforcement learning, and optimizes for multiple sharding objectives simultaneously.

Visual representations underlie object recognition tasks, but they often contain both robust and non-robust features. We develop an algorithm to estimate the causal effect for image classification, which is transportable (i.e., invariant) across source and target environments.

Extends our test-time defense to use multiple self-supervised learning tasks for attack reversal.

We propose a test-time defense that reverses adversarial attacks by restoring the intrinsic structures collatorally damaged by attack vectors. Our defense is still effective even if the attacker is aware of the defense mechanism. Since our defense is deployed during inference instead of training, it is compatible with pre-trained networks as well as most other defenses. Our results suggest deep networks are vulnerable to adversarial examples partly because their representations do not enforce the natural structure of images.

StateFormer recovers source-level types from stripped binaries leveraging transfer learning. Inspired by how human analysts reverse-engineer binaries, we propose a pretraining task called Generative State Modeling (GSM) to teach an ML model assembly code operational semantics, and then transfer the learned knowledge for type inference.

We identify inherent imprecision in prior causal tracing work, and build Argus, a novel system that differentiates weak and strong causal edges in the traced graphs for combating this imprecision. Evaluation shows that Argus effectively helps diagnose open spinning-cursor issues in modern MacOS applications.

This paper explores an approach inspired by the exokernel file systems to leverage BPF for new, super fast storage devices.

We introduce a framework for learning robust visual representations that generalize to new viewpoints, backgrounds, and scene contexts. Key insight is to steer generative models to manufacture interventions on features caused by confounding factors. Experiments, visualizations, and theoretical results show this method learns robust representations more consistent with the underlying causal relationships.

XDA is a transfer-learning-based binary disassembler. Key in XDA is to model the problem of going from bits to assembly code as a language translation problem. Evaluation on real-world binaries compiled by four compilers with different optimization levels shows that XDA achieves extremely high accuracy, substantially surpassing the prior art, and is 38 times faster than hand-written disassemblers such as IDA Pro.

We present both theoretical and empirical analyses that connect the adversarial robustness of a model to the number of tasks that it is trained on. Experiments on two datasets show that attack difficulty increases as the number of target tasks increase. Moreover, our results suggest that when models are trained on multiple tasks at once, they become more robust to adversarial attacks on individual tasks. While adversarial defense remains an open challenge, our results suggest that deep networks are vulnerable partly because they are trained on too few tasks.

Lambadata is a serverless computing system that enables developers to declare a cloud function’s data intents, including both data read and data written. Once data intents are made explicit, Lambadata performs a variety of optimizations to improve speed, including caching data locally and scheduling functions based on code and data locality.

We demonstrate a simple and effective method that changes the nuisance factors for a GAN to fool semantic segmentation models in a single step, even if the models have been adversarially trained for defense. It is the first method able to attack semantic segmentation models online, 100x faster than prior attacks. Earlier version of the paper is on arxiv.

We study the shift invariance of representations learned by CNNs and find that (1) state-of-the-art antialiasing improves local shift invariance but not global shift invariance; (2) horizontally shifted images have more similar representations than vertical translation; and (3) learned representations exhibit what we call 'feature arithemetic' properties that addition or substraction in the feature-space visualize to pixel-space addition or subtraction. [Results]

Presents a new attack that leverages classic buffer overruns to corrupt the weight matrices of deep neural nets and insert trojans on the fly, causing the nets to mispredict on certain trigger inputs. Key is a regularization method to minimize the amount of buffer overruns needed for the attack.

Egalito is a binary recompiler that leverages metadata widely present in modern binaries for full disassembly and transformations. We demonstrate nine binary tools including a novel continuous code randomization technique where Egalito transforms itself, and software emulation of the control-flow integrity in upcoming hardware

Morpheus is the first concurrency testing tool leveraging partial order sampling, a randomized testing method formally analyzed and empirically validated to provide strong probabilistic guarantees of error-detection, for real-world distributed systems. It found previously unknown errors in four Erlang systems including RabbitMQ and Mnesia, 11 total, all of which are flaws in their core protocols that may cause deadlocks, unexpected crashes, or inconsistenlivet states

Describes a blackbox way of verifying computer vision models leveraging the fact that pixel values are discreet and therefore finite. [arxiv]

CodeMason is an optimizing recompiler built atop Egalito.

Our experiments show that adversarial attacks such as PGD cause the deep representations of neural networks to shift closer to the 'false' class. Motivated by this observation, we propose to regularize the representation space under attack with metric learning to produce more robust classifiers. Key is to carefully select the samples for metric learning. Code is here.

Invited OSR paper that overviews our recent work on testing and verifying deep neural nets.

CACM research highlight on DeepXplore (https://cacm.acm.org/magazines/2019/11/240390-deepxplore).

Invited paper on DeepXplore as a SIGMobile GetMobile highlight paper (https://dl.acm.org/citation.cfm?id=3308767).

Describes Neuzz, a fuzzing tool that leverages neural nets to predict which input bytes to mutate to cover many different branches.

Describes YOLO, a system that leverages both cyber security techniques such as rebooting and physical system properties such as inertia to protect cyber physical systems.

AppFlow leverages machine learning to recognize UI screens and widgets, enabling developers to write intuitive, robust, and reusable UI tests that refer to canonical UI screens and widgets.

Neurify improves upon ReluVal with a tighter approximation of the output bounds via linear relaxation and refines overapproximated intermediate neuron output bounds using a LP solver.

Describes ReluVal, a system that uses symbolic interval analysis and iterative refinement to verify neural networks.

Presents POS, a concurrency testing approach that aims to uniformly sample the partial order of concurrent programs. Its core is an extremely simple priority-based scheduling algorithm. It provides exponentially better probabilistic guarantee of error detection than state-or-the-art randomized testing methods. Evaluation shows it finds concurrency bugs in real-world programs, such as Firefox's JavaScript engine, much faster than other methods.

Describes an approach called causal unlearning and a corresponding system called Karma to efficiently repair a polluted learning system.

Presents a study on how real-world concurrency errors can be exploited by attackers and our system Owl for understanding the security implications of concurrency errors and detecting the ones vulnerable to attacks.

Describes WeChat's system for handling occasional massive overloads.

DeepXplore was the first white-box testing tool to bring coverage-guided fuzzing and differential testing to neural networks. It introduced neuron coverage, uncovered thousands of flaws, helped launch a new research field, and influenced Google’s TensorFuzz.

Describes Shuffler, a system that continuously randomizes an application's binary code at runtime, defeating code-reuse attacks. Shuffler is fast: it shuffles all code within tens of milliseconds, whereas cutting-edge ROP attacks need 10--100x more time to discover gadgets. Shuffler is egalitarian: leveraging the insight that randomization doesn't require a higher privilege authority, Shuffler shuffles itself, reducing trusted computing base and making the approach applicable to kernels and hypervisors. Shuffler is deployable: its augmented binary analysis requires no modifications to OS, compilers, and linkers.

Describes Grandet, a storage system that greatly reduces the cost and complexity of deploying web applications in the cloud.

We formally specify what it means for a program to be crash-recoverable, build an automated verifier of this spec, and validate that the commit protocols of a number of industrial storage systems are crash-recoverable.

Describes LockIt, a system that makes lock-free data structures easy to verify.

Describes Crane, a state machine replication system that replicates general server programs for high availability. It does so transparently without requiring developers to modify their programs. Crane essentially provides Replication-as-a-Service.

Describes a nice application of Crane (our transparent Paxos system) for making dynamic program analysis more effective

Describes UNIC, a system that allows mutually distrusting users to deduplicate computations done by general programs.

This paper coined the term machine unlearning: the idea that models should efficiently forget selected training data and its influence. It helped launch a field that has grown from classical learning algorithms to deep neural networks and LLMs.

Describes AppDoctor, a powerful tool for detecting bugs in mobile apps.

StableMT introduced a new concurrency model built on a radical question: do parallel programs need exponentially many thread schedules? Reusing a small set of tested schedules across inputs makes production behavior more predictable, testable, and reliable.

Describes Parrot, a simple, deployable thread runtime system for improving reliability with low overhead. This is our most recent and best paper on stable and deterministic multithreading.

Describes NeonGoby, a system for effectively detecting errors in alias analysis, one of the most important and widely used program analyses.

A position paper describing our vision of stable multithreading, a radically new approach to making multithreading reliable.

Describes Woodpecker, a system that leverages path slicing to speed up symbolic execution. It enables users to check systems rules, and avoids checking program paths irrelevant to the rule, drastically reducing the amount of redundant work.

Technical report version of NeonGoby, a system for effectively detecting errors in alias analysis, one of the most important and widely used program analyses

Summarizes our recent research on stable multithreading systems that dramatically simplify the interleaving behaviors of threads, addressing fundamental, open problems to improve the reliability of multithreaded programs.

Describes a program analysis framework for analyzing multithreaded programs with high precision. The key idea is to statically analyze a multithreaded program w.r.t. only a small set of schedules to improve precision and then enforce these schedules at runtime for soundness.

Studies the security consequences of concurrency errors.

Describes Peregrine, a system for efficiently making threads deterministic, addressing a key open challenge within the field of deterministic execution.

Describes RacePro, a system for finding process races (e.g., multiple processes accessing a shared resource such as a file without proper synchronization).

Our most recent and best model checking paper. It describes a new reduction technique that decomposes a full distributed system into components and then explores the executions of these components in a divide-and-conquer way.

Studies the security consequences of concurrency errors.

Argues that process races (e.g., multiple processes accessing a shared resource such as a file without proper synchronization) are bad and that the research community has not given them their due share of attention.

Presents a crucial problem in data-parallel computing: how to evenly partition data, and sketches a solution to this problem.

Describes CODE, a system for automatically detecting software configuration errors. The key insight is to infer configuration access invariants that predict what access events follow what contexts.

Describes Tern, a system for making threads more deterministic and stable. The key idea is to memoize past schedules and reuse them when possible, much like the natural tendencies in animals and humans to repeat familiar routes to avoid possible hazards along unknown routes.

Describes LOOM, a live-workaround system for fixing races in live applications. LOOM is safe (live-update will not introduce new errors), fast (negligible overhead for most benchmarks), and flexible (able to fix all bugs evaluated).

A more complete description of LOOM compared to our OSDI '10 paper.

Describes how we found many copy-and-paste bugs in a large commercial code base.

Describes how we applied our in-situ model checking approach to find 10 protocol-level errors in three real distributed systems, including a production system that has been managing more than 100 thousand machines for over two years. Note this version has two minor calculation errors fixed.

Describes a version of eXplode for in-vivo model checking.

Describes a new replica placement strategy that uses multiple linear hash functions to achieve high performance, scalability, and availability.

Describes a distributed version of eXplode.

Describes our in-situ model checking approach, which made it easy to thoroughly check real systems. We applied eXplode to 17 storage systems and found serious data-loss errors in every system checked. This paper is my favorite in describing our model checking approach, which forms the basis of my PhD thesis work.

A journal version of our FiSC work, forwarded from OSDI 04.

Describes how we generated disks-of-death using symbolic execution. These disks, when mounted, can crash or take over control of your machine.

Describes a preliminary version of the eXplode storage system checker

FiSC leveraged model checking to systematically explore crash states beyond conventional testing. It found serious bugs in every file system checked—32 across ext3, JFS, and ReiserFS—including failures that could irrecoverably destroy entire directories, even the file-system root; most were patched within a day.

Describes how we can exploit the correlations of error messages emitted by static analysis tools to cluster false positives together, thus improve the effectiveness of the static analysis tools.

Describes an extensible and lightweight annotation system that allows programmers to write a small set of domain-specific annotations to effectively annotate large bodies of code.

Presents our study of the errors found using meta-compilation. Some interesting conclusions include drivers are up to three to seven times buggier than the rest of the kernel.