| NSF Org: |
CNS Division Of Computer and Network Systems |
| Recipient: |
|
| Initial Amendment Date: | August 18, 2008 |
| Latest Amendment Date: | May 6, 2011 |
| Award Number: | 0831440 |
| Award Instrument: | Continuing Grant |
| Program Manager: |
Jeremy Epstein
jepstein@nsf.gov (703)292-8338 CNS Division Of Computer and Network Systems CSE Direct For Computer & Info Scie & Enginr |
| Start Date: | October 1, 2008 |
| End Date: | September 30, 2013 (Estimated) |
| Total Intended Award Amount: | $790,000.00 |
| Total Awarded Amount to Date: | $1,014,400.00 |
| Funds Obligated to Date: |
FY 2009 = $434,400.00 FY 2011 = $250,000.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
5000 FORBES AVE PITTSBURGH PA US 15213-3815 (412)268-8746 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
5000 FORBES AVE PITTSBURGH PA US 15213-3815 |
| Primary Place of Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): |
Information Technology Researc, TRUSTWORTHY COMPUTING |
| Primary Program Source: |
01000910DB NSF RESEARCH & RELATED ACTIVIT 01001112DB NSF RESEARCH & RELATED ACTIVIT |
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
This project is motivated by the fundamental question of whether it is possible to achieve verifiable end-to-end security properties by adding suitable security mechanisms on top of commercially available applications executing on an untrusted computing platform. A concrete example of such a scenario is provided by a user interacting with a bank's web server using a web browser running SSL. An important end-to-end security property in this context is protecting the confidentiality and integrity of the exchanged information and the user's password from malware and insider attacks on the local machine or the bank's server, as well as an active adversary trying to compromise the network communication. The untrusted computing platform here is the user's machine, which is running a commodity OS such as Windows or Linux and applications such as Internet Explorer or Firefox.
We believe that this goal can be achieved if one takes the approach of (1) minimizing the liability of security-property proof based on differentiated application services, and well-defined, useful properties of security-sensitive code, and (2) supporting the identified and proved properties by a security architecture that is compatible with commercially available platforms. Our system architecture includes novel components (e.g. trusted paths to local and remote security sensitive code) and integrates existing
technologies (e.g., hypervisors, isolated execution environments) in a way that minimizes the size of both system and security-sensitive application code, thus enabling formal verification.
The project will provide extensive educational opportunities for undergraduate and graduate students; research results will be integrated into courses at CMU and disseminated via technical publications, student internships, the CyLab Industrial Partners program, and the CMU Women@SCS roadshow program.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
To be useful in practice, security primitives must be available on commodity computers with demonstrable assurance and be understandable by ordinary users with minimum effort. The working hypothesis of this project was that traditional trusted systems comprising a reference monitor and layered operating system services that are formally verified, while useful for a few niche application areas, will continue to fail these criteria for commodity computers. In particular, commodity operating systems will continue to be untrustworthy; i.e., they will lack demonstrable properties and support only low-assurance services. Hence, this project was motivated by the fundamental question of whether it is possible to achieve verifiable security properties by adding suitable security mechanisms to unmodified commodity systems and untrusted applications.
This project represents a fundamental shift in the design of systems with demonstrable security properties. For nearly four decades, most researchers assumed that all security properties must be implemented layer-by-layer from the ground up, starting with a reference monitor. The reference monitor identifies all system subjects and objects, is isolated from external attacks, is always invoked for every subject reference to any object, and hence enforces a system's security policy. The reference monitor is supposed to be small and simple enough to enable correctness verification via formal proofs and hence provides high assurance of correct implementation of security properties. Furthermore, most researchers assumed that full operating system layering is also essential for verifiable security properties of applications.
In contrast with these long-standing assumptions, this project showed that it is possible to add non-virtualizing, micro-hypervisors to unmodified, untrustworthy commodity (i.e., low-assurance) operating systems. These micro-hypervisors enable the creation of isolated execution environments for application modules with verifiable security properties. In contrast with traditional hypervisors, our micro-hypervisors (e.g., TrustVisor, XMHF) do not virtualize hardware; e.g., they do not include scheduling or multiplexing operations. Hence, they are much simpler than all virtualizing hypervisors/VMMs, other recent micro-hypervisor designs, and past security kernels. As a consequence, we are able to verify micro-hypervisor security properties, and compose them with the higher level properties of isolated application modules. In addition, we are able to show that our micro-hypervisors can support higher level security primitives in a verifiable manner; i.e., trusted path to/from isolated application modules, and application level micro-kernels that implement verifiable services for isolated application modules. As a result, trustworthy software components can be supported for security-sensitive applications running on top of unmodified commodity operating systems. Hence, restructuring commodity operating systems to implement native security kernels and fully layered services becomes unnecesary for most security-sensitive applications. In addition, we investigated various mechanisms for the trusted boot of micro-hypervisor software, and the establishment of both hardware-based and software-based root of trust. Finally, we explored the use of micro-hypervisors to support security properties of network protocols.
The impact of this project reached beyond numerous publications in leading security conferences. For example, our reseach helped produce a micro-hypervisor development framework, called the XMHF, which is now available as open-source code. Our micro-hypervisor designs have been used by industry research efforts, including at N...
Please report errors in award information by writing to: awardsearch@nsf.gov.
