12/31 (三) 論文研討─資訊科學與工程 的演講相關資料如下，歡迎聽講！

演講者：蔡明憲博士 Dr. Ming-Hsien Tsai (中研院資訊所)

時間：12/31 (三) 13:20-15:10

地點：工程四館 B1 027

主持人：曾建超教授

主題：Software Verification - Verifying Curve25519 Software

講題簡述：

This talk includes an introduction to formal software verification and a recent work on verifying Curve25519 software. Compared to testing and code auditing, formal verification provides strong guarantee of software correctness but is still unable to verify a large-scale software system in with rich programming language features are applied. In this work, we consider speed-record-setting hand-optimized assembly software for Curve25519 elliptic-curve key exchange presented by Bernstein et al. at CHES 2011. The core part of the computation is implemented in the portable assembly language qhasm without using programming language features such as loops, recursion, pointers, and concurrency that are harder for verification. We successfully verify the core part and reproduce detection of a bug in a previously published edition. An SMT solver supporting array and bit-vector theories is used to establish almost all properties. Remaining properties are verified in a proof assistant with simple rewrite tactics. We also exploit the compositionality of Hoare logic to address the scalability issue.