I am an Assistant Professor in the UCSD CSE Department. I am also the Chief Scientist at Intrinsic (formerly GitStar), a web security start-up I co-founded. My research interests are in building principled and practical secure systems. More broadly, I am interested in research that spans systems, security, and programming languages. My students and I work on several secure systems, spanning from new Web server frameworks (Hails and Frankie), to Web browser architectures (COWL), to constant-time programming languages (FaCT and CT-Wasm), to package managers (SPAM), to multi-core language runtime systems and garbage collectors (LIO, SaferNode.js, and Physis). We are also building benchmarking tools and static bug finding tools to evaluate the performance and security of existing systems and the stuff we build. At Intrinsic, I am putting much research into practice by similarly building systems, tools, and languages that ultimately make it easier for developers to build and deploy web applications with minimal trust.
I am also a member of the W3C WebAppSec Working Group and Node.js Security Working Group.
I completed my Ph.D. in Computer Science at Stanford under "Prof." David Mazières and Prof. John C. Mitchell and (informally) Prof. Alejandro Russo. Prior to Stanford, I obtained a B.E. and M.E. in Electrical Engineering at Cooper Union. At Cooper, I worked on GPU and FPGA crypto implementations. I am still generally interested in hardware architectures, especially in the context of security.
Below are several projects I have been working on. You can read about my broader research vision in my research statement. If you are a student interest in hacking systems or semantics: contact me!
Hails is a Haskell web framework designed for building extensible web platforms. Today's web platforms (e.g., Facebook and Yammer) typically expose REST-like APIs for accessing user data to external apps which, when granted access, can provide new rich functionality. Unfortunately, once granted access, these apps can do as they please with the (often sensitive) data: a malicious or buggy app can easily leak and corrupt user data. This unfortunately forces the end-user to choose between using third-party apps or give up on that functionality to preserve their privacy. To addresses this problem, Hails ties security policies to data using mandatory access control (MAC) or information flow control (IFC) labels. The Hails trusted runtime then ensures that all apps (which now run on the Hails platform) abide by these labels. This allows the platform to treat all apps as untrusted; Hails ensures that these apps cannot leak or corrupt labeled user data. Indeed, core parts of a website can be implemented as untrusted apps, making it easy to build extensible platforms without trading off privacy.
While MAC and IFC systems have been around for a while, Hails stands out as a system that is usable by average developers, today. To this end, we implemented Hails as a library, as opposed to a new language runtime or OS. Moreover, we provide developers with a way of structuring applications in a simple way: Hails just extends the Model-View-Controller architecturewith Policy. Platform developers now only have the additional task of specifying policy. And, Hails makes this an approachable task by tying in the policy with the model definition and providing a declarative, simple policy language for expressing data policies. Expressing high-level concerns in a declarative, simple fashion has been an open challenge for MAC systems. We addressed this challenge and describe the system in the OSDI'12 paper, with a high-level motivation in the POST'14 invited talk. The simple, yet expressive label model used by Hails is described in the NordSec'11 paper.
LIO is a dynamic, language-level decentralized information flow control (DIFC) system. The system explores a new design point in the DIFC space: a mixed-grained DIFC system. This means that LIO typically tracks and controls the flow of information at a coarse grained level (light-weight threads), while still allowing programmers to associate policies (labels) with individual data, when necessary. This has a number of benefits: it allows for the retrofitting of a language with the security mechanism without many changes to its runtime (in Haskell: none); the mechanism can be exposed as a simple API, without changing the language semantics; and, it has a minimal impact on performance. Interestingly, this mixed-grained approach has the expressivity of fine-grained systems in allowing programmers to associate labels with individual values, and the benefit of coarse-grained DIFC OSes in not forcing programmers to understand and reason about many parts of the system: they only need to reason about the data they associate a label with.
The sequential LIO calculus, Coq proofs, and Haskell implementation are described in the JFP paper and Haskell'11 paper. In the ICFP'12 paper we addressed the open challenge of having an expressive concurrent DIFC system that does not leak information through timing covert channels, and showed how to encode flow-sensitive references (common to fine-grained systems) in these calculi in the CSF'14 paper. The demos at PLAS'14 and Haskell'14 show how to build real systems, like Hails, with LIO.
λ→P,Sis a core, but feature-rich language for programming on encrypted data. Secure multiparty computation (SMC) and fully homomorphic encryption (FHE) are promising building blocks for protecting data from untrusted servers; they allow servers to perform computations on encrypted data without access to decryption keys. Unfortunately, existing approaches to programming on encrypted data are restricting: they require compilation to boolean garbled circuits or using APIs in general-purpose languages. The former limits the kinds of programs that can be written, while the latter allows writing programs that cannot be securely executed. λ→P,Sis a new programming language and runtime that addresses these cncerns. The language supports many features common to functional languages such as ML, including conditionals, mutable state, and a form of general recursion. Interestingly, programs are developed and tested using conventional means, without encryption or expert-knowledge of crypto. Using an information-flow type system, our compiler ensures that code that can compile can also run on a secure platform that uses SMC and FHE to provide strong guarantees. The CSF'12 paper and FSTTCS'11 invited talk describe this language, Haskell implementation, and several use cases.
I have served, or am serving, on the program committees for:
Prior to UCSD, I was also an instructor and teaching assistant for several courses at Stanford and Cooper.
Below you will find a select list of papers. Google Scholar has a slightly more complete list.
The following three papers are representative: