| Title | Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Tsai, Ming-Hsien, Wang, Bow-Yaw, Yang, Bo-Yin |
| Conference Name | Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4946-8 |
| Keywords | cryptography, low-level implementation, pubcrawl, Resiliency, Scalability, Security by Default, verification |
| Abstract | 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 OpenSSH. 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. |
| URL | http://doi.acm.org/10.1145/3133956.3134076 |
| DOI | 10.1145/3133956.3134076 |
| Citation Key | tsai_certified_2017 |
Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs