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.

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.

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.

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

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

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.

We increasingly rely on deep learning and deep neural networks (DNNs) in safety- and security-critical applications such as self-driving, medical diagnosis, face-based identification, and malware detection, but it remains an open challenge to thoroughly test DNNs for robustness and security. We propose Neuron Coverage, the first testing coverage metric to empirically understand how much decision logic a testing input set has exercised in a DNN. We design and build DeepXplore, the first systematic testing framework for DNNs. Given a test input, DeepXplore applies physically realizable transformations (e.g., darkening an image) to the inputs (as opposed to noise in prior adversarial ML work) to generate new inputs to maximize neuron coverage. It found thousands of flaws in state-of-art self-driving and malware detection DNNs and improved their neuron coverage by over 50%. (Also appeared in MLSec '17.)

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.

Describes our vision of forgetting systems that quickly and completely forget user data including all derived data for security, privacy, and usability. The paper focuses on making machine learning systems forget (hence the term machine unlearning)

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

This paper is geared toward a general audience. If you have time to read just one paper on our concurrency work, this is the paper to read. It describes our vision of stable multithreading (StableMT), a radical approach to making multithreading reliable, and summarizes our last five years of work on designing, building, and applying stable multithreading systems. The final version of this paper will appear in CACM.

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

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

Describes how we leveraged model checking to find serious errors in three widely used, well tested Linux file system errors. Some of these errors can vaporize your entire file systems.

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.

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 a new replica placement strategy that uses multiple linear hash functions to achieve high performance, scalability, and availability.