Schlein Center for Cybersecurity
The Cedar policy language for authorization, and verification-guided development methodologies for building high-assurance systems.
The goal of our project is to build zero-knowledge proof systems for optimization, search, and parsing tasks, as well as building languages for implementing zero-knowledge proof systems.
A formal verification framework that rigorously specifies and mechanizes the semantics of LLVM’s intermediate representation in Coq, enabling mathematically proven correctness of compiler transformations and analyses.
Building a privacy-preserving cross-organization data integration service.
This project advances secure network provenance by enabling accurate, efficient explanation of system states—even during faults or attacks—through robust storage and querying without relying on trusted components.
Research on fuzzing, property-based testing, and their combination to improve software quality and security.
This project develops bounded-time recovery, a security approach that ensures systems meet timing requirements under normal operation and can rapidly return to a correct state after an attack, even in the presence of unpredictable Byzantine failures.
Research on measuring and improving cybersecurity practices, developer behavior, and end-user impact.
