Our research is primarily focused on investigating long-term, fundamental improvements in how to design and build secure systems. As a result, our work combines theory and practice to provide formal, rigorous security guarantees about concrete systems, with an emphasis on creating solid foundations for practical solutions. We are 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.
Our current work focuses on protocols for verifiable computation and zero-knowledge proofs, building practical, formally verified secure systems, and developing next-generation application models.
We aim to make our results reproducible and of wider use to the public. Hence, we publish our work in a variety of conferences and make our papers freely available online; we default to open sourcing our code and other artifacts online, typically under BSD or Apache licenses; and we do not typically patent our results.
We are a part of CyLab, CMU's Security & Privacy Institute.
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.
We are fortunate that our work has impacted the real world in a variety of ways. Here are some examples.
We are grateful to all of the organizations who have provided funding for the research our lab performs.