Current Lab Members

Abhiram Kothapalli

PhD student

Aymeric Fromherz

PhD student
(advised with Corina Pasareanu)

Jay Bosamiya

PhD student

Josh Gancher

Postdoc 2021-

Lisa Masserova

PhD student
(advised with Vipul Goyal)

Mimi Winchell

Undergrad 2021

Sarah Cai

Undergrad 2021

Sydney Gibson

PhD student

Travis Hance

PhD student

Yi Zhou

PhD student


Alisa Chang

Undergrad 2017-2018

Anne Kohlbrenner

Undergrad 2017-2019

Benjamin Lim

MS 2018-2019

Jack Cameron

Undergrad 2020-2021

Michael Laurent

MS Visitor 2018

Steve Matsumoto

PhD 2017-2019; Assistant Professor @ Olin College

Valerie Choung

Undergrad 2020-2021

Xueyuan Zhao

MS 2018-2019

Yucheng Dai

Undergrad 2019

Recent Research Projects

  • image


    Building and Deploying a Verified HTTPS Stack

    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 definitively solve this problem by constructing a high-performance, standards-compliant, verified 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.

  • image


    Building Provably Secure & Reliable Systems

    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.

  • image

    Verifiable Computing

    Securely Outsourcing Computation to the Cloud: From Cryptographic Theory to Practice

    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.

  • image

    App Security

    New Application Security Models

    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.

Research Sponsors

We are grateful to all of the organizations who have provided funding for the research our lab performs.

Alfred P. Sloan Foundation Google VMware
DARPA Bosch Intel