Doctoral Speaking Skills Talk - Pratap Singh

— 1:00pm

Location:
In Person - Mehrabian Collaborative Innovation Center 1301

Speaker:
PRATAP SINGH , Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://pratap.dev/

Owl: Bringing Verified Cryptographic Protocols to Practice

Cryptographic security protocols, such as TLS or WireGuard, form the foundation of a secure Internet, but vulnerabilities are discovered in them with alarming frequency. Formal verification promises a foundational solution to this problem, with significant prior work on mechanizing cryptographic proofs of high-level protocol designs, and more recent work on verifying particular implementations of single protocols against higher-level specifications. 

In this talk, I will discuss our work on Owl, a verifier and secure compiler for cryptographic protocols. Owl's verifier uses a novel combination of information-flow and refinement types to prove security in the computational model, enabling greater modularity and automation than prior computational tools. Owl's compiler translates well-typed protocols into performant, interoperable, side-channel resistant Rust libraries that are automatically formally verified to be correct. With Owl, developers can define and prove security for their protocols in an intuitive, high-level language, and obtain for free a drop-in executable implementation with formal guarantees of correctness and security. 

We evaluate Owl using a range of case studies. We verify the core logic of 14 protocols, including SSH and Kerberos. We additionally develop two large-scale, interoperable case studies for WireGuard and Hybrid Public-Key Encryption (HPKE), yielding verified implementations that interoperate with, and match the performance of, existing industrial baselines on end-to-end benchmarks. 

Presented as part of the CyLab Student Seminar Series
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement

Add event to Google
Add event to iCal