This paper reports our experience applying lightweight formal methods to validate the correctness of ShardStore, a new key-value storage node implementation for the Amazon S3 cloud object storage service. By "lightweight formal methods" we mean a pragmatic approach to verifying the correctness of a production storage node that is under ongoing feature development by a full-time engineering team. We do not aim to achieve full formal verification, but instead emphasize automation, usability, and the ability to continually ensure correctness as both software and its specification evolve over time. Our approach decomposes correctness into independent properties, each checked by the most appropriate tool, and develops executable reference models as specifications to be checked against the implementation. Our work has prevented 16 issues from reaching production, including subtle crash consistency and concurrency problems, and has been extended by non-formal-methods experts to check new features and properties as ShardStore has evolved.

Data stored in cloud services is highly sensitive and so access to it is controlled via policies written in domain-specific languages (DSLs). The expressiveness of these DSLs provides users flexibility to cover a wide variety of uses cases, however, unintended misconfigurations can lead to potential security issues. We introduce Block Public Access, a tool that formally verifies policies to ensure that they only allow access to trusted principals, i.e. that they prohibit access to the general public. To this end, we formalize the notion of Trust Safety that formally characterizes whether or not a policy allows unconstrained (public) access. Next, we present a method to compile the policy down to a logical formula whose unsatisfiability can be (1) checked by SMT and (2) ensures Trust Safety. The constructs of the policy DSLs render unsatisfiability checking PSPACE-complete, which precludes verifying the millions of requests per second seen at cloud scale. Hence, we present an approach that leverages the structure of the policy DSL to compute a much smaller residual policy that corresponds only to untrusted accesses. Our approach allows Block Public Access to, in the common case, syntactically verify Trust Safety without having to query the SMT solver. We have implemented Block Public Access and present an evaluation showing how the above optimization yields a low-latency policy verifier that the S3 team at AWS has integrated into their authorization system, where it is currently in production, analyzing millions of policies everyday to ensure that client buckets do not grant unintended public access.

The permissions framework for Android is frustratingly inflexible. Once granted a permission, Android will always allow an app to access the resource until the user manually revokes the app's permission. Prior work has proposed extensible plugin frameworks, but they have struggled to support flexible authorization and isolate apps and plugins from each other. In this paper, we propose DALF, a framework for extensible permissions plugins that provides both flexibility and isolation. The insight underlying DALF is that permissions plugins should be treated as apps themselves. This approach allows plugins to maintain state and access system resources such as a device's location while being restricted by Android's process-isolation mechanisms. Experiments with microbenchmarks and case studies with real third-party apps show promising results: plugins are easy to develop and impose acceptable overhead for most resources.

Efficient snapshots are an important feature of modern storage systems. However, the implicit sharing underlying most snapshot implementations makes it difficult to answer basic questions about the storage costs of individual snapshots. Traditional techniques for answering these questions incur significant performance penalties due to expensive metadata overheads. We present a novel probabilistic data structure, compatible with existing storage systems, that can provide approximate answers about snapshot costs with very low computational and storage overheads while achieving better than 95% accuracy for real-world data sets.

A hit rate curve is a function that maps cache size to the proportion of requests that can be served from the cache. (The caching policy and sequence of requests are assumed to be fixed.) Hit rate curves have been studied for decades in the operating system, database and computer architecture communities. They are useful tools for designing appropriate cache sizes, dynamically allocating memory between competing caches, and for summarizing locality properties of the request sequence. In this paper we focus on the widely-used LRU caching policy. Computing hit rate curves is very efficient from a runtime standpoint, but existing algorithms are not efficient in their space usage. For a stream of m requests for n cacheable objects, all existing algorithms that provably compute the hit rate curve use space linear in n. In the context of modern storage systems, n can easily be in the billions or trillions, so the space usage of these algorithms makes them impractical. We present the first algorithm for provably approximating hit rate curves for the LRU policy with sublinear space. Our algorithm uses O( p^2 * log(n) * log^2(m) / epsilon^2 ) bits of space and approximates the hit rate curve at p uniformly-spaced points to within additive error epsilon. This is not far from optimal. Any single-pass algorithm with the same guarantees must use Omega(p^2 + epsilon^{-2} + log(n)) bits of space. Furthermore, our use of additive error is necessary. Any single-pass algorithm achieving multiplicative error requires Omega(n) bits of space.

Users of hosted web-based applications implicitly trust that those applications, and the data that is within them, will remain active and available indefinitely into the future. When a service is terminated, for reasons such as the insolvency of the business that is providing it, users risk the immediate loss of software functionality and may face the permanent loss of their own data. This paper presents Micasa, a runtime for hosted applications that allows a significant subset of application logic and user data to remain available even in the event of the failure of a provider's business. By allowing users to audit application dependence on hosted components, and maintain externalized and private copies of their own data and the logic that allows access to it, we believe that Micasa is a first step in the direction of a more balanced degree of trust and investment between application providers and their users.

As hardware parallelism continues to increase, CPU caches can no longer be considered as a transparent, hardware-level performance optimization. Cache impact on performance, in particular in the face of false sharing, is completely dependent on the software that is executing. To effectively support parallel workloads on cache coherent hardware, the operating system must begin to treat the CPU cache like other shared hardware resources, and manage it appropriately.

