Center for Resilient Software
Mission
We are currently working on several computer security projects. All of these projects work with a system and a specification of the security properties that the system must satisfy. The specification is obtained either directly from a developer or by inferring the specification from observations of the system as it operates securely. Some of the techniques dynamically monitor the execution of the system to observe any attempted security property violation, then intervene to change the behavior of the system to eliminate the violation. Others statically analyze the implementation before it executes to verify that all executions will satisfy the security properties (and potentially change the implementation to do so if it may not).
Unlike many approaches, these projects emphasize the continued safe execution of the system even in the presence of attacks so that it provides as much desirable functionality as possible and continues to provide service to legitimate users while under attack.
People
Researchers
Staff
PhD Students
Research Projects
Secure Cloud Computing Systems
Modern cloud computing systems offer unprecedented computational resources and flexibility in allocating those resources to a variety of users and tasks. But cloud computing systems also provide attackers with new opportunities and can amplify the ability of the attacker to compromise the computing infrastructure.
The Cloud Intrusion Detection and Repair project is developing a system that observes normal interactions during the secure operation of the cloud to derive properties that characterize this secure operation. If any part of the cloud subsequently attempts to violate these properties, the system intervenes and changes the interaction (by, for example, adding or removing operations or changing the parameters that appear in operations) to ensure that the cloud executes securely and survives the attack while continuing to provide uninterrupted service to legitimate users.
The crux of our approach revolves around a new technique that we are developing called Input Rectification. Applications are typically able to process the vast majority of inputs securely. Attacks usually succeed because they contain an atypical feature that the application does not process correctly. Our input rectification research observes inputs that the application processes correctly to derive a model (in the form of constraints over input fields) of the "comfort zone" of the application (the set of inputs that the application can process successfully). When it encounters an input that is outside the comfort zone, the rectifier uses the model to change the input to move the input into the comfort zone of the application. Our results show that this technique eliminates security vulnerabilities in a range of applications, leaves the overwhelming majority of safe inputs unchanged, and preserves much of the useful information in modified atypical inputs.
This project is currently funded under the DARPA Mission-Oriented Resilient Clouds (MRC) program. MIT is the sole performer.
Program Verification for Secure Mobile Applications
Application marketplaces (such as the Android Market) provide users with a wide range of desirable applications for their mobile devices. But application marketplaces can also provide a compelling distribution channel for attackers who place attractive applications containing malware into the application marketplace.
The Provably Safe Android Apps project is developing a static program analysis system for finding malware in Android applications written in Java. A goal is ensuring that application marketplaces contain only safe mobile applications.
As part of this effort we are developing techniques to statically verify that Android applications never violate key security properties. Given a specification that identifies the operating modes of the application and the sequences of safe operations in each mode, the analysis determines if the application satisfies the specification. If it does not, it automatically modifies the application so that it does. Once again, the goal is to preserve as much of the desirable functionality of the application as possible while ensuring that the system remains secure.
This project is a collaboration between MIT and the Kestrel Institute.
Eliminating Vulnerabilities in Java Applications
The VIBRANCE project is developing techniques to eliminate vulnerabilities in Java applications. As part of this effort we are developing techniques to eliminate vulnerabilities that are triggered by unchecked inputs. Examples include injection vulnerabilities (such as SQL, command, ldap, and xquery injection attacks), resource allocation vulnerabilities (which cause the application to request excessive resources), and numeric overflow and underflow vulnerabilties.
A central goal of the project is to develop an efficient taint tracer that can detect when an unchecked input value appears at a potential vulnerability site. For example, the application may use an input field directly as a parameter at a memory allocation site without checking that the value in the field is reasonably small (so that the application can perform the allocation successfully). When the taint tracer detects such a value, it consults a configurable security policy to determine what action to take to eliminate the vulnerability and, ideally, enable the application to continue to execute.
The taint tracer combines precise dynamic taint tracing with static analysis to reduce the tracing overhead. By statically tracking the flow of values through the program, the static analysis makes it possible to eliminate intermediate dynamic taint propagation steps (and therefore the overhead otherwise associated with these steps). The goal is a taint tracer with overhead small enough for routine production use (existing taint tracers are used almost exclusively only for testing or debugging).
This project is funded by IARPA under the STONESOUP program. The performers include MIT and Kestrel.
Eliminating Vulnerabilities in Stripped x86 and x64 Binaries
The SPICE project is working to eliminate vulnerabilities triggered by a variety of low-level errors in stripped x86 binaries. As part of this project we are developing on a combined dynamic and static type inference system. This system analyzes reads and writes to infer how the application structures the flat x86/x64 address space. It uses this information to preserve the integrity of the execution. For example, SPICE is designed to neutralize attacks that attempt to exploit buffer overflow vulnerabilities within allocation units. SPICE uses a configurable security policy to modify the execution to eliminate the vulnerability and enable continued safe execution.
The SPICE project is also developing a precise taint tracing system. This system combines static and dynamic analysis to minimize overhead. The taint information enables SPICE to detect the unsafe direct use of untrusted input fields at vulnerability sites such as SQL and command invocation sites and memory allocation sites. SPICE also tracks memory allocation information to eliminate buffer overflow attacks.
This project is funded by IARPA under the STONESOUP program. The performers include MIT, SAIC, Kestrel, The University of California at Berkeley, and Global Infotech.
Jobs
CRS is actively seeking for talented and motivated people to help improve software reliability. UROP researchers for Spring 2012 and Summer 2012 are particularly encouraged to apply. Contact Stelios or Jeff for more details.