My research is primarily focused on investigating long-term, fundamental improvements in how to design and build secure systems. As a result, my work combines theory and practice to provide formal, rigorous security guarantees about concrete systems, with an emphasis on creating solid foundations for practical solutions. I am interested in a broad range of security topics (e.g., network and system security, applied cryptography, usable security, and data privacy), as well as topics such as operating system design and distributed systems.
My current work focuses on protocols for verifiable computation and zero-knowledge proofs, building practical, formally verified secure systems, and developing next-generation application models.
I'm actively looking for graduate students and postdocs who interested in building secure systems that can provide end-to-end guarantees. Prospective graduate students should first apply to CMU CSD and/or ECE and contact me when admitted. See Dave Andersen's explanation for why my ability to respond pre-admission is limited.
In my time at Microsoft Research, I was fortunate to work with many excellent interns, including Ashay Rane, Ben Kreuter, Karthik Nagaraj, Laure Thompson, Mariana Raykova, Joshua Schiffman, Srinath Setty, Sai Deep Tetali, Xi Xiong, and Samee Zahur.
The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks such as FREAK and LogJam, and emergency patches many times a year.
Building on our experience with Ironclad, MiTLS, and other related projects, Project Everest proposes to deﬁnitively solve this problem by constructing a high-performance, standards-compliant, veriﬁed implementation of the full HTTPS ecosystem, from the HTTPS API down to and including cryptographic algorithms such as RSA and AES. At the TLS level, for instance, we will develop new implementations of existing protocol standards and formally prove, by reduction to cryptographic assumptions on their core algorithms, that our implementations provide a secure-channel abstraction between the communicating endpoints. Project Everest aims to be a drop-in replacement for the HTTPS library in mainstream web browsers, servers, and other popular tools.
While verifiable computation provides strong guarantees, even the best cryptographic system is useless if implemented badly, applied incorrectly, or used in a vulnerable system. Thus, the Ironclad project works to expand formal software verification to provide end-to-end guarantees about the security and reliability of complex systems. By creating a set of new tools and methodologies, Ironclad produced the first complete stack of verified-secure software. We also recently developed the first methodology for verifying both the safety and liveness of complex distributed systems implementations. Many interesting challenges remain, including verifying concurrent or probabilistic programs, improving the performance of verifiers and verified code, and enhancing the stability of automated proofs. Nonetheless, I expect that verification will fundamentally improve the software that underpins our digital and physical infrastructure.
To provide strong guarantees for outsourced computations, we developed a new cryptographic framework, Verifiable Computation, which allows clients to outsource general computations to completely untrusted services and efficiently verify the correctness of each returned result. Through improvements to the theory and the underlying systems over the last few years, we reduced the costs of verification by over twenty orders of magnitude. As a result, verifiable computation is now a thriving research area that has produced several startups, as well as enhancements to the security and privacy of X.509, MapReduce, and Bitcoin. We are continuing to explore improvements and applications in this space, as well as other settings where cryptographic advances can be deployed to create fundamentally more secure services.
In the last decade, we've seen the rise of modern client platforms like iOS, Android, and even web browsers. On each platform, unlike on the traditional desktop, applications are strongly isolated. A key challenge, however, is determining how and when the platform should grant applications access to user-owned resources, e.g., to sensitive devices like the camera or to user data residing in other applications. Previous systems either granted access by prompting the user (Windows 7, iOS), relied on install-time manifests (Android), or both (Windows Phone). Unfortunately, multiple studies indicate the futility of these measures; in practice, users ignore them both.
We designed a brand new approach called user-driven access control, whereby permission granting is built into existing user actions.
We also reenvisioned the web interface based on the notion of a client-side pico-datacenter. Just as in the cloud datacenter, the simple client semantics make isolation tractable while giving web applications the freedom to run any software stack. Since the datacenter model is designed to be robust to malicious tenants, it is never dangerous for the user to click on a URL.
I am grateful to all of the organizations who have provided funding for the research my group performs.