Research

My research involves the development and analysis of technologies for enforcing security policies that constrain the behavior of untrusted code. Enforcing security policies over untrusted code has become increasingly important with the rise of distributed and extensible systems. For example, web browsers that upload and execute applet programs (e.g. in the form of .NET or JVM bytecode) must somehow ensure that this untrusted code behaves in a way that is consistent with the intentions of the web browser designer, the client network administrators, and the users of the client machine.

Security policies of these sorts have traditionally been enforced by applying static analyses (wherein the untrusted code is analyzed before it is executed to determine if it might exhibit a security violation when executed) or by implementing execution monitors (which run alongside the untrusted code as it executes and intervene in the event of a security violation). My research investigates a third option: automated program-rewriting. A program-rewriter takes an arbitrary untrusted program as input and outputs a new program satisfying the following two constraints:

• The resultant program must satisfy the security policy to be enforced.
• If the original program already satisfied the security policy, then the resultant program must behave identically to the original program.

Program-rewriters therefore enforce security policies by transforming policy-violating code into policy-obeying code whilst preserving the behavior of policy-obeying code.

My thesis work on program-rewriting technologies has raised and addressed several important questions, yielding results that indicate that program-rewriting could be an extremely promising alternative to more traditional methods:

1. Which security policies can program-rewriters enforce? My theoretical work with Greg Morrisett and Fred Schneider (published in TOPLAS) has shown that program-rewriters can not only enforce every security policy enforceable by a static analysis or execution monitor, they can also precisely enforce policies that are not precisely enforceable by any static analysis or execution monitor. That is to say, the technique of program-writing is strictly more powerful than the other two techniques combined.
2. Since program-rewriters can be sophisticated pieces of software, is it reasonable to trust them in a security-sensitive setting? Program-rewriters must often perform sophisticated analyses and transformations on the untrusted code they receive, and can therefore be very large and difficult to verify. However, I presented a paper by Greg Morrisett, Fred Schneider, and me at the ACM SIGPLAN Programming Languages and Analysis for Security (PLAS'06) conference in which we showed how to design a program-rewriter that need not be trusted at all. (Here are slides from that talk in PowerPoint and web-viewable formats.) Program-rewriters can be removed from a system's trusted computing base (the set of programs that must be trusted for security to be maintained) by replacing them with certifying program-rewriters, which output rewritten programs annotated with typing information sufficient to prove that the rewritten program satisfies the policy in question. These type annotations can then be verified automatically by a smaller trusted type-checker.
3. Is program-rewriting a feasible technology for real languages and systems? To show that it is, I developed a certifying program-rewriter and a type-checker for the Microsoft .NET framework. In addition, I've implemented a general-purpose type-checker that verifies that properly annotated managed CLI code obeys an arbitrary security policy written in a high-level specification language. The system supports important .NET language features like concurrency, non-terminating programs, exceptions, finalizers, and unbounded collections of dynamically allocated objects. See Chapter 4 of my thesis for a complete description.

Papers

The following is a list of some research papers and theses that I've written. Each is provided in PDF form.

Kevin W. Hamlen and Micah Jones. Aspect-Oriented In-lined Reference Monitors. In Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), to appear June 2008.

Kevin W. Hamlen and Bhavani Thuraisingham. Secure Peer-to-peer Networks for Trusted Collaboration, Invited paper. In Proceedings of the 2nd IEEE International Workshop on Trusted Collaboration (TrustCol), November 2007.

Nathalie Tsybulnik, Kevin W. Hamlen, Bhavani Thuraisingham. Centralized Security Labels in Decentralized P2P Networks. In Proceedings of the Annual Computer Security Applications Conference (ACSAC), December 2007, pp. 315-324.

Kevin W. Hamlen. Security Policy Enforcement by Automated Program-rewriting. PhD Thesis (Advisors: Greg Morrisett and Fred B. Schneider), Cornell University, Ithaca, New York, August 2006.

Kevin W. Hamlen, Greg Morrisett, and Fred B. Schneider. Certfied In-lined Reference Monitoring on .NET. In Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), June 2006, 7-16. [slides: PPT HTML]

Kevin W. Hamlen, Greg Morrisett, and Fred B. Schneider. Certified In-lined Reference Monitoring on .NET. Cornell Computer Science Department Technical Report TR-2005-2003, November 2005.

Kevin W. Hamlen, Greg Morrisett, and Fred B. Schneider. Computability Classes for Enforcement Mechanisms. ACM Transactions on Programming Languages And Systems (TOPLAS), 28(1), January 2006, 175-205. Also available as Cornell Computer Science Department Technical Report TR-2003-1908, August 2003.

Kevin W. Hamlen. Proof-Carrying Code for x86 Architectures. Undergraduate Senior Honors Thesis (Advisors: Peter Lee and George C. Necula), Carnegie Mellon, Pittsburgh, Pennsylvania, May 1998.

William Hamlen and Kevin W. Hamlen. A Closed System of Production Possibility and Social Welfare. Computers in Higher Education Economics Review (CHEER), 18, December 2006.