Title: Verification of Cryptographic Software
Speaker: Dr. Ming-Hsien Tsai
Software failures in critical systems may cause severe damage. For example, bugs in cryptographic software may induce security vulnerabilities that can be utilized by adversaries to steal personal property, retrieve sensitive data, or gain unauthorized access to systems. It is thus important to assure correctness and security of cryptographic software. Especially there are new implementations of post-quantum cryptographic algorithms actively developed due to the threat from quantum computers. Formal verification is a technique that can provide a high level of correctness and security assurance. In this talk, we will review the state-of-the-art verification of cryptographic software.
Dr. Ming-Hsien Tsai is an associate researcher in National Institute of Cyber Security (NICS). He received his PhD degree from National Taiwan University. His research interests include formal verification, program analysis, logics for computer science, automata, and software quality.