Practical Security Guarantees in Distributed Systems: Making secure-typed languages practical for real systems

Our research primarily explores these two areas:

  1. security-typed language design and implementation, including automation and visualization developer tool
  2. policy management and enforcement mechanisms for security-typed applications in distributed systems.

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 some very 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. We will demonstrate this thesis by using security-typed languages to develop two significant applications: a mediation policy enforcement mechanism and a distributed file system. In order to develop these applications, security-typed languages and distributed systems must meet in the middle. The language-based tools must be extended to better handle distributed applications. Furthermore, developer tools are needed to aid in visualization and inference of information flows. At the same time, distributed systems must be extended through policy management and enforcement mechanisms which can accommodate security-typed applications.

JPmail

JPmail is a secure email client which uses the security-typed language Jif to get information-flow control guarantees. JPmail was developed in Jif and utilizes some tools we built to handle high-level security policy, cryptography, declassification and distributed policy. For more information, see the JPmail page. For downloads, see the JPmail downloads page.

Jifclipse

Jifclipse is an IDE for the security-typed language Jif built on the Eclipse extensible development platform. Jifclipse provides a Jif programmer with additional tools to view hidden information generated by a Jif compilation, to suggest fixes for errors, and to get more specific information behind an error message. For more information see the Jifclipse page.

Jif signature generator

The Jif language allows programmers to check that their programs are information-flow secure. This requires that every source and sink in the program be labeled, including library functions. Signatures are used to specify the security behavior of library functions. Generating these signatures by hand can be tedious. siggen automatically generates signature files based on what external classes and methods a Java or Jif program uses. For more information see the Jif signature generator page.

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, 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, 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, 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]