CAREER: Realizing Practical High Assurance through Security-Typed Information Flow Systems

Project: Research project

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.

StatusFinished
Effective start/end date8/15/077/31/13

Funding

  • National Science Foundation: $400,000.00

Fingerprint

Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.