Curve25519 verification in SPARK2014

Note: This repository does not provide a full implementation of curve25519.

This project was inspired by this article, a “disappointing” attempt to verify some basic functions from a curve25519 implementation available here.

The SPARK2014 code for implementation of functions in src/curve25519.adb is a translation and/or adaptation from the C code in curve25519-donna repository.

Tools used

GNAT Community 2019 has been used for this project. You may download and install it by following the previous link.

Verification

To avoid overflow checks in ghost code, a non-executable big integers library was created, inspired from an upcoming big integers library in Ada 2020.

An axiomatization of this library in Why3 was done to be able to use it in proofs. For more information about external axiomatization in SPARK, see here.

All proofs are run on a machine equipped with an Intel Core i7-7700HQ CPU and 16 GB of RAM.

Content of each directory

• src directory contains all source files: big integers library, files containing ghost code, curve25519 partial implementation
• proof/_theories contains the external axiomatization for src/big_integers.ads, as specified in project file test.gpr

More about curve25519

Daniel J. Bernstein provides an implementation of curve25519 and links to learn more about curve25519 in http://cr.yp.to/ecdh.html.