Efficient Verification of Optimized Code: Correct High-speed X25519

Marc Schoolderman, Jonathan Moerman, Sjaak Smetsers +1

Code that is highly optimized poses a problem for program-level verification: programmers can employ various clever tricks that are non-trivial to reason about. For cryptography on…