Publications

To our knowledge, ProAct is the first proactive jailbreak defense. Its decoy responses make the attacker’s model believe a jailbreak succeeded, stopping iterative searches early. ProAct cuts attack success rates by up to 94% without harming utility; combined with existing defenses, it reduces them to 0%.

An official, unmodified deep-learning compiler can silently change model semantics enough to activate a backdoor that is absent before compilation. The attack reaches 100% success after compilation, and a survey of popular Hugging Face models finds naturally occurring triggers in 31 of 100 models.

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.

Software vulnerabilities like buffer overflows can let attackers backdoor models after deployment. Our proof-of-concept attacks use small, contiguous weight patches that, when applied to a running model, cause mispredictions on trigger inputs while largely preserving normal accuracy.

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

A neural network can get most test examples right yet fail dangerously in unusual situations. This invited overview presents our five testing and verification tools, using neuron coverage to expose errors and formal analysis to prove robustness under specified input transformations and bounds.

Lighting changes or rotation can fool vision models. VeriVis provides the first blackbox verification of a broad range of such properties, exploiting discrete pixels to exhaustively check specified transformations of a given image. arXiv

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

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.

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.

Test-time adaptation can handle more than pixel corruption by guiding reverse diffusion with the model’s uncertainty while preserving each image’s style and content. The method adjusts inputs rather than weights and consistently improves recognition across corruption, rendition, sketch, and stylized shifts.

Latent visual tokens become interpretable when their semantics are carried through the transformer and matched to natural-language explanations—without new training data. Those explanations also become a control surface for editing model reasoning and reducing reliance on bias or spurious correlations.

A convolutional prompt gives test-time adaptation the structural bias that an unconstrained pixel prompt lacks. Using under 1% as many trainable parameters limits overfitting without labels and improves robustness across out-of-distribution visual tasks by up to 5.87%.

Natural images provide dense equivariance constraints that can be enforced at inference time, letting a frozen model adapt its defense to each input. Restoring feature equivariance improves adversarial robustness across recognition, semantic segmentation, and instance segmentation on four datasets.

A recognition model should be right about both its label and its reason. Transferring language-model rationales into visual prompts improves this stricter “doubly right” objective and carries those explanations to unseen tasks and datasets.

Masked-autoencoder reconstruction loss doubles as a signal for detecting adversarial inputs and as a guide for repairing them, without changing frozen model weights. The method averages 82% detection across eight attacks and substantially raises robust accuracy against previously unseen attacks.

Zero-shot robustness depends as much on how a foundation model is adapted as on the loss used to adapt it. Text-guided contrastive adversarial training, paired with the right choice between fine-tuning and visual prompting, improves average robustness by 31 points across ImageNet and 15 transfer datasets.

DIVA exposes a new vulnerability created by adapting full-precision models for edge deployment: subtle behavioral gaps let an attacker fool the adapted model while remaining benign to the authoritative original used for validation. Using differential testing, it is 1.9–4.2× more likely than PGD to evade detection.

Image representations mix robust object features with spurious cues, such as backgrounds and textures, that can fail in new environments. We estimate causal effects from these representations to improve generalization.

Extends our attack-reversal defense with multiple self-supervised tasks, improving both robustness and clean accuracy.

Adversarial perturbations damage more than a classifier’s final prediction: they also disturb the image’s incidental natural structure. In an early use of test-time adaptation for adversarial defense, the method restores that structure at inference, undoing diverse attacks—even when the attacker knows the defense—without retraining pretrained models.

Image classifiers often rely on spurious context and fail in new settings. We steer generative models to vary backgrounds and viewpoints while preserving object categories, creating causal interventions that improve robustness and generalization.

Previous attacks could take tens of seconds to generate one image that fools a segmentation model. We train a GAN to change color, lighting, and texture while preserving scene layout, generating attacks in one pass over 100× faster and fooling even adversarially trained models.

Deep networks may be fragile partly because they are trained too narrowly. Through theory and experiments, we show that learning multiple tasks improves adversarial robustness, and that attacks become harder as the number of targeted tasks grows.

Moving objects within images changes CNN representations. Our visualizations show that antialiasing helps with small shifts but does little for large ones, and horizontal shifts preserve more similarity than vertical shifts. Feature arithmetic in some layers can add or remove objects in reconstructed images. Results

PGD attacks do not merely flip predictions; they pull internal representations toward the wrong class. The paper turns that observation into a metric-learning regularizer that strengthens robustness and helps detect previously unseen adversarial examples.

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

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.

