I am a doctoral student in computer science, primarily interested in
security, programming languages, software engineering, and the
intersection thereof. I am advised by
Dawn Song. So far,
my graduate research has focused on making the Web a safer place. Check out WebBlaze for more like-minded folk.
I previously received a B.S. and M.S. from
Brown University.
From 2007 to 2008, I worked in the
Fishworks group at Sun
Microsystems. For posterity's sake, you can view my old Brown University
undergraduate home page here.
Refereed Publications
-
Preventing Capability Leaks in Secure JavaScript Subsets. To Appear in Proc. of Network and Distributed System Security Sympossium (NDSS), 2010.Publishers wish to sandbox third-party advertisements to protect themselves from malicious advertisements. One promising approach, used by ADsafe, Dojo Secure, and Jacaranda, sandboxes advertisements by statically verifying that their JavaScript conforms to a safe subset of the language. These systems blacklist known-dangerous properties that would let advertisements escape the sandbox. Unfortunately, this approach does not prevent advertisements from accessing new methods added to the built-in prototype objects by the hosting page. In this paper, we design an algorithm to detect these methods and use our tool to determine experimentally that one-third of the Alexa US top 100 web sites would be exploitable by an ADsafe-verified advertisement. We propose an improved statically verified JavaScript subset that whitelists known-safe properties using namespaces. Our approach maintains the expressiveness and performance of static verification while improving security.
-
Cross-Origin JavaScript Capability Leaks: Detection, Exploitation, and Defense. In Proc. of USENIX Security Symposium, 2009.Visit the project page for code and more information.USENIX presentation slides (with notes).We identify a class of Web browser implementation vulnerabilities, cross-origin JavaScript capability leaks, which occur when the browser leaks a JavaScript pointer from one security origin to another. We devise an algorithm for detecting these vulnerabilities by monitoring the "points-to" relation of the JavaScript heap. Our algorithm finds a number of new vulnerabilities in the open-source WebKit browser engine used by Safari. We propose an approach to mitigate this class of vulnerabilities by adding access control checks to browser JavaScript engines. These access control checks are backwards-compatible because they do not alter semantics of the Web platform. Through an application of the inline cache, we implement these checks with an overhead of 1–2% on industry-standard benchmarks.
-
Composition with Consistent Updates for Abstract State Machines. In Proc. of the International ASM Workshop, 2007.Abstract State Machines (ASMs) offer a formalism for describing state transitions over relational structures. This makes them promising for modeling system features such as access control, especially in an environment where the policy's outcome depends on the evolving state of the system. The current notions of modularity for ASMs, however, provide insufficiently strong guarantees of consistency in the face of parallel update requests. We present a real-world context that illustrates this problem, discuss desirable properties for composition in this context, describe an operator that exhibits these properties, formalize its meaning, and outline its implementation strategy.
Non-Refereed Papers
-
ASM Relational Transducer Security Policies. Technical Report, 2006.We present a model of the security policy for the Web-based Continue conference management tool. The policy model and properties are written as ASM Relational Transducers, which we extend with a module system in order to simplify the handling of conflicting updates. We assume prior familiarity with the security policy concerns surrounding Continue. First, we review the ASM Relational Transducer modeling and property language. Then we describe the basic structure of our policy implementation and demonstrate the ability to model useful properties in the original core ASM language. We exploring the use of the unmodified modeling language in a security policy context and describe typical ASM Relational Transducer complexity concerns and how these minimally impact our implementation. Next, we discuss difficulties encountered in representing our policy and properties in the standard ASM language, including our implementation in the appendices. Following the description of adapting ASMs for use in security modeling, we introduce policy modules and a composition operator to overcome the difficulty of programming in the original language known as the consistent update problem. Finally, we describe a reduction from our extended language to the original language, and prove it satisfies our required correctness property.
