【04-16】Certified Verification of Cryptographic Primitive Programs
文章来源： | 发布时间：2025-04-15 | 【打印】 【关闭】
| Title: | Certified Verification of Cryptographic Primitive Programs |
| Speaker: | 王柏尧（研究员, Academia Sinica） |
| Time: | 2025年4月16日（周三），上午10:00 |
| Venue: | 中国科学院软件研究所5号楼3层334报告厅 |
| Abstract: | 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, bitcoin, and PQClean. Our technique combines algebraic reasoning and SMT QFBV solving. To attain high assurance of verification results, we use Coq to verify our technique and extract OCAML programs to build CoqCryptoLine. To ensure each verification task is solved correctly, we employ verified certificate checkers to validate answers from external solvers. We report our case studies on various cryptographic assembly programs from classical cryptography to post quantum cryptography. |
| Bio: | Bow-Yaw Wang is a Research Fellow in Institute of Information Science, Academia Sinica, Taiwan, China. 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 PQClean. |
