We present OASIS, a CPU instruction set extension for externally verifiable initiation, execution, and termination of an isolated execution environment with a trusted computing base consisting solely of the CPU. OASIS leverages the hardware components available on commodity CPUs to achieve a low-cost, low-overhead design.

We present the design, implementation, and verification of XMHF- an eXtensible and Modular Hypervisor Framework. XMHF is designed to achieve three goals -- modular extensibility, automated verification, and high performance. XMHF includes a core that provides functionality common to many hypervisor-based security architectures and supports extensions that augment the core with additional security or functional properties while preserving the fundamental hypervisor security property of memory integrity (i.e., ensuring that the hypervisor's memory is not modified by software running at a lower privilege level). We verify the memory integrity of the XMHF core -- 6018 lines of code -- using a combination of automated and manual techniques. The model checker CBMC automatically verifies 5208 lines of C code in about 80 seconds using less than 2GB of RAM. We manually audit the remaining 422 lines of C code and 388 lines of assembly language code that are stable and unlikely to change as development proceeds. Our experiments indicate that XMHF's performance is comparable to popular high-performance general-purpose hypervisors for the single guest that it supports.

Much effort has been spent to reduce the software Trusted Computing Base (TCB) of modern systems. However, there remains a large and complex hardware TCB, including memory, peripherals, and system buses. There are many stronger, but still realistic, adversary models where we need to consider that this hardware may be malicious or compromised. Thus, there is a practical need to determine whether we can achieve secure program execution in the presence of not only malicious software, but also malicious hardware.

A trusted path is a protected channel that assures the secrecy and authenticity of data transfers between a user's input/output (I/O) device and a program trusted by that user. We argue that, despite its incontestable necessity, current commodity systems do not support trusted path with any significant assurance. This paper presents a hyper visor-based design that enables a trusted path to bypass an untrusted operating-system, applications, and I/O devices, with a minimal Trusted Computing Base (TCB). We also suggest concrete I/O architectural changes that will simplify future trusted-path system design. Our system enables users to verify the states and configurations of one or more trusted-paths using a simple, secret less, hand-held device. We implement a simple user-oriented trusted path as a case study.

In this paper, we explore the problem of creating \emph{vulnerability signatures}. A vulnerability signature is based on a program vulnerability, and is not specific to any particular exploit. The advantage of vulnerability signatures is that their quality can be guaranteed. In particular, we create vulnerability signatures which are guaranteed to have zero false positives. We show how to automate signature creation for any vulnerability that can be detected by a runtime monitor. We provide a formal definition of a vulnerability signature, and investigate the computational complexity of creating and matching vulnerability signatures. We systematically explore the design space of vulnerability signatures. We also provide specific techniques for creating vulnerability signatures in a variety of language classes. In order to demonstrate our techniques, we have built a prototype system. Our experiments show that we can, using a single exploit, automatically generate a vulnerability signature as a regular expression, as a small program, or as a system of constraints. We demonstrate techniques for creating signatures of vulnerabilities which can be exploited via multiple program paths. Our results indicate that our approach is a viable option for signature generation, especially when guarantees are desired.

The vulnerabilities that plague computers cause endless grief to users. Slammer compromised millions of hosts in minutes; a hit-list worm would take under a second. Recently proposed techniques respond better than manual approaches, but require expensive instrumentation, which limits deployment. Although spreading "antibodies" (e.g. signatures) ameliorates this limitation, hosts depending on antibodies are defenseless until inoculation; to the fastest hit-list worms this delay is crucial. Additionally, most recently proposed techniques cannot provide recovery to provide continuous service after an attack.

We address the problem of replaying an application dialog between two hosts. The ability to accurately replay application dialogs is useful in many security-oriented applications, such as replaying an exploit for forensic analysis or demonstrating an exploit to a third party.A central challenge in application dialog replay is that the dialog intended for the original host will likely not be accepted by another without modification. For example, the dialog may include or rely on state specific to the original host such as its hostname, a known cookie, etc. In such cases, a straight-forward byte-by-byte replay to a different host with a different state (e.g., different hostname) than the original observed dialog participant will likely fail. These state-dependent protocol fields must be updated to reflect the different state of the different host for replay to succeed.We formally define the replay problem. We present a solution which makes novel use of program verification techniques such as theorem proving and weakest pre-condition. By employing these techniques, we create the first sound solution to the replay problem: replay succeeds whenever our approach yields an answer. Previous techniques, though useful, are based on unsound heuristics. We implement a prototype of our techniques called Replayer, which we use to demonstrate the viability of our approach.

In this paper we explore the problem of creating vulnerability signatures. A vulnerability signature matches all exploits of a given vulnerability, even polymorphic or metamorphic variants. Our work departs from previous approaches by focusing on the semantics of the program and vulnerability exercised by a sample exploit instead of the semantics or syntax of the exploit itself. We show the semantics of a vulnerability define a language which contains all and only those inputs that exploit the vulnerability. A vulnerability signature is a representation (e.g., a regular expression) of the vulnerability language. Unlike exploit-based signatures whose error rate can only be empirically measured for known test cases, the quality of a vulnerability signature can be formally quantified for all possible inputs. We provide a formal definition of a vulnerability signature and investigate the computational complexity of creating and matching vulnerability signatures. We also systematically explore the design space of vulnerability signatures. We identify three central issues in vulnerability-signature creation: how a vulnerability signature represents the set of inputs that may exercise a vulnerability, the vulnerability coverage (i.e., number of vulnerable program paths) that is subject to our analysis during signature creation, and how a vulnerability signature is then created for a given representation and coverage. We propose new data-flow analysis and novel adoption of existing techniques such as constraint solving for automatically generating vulnerability signatures. We have built a prototype system to test our techniques. Our experiments show that we can automatically generate a vulnerability signature using a single exploit which is of much higher quality than previous exploit-based signatures. In addition, our techniques have several other security applications, and thus may be of independent interest.

It is widely believed that content-signature-based intrusion detection systems (IDS) are easily evaded by polymorphic worms, which vary their payload on every infection attempt. In this paper, we present Polygraph, a signature generation system that successfully produces signatures that match polymorphic worms. Polygraph generates signatures that consist of multiple disjoint content substrings. In doing so, Polygraph leverages our insight that for a real-world exploit to function properly, multiple invariant substrings must often be present in all variants of a payload; these substrings typically correspond to protocol framing, return addresses, and in some cases, poorly obfuscated code. We contribute a definition of the polymorphic signature generation problem; propose classes of signature suited for matching polymorphic worm payloads; and present algorithms for automatic generation of signatures in these classes. Our evaluation of these algorithms on a range of polymorphic worms demonstrates that Polygraph produces signatures for polymorphic worms that exhibit low false negatives and false positives.

Security is important for many sensor network applications. A particularly harmful attack against sensor and ad hoc networks is known as the Sybil attack [6], where a node illegitimately claims multiple identities. This paper systematically analyzes the threat posed by the Sybil attack to wireless sensor networks. We demonstrate that the attack can be exceedingly detrimental to many important functions of the sensor network such as routing, resource allocation, misbehavior detection, etc. We establish a classification of different types of the Sybil attack, which enables us to better understand the threats posed by each type, and better design countermeasures against each type. We then propose several novel techniques to defend against the Sybil attack, and analyze their effectiveness quantitatively.

The widespread deployment of sensor networks is on the horizon. One of the main challenges in sensor networks is to process and aggregate data in the network rather than wasting energy by sending large amounts of raw data to reply to a query. Some efficient data dissemination methods, particularly data-centric storage and information aggregation, rely on efficient routing from one node to another. In this paper we introduce GEM (Graph EMbedding for sensor networks), an infrastructure for node-to-node routing and data-centric storage and information processing in sensor networks. Unlike previous approaches, it does not depend on geographic information, and it works well even in the face of physical obstacles. In GEM, we construct a labeled graph that can be embedded in the original network topology in an efficient and distributed fashion. In that graph, each node is given a label that encodes its position in the original network topology. This allows messages to be efficiently routed through the network, while each node only needs to know the labels of its neighbors.To demonstrate how GEM can be applied, we have developed a concrete graph embedding method, VPCS (Virtual Polar Coordinate Space). In VPCS, we embed a ringed tree into the network topology, and label the nodes in such a manner as to create a virtual polar coordinate space. We have also developed VPCR, an efficient routing algorithm that uses VPCS. VPCR is the first algorithm for node-to-node routing that guarantees reachability, requires each node to keep state only about its immediate neighbors, and requires no geographic information. Our simulation results show that VPCR is robust on dynamic networks, works well in the face of voids and obstacles, and scales well with network size and density.