I'm a Researcher in the RiSE group at MSR Redmond. My work covers various topics including type systems, program logics, functional programming, type-preserving compilation, and interactive theorem proving. I often think about how to use these techniques to build provably secure programs, including web applications, web browsers, crypto protocol implementations, and low-level systems code. A list of my publications is here.

I have been in the past or am currently the co-chair of PLPV 2012 and on the program committees for HOPE 2012, TFP 2012, CSF 2012, PLACES 2012, POST 2012, CSF 2011, PLAS 2011, FTfJP 2010; and on the external review committee for POPL 2012.

Current projects

		F* is a programming language that integrates refinement types, substructural types, mobile proofs, and higher-order polymorphism within a core ML subset of F#. It compiles to compact and verifiable .NET bytecode and interoperates with other .NET languages and frameworks. We have used it to build verified Azure cloud apps, web browser extensions, secure multi-party crypto protocols, new zero-knowledge privacy protocols schemes: in total verifying some 20,000 lines of code. Read more about F* here. Try out some examples of programming in F* using your web browser or mobile device at Rise4fun.com.
		Web browsers like IE, Chrome, Firefox, and Safari can be extended with third party code. Extensions however can compromise the security of the browser platform: for instance, a survey of 1,200 Chrome extensions we conducted found that over 60% of extensions have entirely unrestricted access to a user's browsing history. As part of the IBX project, we are developing a comprehensive new security model for browser extensions based on specifying fine-grained authorization and information flow policies for extensions in Datalog and automatically verifying extension code for policy compliance. Read more about IBX here.
		Even with protections like array-bounds checking in place, C programs remain vulnerable to errors in untrusted third-party libraries. Yarra is a new extension to C that uses a combination of static and dynamic techniques to protect the integrity of critical data structures in a C program from corruption by buggy libraries. We have used Yarra to harden applications ranging from SSH, FTP, and HTTP servers to memory allocators like BGET from non-control data attacks in third party code. Read more about Yarra here.
		Type coercions are surprisingly versatile. They can be used to enforce a variety of programming disciplines ranging from embedding lazy programming in a strict language and operator overloading, to information flow tracking and functional reactivity. Coco is a prototype compiler that applies a theory of type-directed coercion insertion to automatically insert coercions in ML-like programs. Read more about the theory and applications of type coercions here.
		Fine is the predecessor of F*. It extends a core subset of F# with refinement and substructural types, and a simple module system based on a syntactic form of type abstraction. Fine programs are automatically verified using Z3, we extract typeable proof terms from Z3, and compile in a type preserving style to DCIL. We have used it to build a variety of secure applications, including a conference management system and a electronic health-record server. Read more about Fine here and try out some examples of programming in Fine using your web browser or Windows phone at Rise4fun.com.

Before MSR, I was a graduate student at the University of Maryland's programming languages research group. You can find links to my prior projects there.