Project Details
Description
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.
Status | Finished |
---|---|
Effective start/end date | 8/15/07 → 7/31/13 |
Funding
- National Science Foundation: $400,000.00