
NSF Org: |
CNS Division Of Computer and Network Systems |
Recipient: |
|
Initial Amendment Date: | January 18, 2007 |
Latest Amendment Date: | January 18, 2007 |
Award Number: | 0643907 |
Award Instrument: | Standard Grant |
Program Manager: |
Sol Greenspan
sgreensp@nsf.gov (703)292-7841 CNS Division Of Computer and Network Systems CSE Directorate for Computer and Information Science and Engineering |
Start Date: | August 15, 2007 |
End Date: | July 31, 2013 (Estimated) |
Total Intended Award Amount: | $400,000.00 |
Total Awarded Amount to Date: | $400,000.00 |
Funds Obligated to Date: |
|
History of Investigator: |
|
Recipient Sponsored Research Office: |
201 OLD MAIN UNIVERSITY PARK PA US 16802-1503 (814)865-1372 |
Sponsor Congressional District: |
|
Primary Place of Performance: |
201 OLD MAIN UNIVERSITY PARK PA US 16802-1503 |
Primary Place of
Performance Congressional District: |
|
Unique Entity Identifier (UEI): |
|
Parent UEI: |
|
NSF Program(s): | ADVANCED NET INFRA & RSCH |
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
Patrick McDaniel
Pennsylvania State University
cAREER: Realizing Practical High Assurance through Security-Typed Information Flow Systems
0643907
Panel ID:070111
Abstract
This grant supports an investigation of formal models, algorithms,
methods, tools, and infrastructure that build upon the information
flow guarantees of security-typed languages to achieve high assurance
software systems. The information flow guarantees of security-typed
languages provide a practical avenue to achieving system security by
producing proofs of an implementation's compliance with a specified
policy. However, these languages are simply tools for restricting
information flow through source-code annotations: they provide no
theory or practice to indicate how such annotations can be used to
implement security in real systems. This work bridges the theoretical
and practical gap between systems security and security-typed
languages. In this, the following three central research thrusts are
under investigation: a) the mapping of high-level policies to secure
implementations through models and algorithms that enable the
generation of semantically equivalent policies and the automated
instrumentation of code to enforce them, b) the study of services and
languages that govern application and infrastructure information flow,
and c) the exploration of tools to instrument legacy systems with
information flow policy. Demonstrative stand-alone, distributed, and
multi-user applications and systems are being be developed and
evaluated with respect to a broad range of security goals. The
evaluation efforts include pursing formal proofs of correctness and
empirical analysis of performance and security tradeoffs.
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.
Please report errors in award information by writing to: awardsearch@nsf.gov.