| NSF Org: |
CNS Division Of Computer and Network Systems |
| Recipient: |
|
| Initial Amendment Date: | July 30, 2010 |
| Latest Amendment Date: | July 30, 2010 |
| Award Number: | 1018061 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Deborah Shands
CNS Division Of Computer and Network Systems CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 1, 2010 |
| End Date: | August 31, 2015 (Estimated) |
| Total Intended Award Amount: | $499,995.00 |
| Total Awarded Amount to Date: | $499,995.00 |
| Funds Obligated to Date: |
|
| 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): | TRUSTWORTHY COMPUTING |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Compositional security is a recognized central scientific challenge for trustworthy computing. Contemporary systems are built up from smaller components. However, even if each component is secure in isolation, the composed system may not achieve the desired end-to-end security property: an adversary may exploit complex interactions between components to compromise security.
This project addresses this important problem by developing a general model of systems and adversaries and techniques for modular reasoning and design. A central idea is to view a trusted system in terms of the interfaces that the various components expose: larger trusted components are built by combining interface calls in known ways; the adversary is constrained to the interfaces it has access to, but may combine interface calls without restriction. At a technical level, we are developing an expressive concurrent programming language with recursive functions for modeling interfaces and higher-order data for modeling code obtained at run time, and a logic of programs to capture reasoning principles for compositional security. We are using this framework to develop a systematic basis for web security, to formalize attacker models for web browsers proposed in literature and develop new ones, and to build an understanding of relevant security policies, end-to-end security properties, attacks in the wild, and ways to defend and prove web applications secure against these attacks. This study could have impact on security mechanisms and policies used in web applications in practice. The reasoning methods developed in the project will be mechanized in a tool.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
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.
Compositional security principles are critical for scalable construction and analysis of secure systems. Contemporary systems are built up from smaller components, but even if each component is secure in isolation, a system composed of secure components may not meet its security requirements. Attacks using properties of one component to subvert another have shown up in practice in many different settings, including cryptographic protocols, systems software, application software, web browsers and infrastructure.
The intellectual merit of the project is reflected in new theory of compositional security called Adversary-aware Assume Guarantee. In traditional assume-guarantee reasoning for reasoning about system correctness, system components assume that other components satisfy certain assumptions. These assumptions are discharged by analyzing the code of other components. In contrast, in the security setting addressed by the new theory, assumptions about adversarial components are enforced using a combination of cryptographic, hardware, and software protection mechanisms and associated program-directed methods for reasoning about them.
Specifically, the project develops System M -- the first program logic that allows proofs of safety for higher-order programs that execute adversary-supplied code without requiring the adversarial code to be available for deep static analysis. It supports reasoning about invariants of adversarial components via interface-confinement (or sandboxing) and code identity checks. System M has been used to prove security properties of models of implemented hypervisors and trusted computing systems built at Carnegie Mellon University.
The broader impact of the project includes impact on the emerging science of security and contributions to human resource development in this important area. The project has supported two PhD students who have transitioned to research and industry positions. It has also provided support for two co-PIs (one female, one male) who have transitioned from postdoctoral research positions to faculty positions.
Last Modified: 01/17/2016
Modified by: Anupam Datta
Please report errors in award information by writing to: awardsearch@nsf.gov.
