Seminars & Colloquia
"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)
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.
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