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 (Cornell University, 2006) raised several important questions about program-rewriting technologies that are being investigated by my continuing work and that of other researchers. This has led to a growing belief that program-rewriting could be an extremely promising alternative to more traditional methods:

Which security policies can program-rewriters enforce? Understanding exactly what classes of security policies can be effectively enforced by program-rewriters is critical for selecting adequate defenses to perceived threats. In past work I have 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.
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. A promising alternative strategy involves automatically verifying the rewritten code produced by the rewriter rather than the rewriter itself. The Mobile Certified In-lined Reference Monitoring System that I implemented for the .NET framework demonstrates that such verification can be made far more tractable than traditional formal verification methods by using effect-based type systems and type-checkers.
Is program-rewriting a feasible technology for real languages and systems? To bring certifying IRM technology more toward real-world practice, my ongoing work on the SPoX (Security Policy XML) system involves developing code transformation tools, declarative policy specification languages, and formal policy analysis algorithms that bring certifying IRM technologies into real-world practicability.

Papers

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

Brian W. DeVries, Gopal Gupta, Kevin W. Hamlen, Scott Moore, and Meera Sridhar. ActionScript Bytecode Verification With Co-Logic Programming. In Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), June 2009.

Micah Jones and Kevin W. Hamlen. Enforcing IRM Security Policies: Two Case Studies. In Proceedings of IEEE Intelligence and Security Informatics (ISI) Conference, June 2009.

Kevin W. Hamlen, Vishwath Mohan, Mohammad M. Masud, Latifur Khan, and Bhavani Thuraisingham. Exploiting an Antivirus Interface. Computer Standards & Interfaces, April 2009.

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), 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.