Verifying Curve25519 Software
- 講者蔡明憲 博士 (IIS, Academia Sinica)
邀請人：楊柏因 - 時間2014-08-27 (Wed.) 14:00 ~ 16:00
- 地點資訊所新館106演講廳
摘要
This paper presents results on formal verification of high-speed cryptographic software. We consider speed-record- setting hand-optimized assembly software for Curve25519 elliptic-curve key exchange presented by Bernstein et al. at CHES 2011. Two versions for different microarchitectures are available. We successfully verify the core part of the computation, 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. Es- sential differences between both versions of the software are discussed from a formal-verification perspective.