Tracing five repair agents across 500 real bugs reveals why benchmark wins do not always translate into sound patches: weak test generation, skipped regression tests, and primitive tooling encourage verbose, overfit fixes. The study argues for shifting effort toward early reproduction and validation.

Rather than treating kernel crashes like ordinary bug reports, the agent follows an execution-grounded developer workflow: inspect logs, form hypotheses, patch, reproduce, and refine. It repairs 54.5% of crashes without localization and 65% when given the correct file.

A continuously refreshed kernel-crash benchmark keeps evaluation ahead of model knowledge cutoffs, while a standardized execution environment makes agent comparisons fair and scalable. It exposes a sizable contamination gap and shows that execution feedback improves crash resolution by 29%.

The key diagnosis is that coding agents leave behind speculative and abandoned edits from their search trajectories. Minimizing those trajectories cuts functionally unnecessary code by 17.9–32.9% across agent scaffolds with negligible regression, while using about half the validation cost of delta-debugging baselines.

Combining LLM-directed search with classic program analysis lets one analysis follow privilege checks across services and seven programming languages. The system found 24 zero-day privilege-escalation vulnerabilities with 81% precision and 85% recall, then uncovered 18 more vulnerabilities in other domains.

Small coding models can become more capable by mastering one repository rather than training broadly across many. Repository-specific experience lets a 4B model outperform models up to 8× larger on average across bug fixing, test generation, and feature implementation, with lower inference costs than task-centric training.

Code edits become more robust when a language model first induces explicit transformation rules from before-and-after examples instead of learning an opaque end-to-end mapping. Those reusable meta-rules improve editing performance, robustness, and functional correctness across models and applications.

Separate security and functionality benchmarks draw from different code distributions, creating a shortcut: a model can appear both safe and capable by avoiding security-sensitive code. CWEval is, to our knowledge, the first benchmark to apply outcome-driven functionality and security tests to the same security-critical programs, distinguishing genuinely secure coding from avoidance.

A reproducible kernel-development environment and a benchmark built from real Syzkaller crashes make systems-level coding agents measurable. Early baselines solve only 0.72% of unassisted cases and 5.38% with the buggy file disclosed, defining a demanding frontier for machine learning on foundational software.

Rubber-duck-style monologues teach a compact code model to connect static text with functions, statement effects, and execution behavior. With 6.7 billion parameters, the resulting model rivals or surpasses GPT-3.5 on generation and execution reasoning while improving debugging and self-refinement.

Smart-contract fuzzers struggle to reach bugs hidden behind complex transaction sequences. A foundation model chooses when to use concolic execution and generates fuzz targets, then uses compiler and runtime feedback to correct hallucinated code. The system uncovered a protocol vulnerability missed by eleven tools and multiple audits.

Semantics-preserving program transformations can be treated as a mathematical symmetry group and built directly into attention. Encoding that structural prior yields faster generalization and outperforms leading code models, including GPT-4, on five program-analysis tasks without pretraining.

Smart-contract invariants often live jointly in code and natural-language transaction intent. Tiered multimodal reasoning turns both into executable checks, localizing 119 previously unknown bugs; six of eight sampled reports were fixed, including five confirmed as high severity.

TREX turns deliberately imprecise forced-execution traces into useful supervision: they teach a model enough instruction behavior to recognize equivalent functions despite changes in architecture, optimization, or obfuscation. Across more than 1.4 million binaries, it improved matching accuracy in all three settings and ran eight times faster than prior art.

Pretraining on dynamic memory value flows teaches a model enough execution semantics to infer binary memory dependencies statically. The resulting analysis is 1.5× more precise and 3.5× faster than prior work, and its representations also support signature recovery and indirect-call matching.

Compilation often strips type information from binaries. Inspired by analysts’ mental execution of code, StateFormer introduces Generative State Modeling to learn instruction effects during pretraining, then fine-tunes to recover source-level types.

XDA was one of the early works to apply pretrained language models to software analysis. It learns the structure of binary code through self-supervised pretraining, then fine-tunes for accurate, robust disassembly across compilers and optimization settings.

Random input mutations often leave fuzzers stuck testing the same code. NEUZZ introduces the first scalable neural program smoothing technique, learning a smooth model of branching behavior whose gradients guide mutations toward unexplored code. It found 31 previously unknown bugs.

