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

Award #: 0643907
Amount Awarded: $400,000
Sponsoring Organization: NSF (CNS)
Grant Period: 2007-2012
Primary Investigator(s): Patrick McDaniel

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.

Related Research Projects

Control Systems and Smart Grid

Secure Languages

Smartphone Application Analysis

Related Publications

Boniface Hicks, Timothy Misiak, and Patrick McDaniel, Channels: Runtime System Infrastructure for Security-typed Languages. 23rd Annual Computer Security Applications Conference (ACSAC), December 2007.

Boniface Hicks, Sandra Rueda, Trent Jaeger, and Patrick McDaniel, From Trusted to Secure: Building and Executing Applications that Enforce System Security. Proceedings of the USENIX Annual Technical Conference, June 2007. [Full Paper: pdf Abstract]

Boniface Hicks, Dave King, and Patrick McDaniel, Jifclipse: Development Tools for Security-Typed Applications. Proceedings of the 2nd ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS '07), ACM Press, June 14 2007. Editor: Michael Hicks. [Full Paper: pdf Abstract]

Boniface Hicks, Sandra Rueda, Trent Jaeger, and Patrick McDaniel, Integrating SELinux with Security-typed Languages. Third Annual Security Enhanced Linux Symposium, March 2007. [Full Paper: pdf Abstract]

Boniface Hicks, Sandra Rueda, Trent Jaeger, and Patrick McDaniel, From Trusted to Secure: Building and Executing Applications that Enforce System Security. Technical Report NAS-TR-0061-2007, Network and Security Research Center, January 2007.

Boniface Hicks, Kiyan Ahmadizadeh, and Patrick McDaniel, Understanding Practical Application Development in Security-typed Languages. 22st Annual Computer Security Applications Conference (ACSAC), December 2006. [Full Paper: pdf Abstract]

Boniface Hicks, Sandra Rueda, Trent Jaeger, and Patrick McDaniel, Breaking Down the Walls of Mutual Distrust: Security-typed Email Using Labeled IPsec. Technical Report NAS-TR-0049-2006, Network and Security Research Center, September 2006.

Boniface Hicks, Dave King, Patrick McDaniel, and Michael Hicks, Trusted Declassification: High-level policy for a security-typed language. Proceedings of the 1st ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS '06), ACM Press, June 10 2006. [Full Paper: pdf Abstract]

Boniface Hicks, Kiyan Ahmadizadeh, and Patrick McDaniel, From Languages to Systems: Understanding Practical Application Development in Security-typed Languages. Technical Report NAS-TR-0035-2006, Network and Security Research Center, April 2006.

Boniface Hicks, Dave King, and Patrick McDaniel, Declassification with Cryptographic Functions in a Security-Typed Language. Technical Report NAS-TR-0004-2005, Network and Security Center, January 2005. (updated May 2005). [Full Paper: Abstract]