​Mathematical constructs are necessary for computation on the underlying algebraic structures of cryptosystems. They are often written in assembly
​languages and optimized manually for efficiency. We develop a hybrid ​technique to verify mathematical constructs implemented by assembly
​codes in OpenSSL and bitcoin. Our technique translates an algebraic ​specification of mathematical constructs into an algebraic problem.
​The technique also translates overflow and range checking into SMT ​QFBV solvers. To attain high assurance of verification results, we
​have built a formally verified verification tool with certified ​results. We report our case studies on various cryptographic assembly
​programs from classical cryptography to post quantum cryptography.​

​Bow-Yaw Wang is a Research Fellow in Institute of Information Science, Academia Sinica, Taiwan. 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.

​