Operating systems represent large pieces of complex software that are carefully tested and broadly deployed. Despite this, developers frequently have little more than their source code to understand how they behave. This static representation of a system results in limited insight into execution dynamics, such as what code is important, how data flows through a system, or how threads interact with one another. We describe Tralfamadore, a system that preserves complete traces of machine execution as an artifact that can be queried and analyzed with a library of simple, reusable operators, making it easy to develop and run new dynamic analyses. We demonstrate the benefits of this approach with several example applications, including a novel unified source and execution browser.

This paper describes the design and implementation of SecondSite, a cloud-based service for disaster tolerance. SecondSite extends the Remus virtualization-based high availability system by allowing groups of virtual machines to be replicated across data centers over wide-area Internet links. The goal of the system is to commodify the property of availability, exposing it as a simple tick box when configuring a new virtual machine. To achieve this in the wide area, we have had to tackle the related issues of replication traffic bandwidth, reliable failure detection across geographic regions and traffic redirection over a wide-area network without compromising on transparency and consistency.

Cloud computing uses virtualization to lease small slices of large-scale datacenter facilities to individual paying customers. These multi-tenant environments, on which numerous large and popular web-based applications run today, are founded on the belief that the virtualization platform is sufficiently secure to prevent breaches of isolation between different users who are co-located on the same host. Hypervisors are believed to be trustworthy in this role because of their small size and narrow interfaces.

Program source is an intermediate representation of software; it lies between a developer's intention and the hardware's execution. Despite advances in languages and development tools, source itself and the applications we use to view it remain an essentially static representation of software, from which developers can spend considerable energy postulating actual behavior.

Parallax is a distributed storage system that uses virtualization to provide storage facilities specifically for virtual environments. The system employs a novel architecture in which storage features that have traditionally been implemented directly on high-end storage arrays and switches are relocated into a federation of storage VMs, sharing the same physical hosts as the VMs that they serve. This architecture retains the single administrative domain and OS agnosticism achieved by array- and switch-based approaches, while lowering the bar on hardware requirements and facilitating the development of new features. Parallax offers a comprehensive set of storage features including frequent, low-overhead snapshot of virtual disks, the 'gold-mastering' of template images, and the ability to use local disks as a persistent cache to dampen burst demand on networked storage.

Many software attacks are based on injecting malicious code into a target host. This paper demonstrates the use of a well-known technique, data tainting, to track data received from the network as it propagates through a system and to prevent its execution. Unlike past approaches to taint tracking, which track tainted data by running the system completely in an emulator or simulator, resulting in considerable execution overhead, our work demonstrates the ability to dynamically switch a running system between virtualized and emulated execution. Using this technique, we are able to explore hardware support for taint-based protection that is deployable in real-world situations, as emulation is only used when tainted data is being processed by the CPU. By modifying the CPU, memory, and I/O devices to support taint tracking and protection, we guarantee that data received from the network may not be executed, even if it is written to, and later read from disk. We demonstrate near native speeds for workloads where little taint data is present.

The emergence of wireless ad hoc networking has opened the way for a new style of distributed computing. Ad hoc networks operate without infrastructure such as routers or access points. Software designed for this environment faces new challenges. In traditional networks, partitioning is typically treated as an exceptional and transient condition. The situation in ad hoc wireless networks is completely reversed. Each ad hoc group is an isolated network, partitioned from all other ad hoc networks. As computers move from one ad hoc group to another, the set of partitions changes. This paper presents the design and implementation of a data synchronization service intended specifically for ad hoc wireless networks. It describes the underlying factors affecting the design, the protocol used to achieve synchronization, and some performance measurements from the actual implementation.

Numerous systems have been designed which use virtualization to subdivide the ample resources of a modern computer. Some require specialized hardware, or cannot support commodity operating systems. Some target 100% binary compatibility at the expense of performance. Others sacrifice security or functionality for speed. Few offer resource isolation or performance guarantees; most provide only best-effort provisioning, risking denial of service.This paper presents Xen, an x86 virtual machine monitor which allows multiple commodity operating systems to share conventional hardware in a safe and resource managed fashion, but without sacrificing either performance or functionality. This is achieved by providing an idealized virtual machine abstraction to which operating systems such as Linux, BSD and Windows XP, can be ported with minimal effort.Our design is targeted at hosting up to 100 virtual machine instances simultaneously on a modern server. The virtualization approach taken by Xen is extremely efficient: we allow operating systems such as Linux and Windows XP to be hosted simultaneously for a negligible performance overhead --- at most a few percent compared with the unvirtualized case. We considerably outperform competing commercial and freely available solutions in a range of microbenchmarks and system-wide tests.

Summary form only given. Our work to date has been in the design and development of a stream-centric model for communications which we have called the flow. A flow is a uniquely named, message-based, multicast communications stream. Flows are named by FlowIDs which represent a collection of resources used to provide a communications stream in the same manner that process IDs represent resources associated with a computational task. By providing distinct names for these multicast streams, services become decoupled from network endpoints. This single property provides sweeping benefits for mobility, fault tolerance, and resource location. In addition to naming, we have implemented three properties of flows which we feel are beneficial to distributed applications. We have finished an initial implementation of flows as a network middleware and have become convinced that they are an interesting and useful communications abstraction.