Rare prompts elicit model-specific responses that often survive fine-tuning because ordinary training gives those regions little attention. Optimizing these prompts creates fingerprints without changing model weights, allowing black-box lineage checks after adaptations such as supervised fine-tuning, LoRA, and quantization.

This is the first large-scale study to measure AI-generated malicious email in the wild, using pre-ChatGPT messages as a real-world calibration baseline. Its most conservative detector estimates that at least 51% of spam and 14% of business-email-compromise messages in the study’s final month were LLM-generated.

Machine-generated text tends to change less than human writing when another language model rewrites it. Training the rewriter to amplify that gap produces a detector that generalizes across 21 domains and remains markedly stronger under distribution shift and adversarial attack.

A 1.3-million-sample voice benchmark reveals that leading deepfake-audio detectors lean on fragile high-frequency cues. Training selectively against attacks on those frequencies improves accuracy by 29.3% on corrupted and adversarial samples, turning the discovered weakness into a targeted defense.

Video detectors often struggle with unfamiliar generators. This training-free framework lets vision-language models select tools such as optical flow and depth estimation, then refine structured prompts using feedback. The resulting detector combines explicit visual evidence with model reasoning to identify diffusion-generated videos.

Grammar-preserving word substitutions, selected through transferable language-model embeddings, form a realistic black-box attack on AI-text detectors. The attack fools every evaluated detector by up to 99% while preserving human-perceived quality, and its examples can train more robust detectors.

Attacking a stochastic diffusion pipeline end to end is ineffective; guiding perturbations at internal representations makes detector evasion practical. The resulting black-box attack cuts accuracy by up to 69 points, reaches 91–100-point drops with white-box access, and transfers to unseen generators.

Image-level deepfake detectors miss the temporal evidence that distinguishes generated video, especially outside their training domain. Pairing diffusion-derived frame representations with temporal modeling reaches 93.7% in-domain accuracy and improves out-of-domain detection by as much as 16 points.

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.

Differential-privacy budget is a nonrenewable computing resource, so scheduling it for fairness can leave useful training capacity stranded. Casting allocation as a multidimensional privacy knapsack yields near-efficient schedules and runs 1.3–1.7× more jobs on an Alibaba-derived workload, with an explicit fairness tradeoff.

On-device ML model accuracy drift is often a shared, diagnosable failure rather than an isolated device problem. By detecting affected device groups, finding their common root cause, and adapting specifically to it, Nazar improves model accuracy by up to 19.4% without asking users for feedback.

A lineage graph turns families of fine-tuned, quantized, and distilled models into manageable versions rather than isolated files. Sharing parameters across that graph cuts storage by up to 7×, while model-update workflows helped practitioners finish a task three times faster.

Distributed systems have too many event orderings to test exhaustively. Morpheus is the first tool to apply partial order sampling to real-world distributed systems, combining its probabilistic guarantees with conflict analysis to focus on orderings that affect outcomes. It found 11 previously unknown protocol bugs in four Erlang systems, including RabbitMQ and Mnesia.

POS samples concurrency executions by partial order rather than by raw thread schedule, using a simple priority rule to give meaningful probability to each behavior. That shift yields exponentially better error-detection guarantees than earlier randomized methods and finds real bugs, including in Firefox’s JavaScript engine.

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 LockIt, a system that makes lock-free data structures easy to verify.

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.

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

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.

One of our best model checking papers. 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.

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).

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.

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).

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 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.

Independently replicating database partitions can leave a backup in an inconsistent state after failure. Coordinating snapshots with asynchronous replication preserves a consistent prefix across partitions; push-based backpressure bounds lag, while separating replication from applying writes supports fast recovery without sacrificing local transaction latency.

Actor transactions over slow cloud storage become practical by releasing locks during the first phase of commit, tracking dependencies for cascading aborts, and prefetching actor state before locking. Together these techniques hide storage latency, enable distributed group commit, and raise throughput without weakening ACID semantics.

Building on Chardonnay, Chablis extends its epoch-based transaction design from one datacenter to multiple regions. It preserves low-latency regional read-write transactions while adding lock-free, globally consistent snapshot reads, providing strict serializability without a restricted programming model or specialized clock hardware.

Fast datacenter networking and low-latency log storage make two-phase commit fast enough that reading on-disk data while holding locks becomes the real bottleneck. Chardonnay uses strongly consistent, lock-free snapshots to prefetch transaction data before acquiring locks, delivering general, strictly serializable on-disk transactions while avoiding deadlock aborts.

