Current Lab Members

Lisa Masserova

PhD student
(advised with Vipul Goyal)

Mike McLoughlin

PhD student
(advised with Fraser Brown)

Paul Hitchcox

Undergrad 2024

Pratap Singh

PhD student

Rory Brennan-Jones

Undergrad 2024

Sydney Gibson

PhD student

Travis Hance

PhD student

Yi Zhou

PhD student

Zhengyao Lin

PhD student

Alumni

Abhiram Kothapalli

PhD student 2018-2024
Postdoc at UC Berkeley

Alex Bai

Undergrad 2023

Alisa Chang

Undergrad 2017-2018

Anne Kohlbrenner

Undergrad 2017-2019
Professor at Carnegie Mellon University

Aymeric Fromherz

PhD 2017-2021
(advised with Corina Pasareanu)
Researcher at Inria

Benjamin Lim

MS student 2018-2019

Chanhee Cho

MS student 2021-2023
PhD student at Carnegie Mellon University

Jack Cameron

Undergrad 2020-2021

Jay Bosamiya

PhD student 2017-2024
Senior Researcher at Microsoft Research

Jessica Li

Undergrad 2023

Josh Gancher

Postdoc 2021-2024
Professor at Northeastern University

Liz Austell

Undergrad 2023

Michael Laurent

MS visitor 2018

Mimi Winchell

Undergrad 2021

Samvid Dharanikota

MS student 2022

Sarah Cai

Undergrad 2021

Steve Matsumoto

PhD 2017-2019
Assistant Professor @ Olin College

Valerie Choung

Undergrad 2020-2021
PhD student at Carnegie Mellon University

Xueyuan Zhao

MS student 2018-2019

Yi Cai

MS student 2023-2024
PhD student at University of Maryland

Yucheng Dai

Undergrad 2019

Recent Research Projects

  • image

    Verus

    Verifying Systems Code Written in Rust

    Writing high-performance low-level code that is correct, reliable, and secure is notoriously difficult, and yet increasingly critical. We are developing a new tool, Verus, that leverages the sophisticated design and engineering of the Rust language to enable full verification of such systems code. Verification enables developers to prove strong properties (including functional correctness, reliability and security) about their Rust code and, in many cases, avoid the risks of using unsafe Rust code. In the other direction, Rust's linearity and type checkers can simplify proofs about low-level code correctness, and even enable developers to ergonomically reason about shared-memory concurrency. Building on our prior experience with systems verification in the Ironclad and Everest projects, Verus includes dedicated automation to address the thorny verification problems that arise in a systems setting.

  • image

    Everest

    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

    Ironclad

    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 Impact

We are fortunate that our work has impacted the real world in a variety of ways. Here are some examples.

Research Sponsors

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

NSF ONR SRC
Alfred P. Sloan Foundation Google VMware
DARPA Bosch Intel
Amazon