Prof. Bow-Yaw Wang
Biography
Prof. Bow-Yaw Wang is a Research Fellow in Institute of Information Science, Academia Sinica, Taiwan. He was an Associate Research Fellow at Academia Sinica from 2008 to 2012, an INRIA Invited Professor from 2009 to 2011, an Invited Associate Professor at Tsinghua University from 2009 to 2010, an Adjoint Associate Professor at National Taiwan University from 2009 to 2012, an Assistant Research Fellow at Academia Sinica from 2003 to 2008, and an Adjoint Assistant Professor at National Taiwan University from 2004 to 2009. His research interest is logic and its application in computer science. He mainly works on formal verification. In the past, he has been working on compositional reasoning, program verification, learning-based verification techniques. More recently, he is interested in verifying assembly implementations of cryptographic primitives from security libraries such as OpenSSL and boringSSL. He is also running an interdisciplinary privacy research project at Academia Sinica.
Abstract
Cryptographic programs are widely used in computer systems. From on-line banking to identification cards, sensitive information is encrypted by various cryptosystems from computer cryptography. Cryptographic programs are subsequently one of the most critical software in modern world. In this lecture, I will motivate the research of verifying assembly cryptographic programs in practical cryptography. We will see the limitation of existing verification techniques. Finally, I will introduce our hybrid technique CryptoLine for the functional verification of assembly cryptographic programs. We will see how CryptoLine is applied to verify assembly programs in OpenSSL.