Seminars & Colloquia

Will Enck - Guest


"Towards a High-Assurance and Specification-Compliant X.509 PKI Implementation"

Friday April 01, 2022 10:00 AM
Location: 3211, EB2 NCSU Centennial Campus
Zoom Meeting Info
(Visitor parking instructions)


Abstract: The X.509 Public-Key Infrastructure (PKI) is one of the most prominent and widely used authentication mechanisms, which plays a crucial role in different applications such as secure communication (e.g., SSL/TLS, IPSec), software updates, and emails. Flaws in an X.509 PKI implementation can make an application relying on X.509 PKI susceptible to impersonation attacks or interoperability issues. In this talk, I will discuss my group's effort in developing a high-assurance and specification-compliant implementation of X.509 PKI.


First, I will discuss the Symcerts system that uses domain-specific optimizations, symbolic execution, and differential analysis to automatically identify specification non-compliance in open-source SSL/TLS libraries. Second, I will discuss Morpheus, a black-box analysis engine that automatically checks the logical correctness of RSA signature verification implementations in open-source SSL/TLS libraries through a formally verified oracle. Third, I will discuss my group's effort to formalize and re-engineer the specification of the X.509 certificate chain validation using an executable specification. I will conclude my talk with a sneak peek of our ongoing work on developing a formally verified implementation of the X.509 PKI, and other relevant efforts.

Short Bio: None listed.

Special Instructions: Please do not list this applicant's name. His bio is not included. As a note: applicant requested we not advertise the talk on a public website and just advertise to our faculty and students.

Host: William Enck, CSC

Back to Seminar Listings
Back to Colloquia Home Page