In order to achieve security, protocol implementations not only need to avoid low-level memory access errors, but also faithfully follow and fulfill the requirements prescribed by the protocol specifications at the semantic level. In this talk, I will focus on how to use symbolic execution to analyze semantic correctness of protocol implementations. I will first present our recent work on analyzing implementations of X.509 certificate validation. Our analysis of 9 small footprint TLS libraries has uncovered 48 instances of noncompliance, as well as some inaccurate claims in a previous work based on blackbox fuzzing. I will then present our most recent work on analyzing implementations of PKCS#1 v1.5 RSA signature verification, and explain how some of the implementation flaws we found can lead to new variants of the Bleichenbacher-style low-exponent RSA signature forgery.
Sze Yiu Chau is a PhD candidate at Purdue University, Department of Computer Science, working with Prof. Ninghui Li and Prof. Aniket Kate. His research interest is mainly on the (in)secure design and implementation of widely deployed systems and network protocols. In particular, he and his colleagues have investigated exploitable weaknesses in many popular content delivery apps on Android, as well as the robustness of X.509 certificate
validation and RSA signature verification implemented in various open source software, which led to the discovery of many vulnerabilities with varying degrees of severity. Prior to joining Purdue, Sze Yiu received his BSc in Information Technology from The Hong Kong Polytechnic University with First-class honours.