UK-SPS Seminar - 2nd Feb 2022 Title: Towards a High-Assurance

The UK-SPS Seminar:

Time: Wed, February 2 2022

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

Speaker: Omar Haider Chowdhury (University of Iowa)

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.

Bio: 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.

Please feel free to forward to others who might be interested. 

UK-SPS is an inter-university seminar series on cyber security and privacy. Seminar details are also advertised on our website, calendar and Twitter, and recordings will be available on our YouTube channel afterwards. 

Last modified: Mon, 07 Feb 2022 10:09:33 GMT