Fast NVMe devices make kernel overhead a bottleneck. XRP runs application-defined eBPF storage functions inside the NVMe driver, bypassing most of the storage stack while preserving file access controls.

Sharding must balance load while limiting costly distributed queries. Neuroshard is the first system to learn row placements directly from workloads using reinforcement learning, optimizing multiple objectives together.

Fast NVMe devices make kernel overhead a bottleneck. Inspired by exokernels, we propose BPF functions that chain dependent reads inside the NVMe driver, bypassing most of the storage stack.

Serverless platforms waste time fetching the same data repeatedly. Lambdata lets developers declare what each function reads and writes, enabling caching and scheduling that reuse data and warm containers to reduce latency and cost.

Describes WeChat's system for handling occasional massive overloads.

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 UNIC, a system that allows mutually distrusting users to deduplicate computations done by general programs.

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

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

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 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.

A language-independent consistency test unifies under- and over-constrained zero-knowledge circuit bugs, then mutation-guided fuzzing turns that foundation into a practical detector. Across 452 Circom circuits, it found 85 bugs, including 59 zero-days; developers confirmed 39 and fixed 14.

Model repositories create a software-supply-chain risk: loading a malicious pickle model can invoke arbitrary code. PickleBall statically derives safe deserialization policies from ML library code and enforces them in a drop-in loader, accepting 79.8% of benign models while rejecting every malicious example evaluated.

Rogue package updates reveal themselves through new data flows across trust boundaries, not merely through suspicious code in isolation. Comparing only changed flows between JavaScript package versions improves detection while reducing false positives, outperforming prior malicious-package systems by more than sevenfold.

Instead of asking developers to hand-write deserialization allowlists, static duck typing infers which classes the surrounding program actually needs. The generated bindings block an average of 97% of potential gadget code, prevent automated exploits in the evaluation, and produce fixes developers merged.

Compiler optimization can leave one value with divergent internal representations, turning a nearby bug into a more powerful exploit. A SQLite case study demonstrates the risk, while candidate-producing patterns in 44% of scanned repositories suggest it is not an isolated phenomenon.

Fear of breakage delays software dependency updates and security fixes. Upgradvisor combines static analysis with selective hardware tracing to focus review on changed dependency code an application actually uses.

Egalito is a binary recompiler that leverages metadata widely present in modern binaries to recover all code pointers for full disassembly and free rewrites, enabling nine tools including continuous randomization that protects Egalito itself and software versions of hardware control-flow protections.

Rebooting can remove an attacker’s foothold, but interrupts physical control. YOLO combines frequent resets and software diversification, using inertia to keep engines and drones operating while their controllers recover.

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.

Shuffler turns code randomization into a continuously moving target, reshuffling an application—including the shuffler itself—faster than practical code-reuse attacks can assemble an exploit. Its self-hosting design needs no operating-system, compiler, linker, or source changes, making the defense unusually deployable.

Studies the security consequences of concurrency errors.

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

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.

The hottest function is not always the cause of a slowdown. Recording variable values alongside cost profiles exposes anomalies that separate healthy and faulty executions, diagnosing all 15 evaluated real-world performance bugs and several issues that had remained unresolved for years.

Conventional tracing can mistake incidental activity for causality, misleading performance debugging. Argus differentiates definite and ambiguous links, then uses beam search to find likely causal paths despite this ambiguity. It successfully diagnosed longstanding macOS freezes.

Optimizing software for a workload usually requires source code and recompilation. Built on Egalito, CodeMason profiles binaries, rearranges functions to improve CPU cache use, and replaces indirect library calls with direct calls to reduce overhead.

UI changes often break tests. AppFlow is the first to use machine learning to recognize app screens and widgets. It combines modular test flows into tests that adapt across versions and similar apps.

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

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

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

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.

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 how we found many copy-and-paste bugs in a large commercial code base.

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

Describes a distributed version of eXplode.

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.

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.

Radshield protects commodity hardware used in space from radiation-induced short circuits and silent data corruption entirely in software. It was deployed aboard NASA’s Perseverance Mars rover to protect an autonomous navigation algorithm.

The shift from bespoke satellites to heterogeneous, intermittently connected fleets makes space computing look like a severely constrained multi-tenant cloud. This position paper maps the resulting systems and security questions and sketches a lightweight eBPF runtime for managing them.

Commodity computers could make small satellites far more capable if software can absorb radiation faults that specialized hardware handles today. This vision identifies destructive overheating and silent data corruption as the central threats and outlines software defenses for both.