Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs
Mathematical constructs are necessary for computation on the underlying algebraic structures of cryptosystems. They are often written in assembly language and optimized manually for efficiency. We develop a certified technique to verify low-level mathematical constructs in X25519, the default elliptic curve Diffie-Hellman key exchange protocol used in OpenSSL. Our technique translates an algebraic specification of mathematical constructs into an algebraic problem. The algebraic problem in turn is solved by the computer algebra system Singular. The proof assistant Coq certifies the translation and solution to algebraic problems. Specifications about output ranges and potential program overflows are translated to SMT problems and verified by SMT solvers. We report our case studies on verifying arithmetic computation over a large finite field and the Montgomery Ladderstep, a crucial loop in X25519.
Bow-Yaw Wang is a Research Fellow in Institute of Information Science, Academia Sinica since 2012. He visited the FORMES group at Tsinghua University from 2009 to 2011. His research interests include model checking and particularly compositional reasoning. He has applied learning-based techniques to verifying classical and probabilistic systems, and to program verification.