- This seminar has passed.
Towards a High-Assurance and Specification-Compliant X.509 PKI Implementation
2 February 2022 @ 3:00 pm - 4:00 pm
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.
Zoom meeting link: https://newcastleuniversity.zoom.us/j/88036980317?pwd=Q2xkbkxhLzFYOTRVZGNSR2NucHJmQT09
Meeting ID: 880 3698 0317
Passcode: 293746
Youtube live streaming: https://youtu.be/MHzK_EKCQiY
Youtube VoD
Presenter
-
Omar Haider Chowdhury (University of Iowa)Dr. Omar Haider Chowdhury is an Assistant Professor of Computer Science at the University of Iowa, where he also serves as the co-director of the Computational Logic Center (CLC). He received his Ph.D. in Computer Science at the University of Texas at San Antonio and his BSc. in Computer Science and Engineering from the Bangladesh University of Engineering and Technology. Before joining Iowa, he was a postdoctoral research associate at Carnegie Mellon University and Purdue University. His research focuses on developing principled approaches based on automated reasoning techniques for analyzing and strengthening computer software and networks. His work has appeared in both reputed computer security and formal methods venues including IEEE S&P, ACM CCS, NDSS, ACSAC, CAV, FMCAD, and RV. His research has been supported by both NSF and DARPA including the DARPA Young Faculty Award.