Extending Developer Tools for Security-typed Languages

Award #: N/A
Amount Awarded: $46,400
Sponsoring Organization: Software Engineering Research Center, Motorola
Grant Period: 2005-2007
Primary Investigator(s): Patrick McDaniel (PI)

Abstract

As massively increasing amounts of sensitive information are stored in electronic media, the concerns for electronic data security have become ever more vital. Currently, the only way to ensure confidentiality and integrity of data for significant applications, however, is by manually inspecting the code. For large applications this is impractical—we need the help of automated tools. For other high-assurance applications, this is too imprecise—we need mathematical precision. Our goal is to show that it is possible, in a general- purpose and easy manner, to develop robust, efficient distributed applications which exhibit automated, provable security guarantees.

Security-typed languages have received much attention in the security literature, because they are a promising tool for solving some fundamental application security problems. Jif is a robust and powerful im- plementation of such a language. It has the necessary breadth and power to be useful in providing provable confidentiality guarantees for real applications. Unfortunately, it is currently complicated and burdensome in ways that severely inhibit its use for real applications. We believe that by providing an IDE in Eclipse, com- plete with tools to assist programmers with the visualization of information flows as well as the automation of both tedious and complex tasks, we can make programming in Jif more accessible for real applications.

This is the second year of an ongoing project in this area. We have made significant progress since its inception, and several important and challenging efforts remain. The following sections provide a brief overview of the project, specific progress and accomplishments.

Related Research Projects

Secure Languages

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]