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.
CAREER: Realizing Practical High Assurance through Security-Typed Information Flow Systems