End-to-end verification of elliptic curve cryptographic primitives: From specification to secure code

Abstract

   Objectives. The work set out to develop and substantiate a methodology for synthesizing high-performance and simultaneously verified implementations of elliptic curve cryptosystems.    The challenge of ensuring mathematical correctness and engineering security of the code was overcome by integrating machine-checkable proofs with automated inspection.    Methods. In order to carry out formal verification within the Coq interactive environment 6 , the study employs ring 7 and nsatz8 tactics to automate algebraic proofs together with custom fold-based synthesis methods. For low-level security analysis, static range analysis and deductive verification are carried out within Frama-C 9 . The efficiency of the resulting solutions is evaluated through a comparative analysis of arithmetic complexity and execution time.    Results. The proposed approach is implemented by generating executable C code alongside a formal proof of its conformance to a simple mathematical specification to ensure the absence of algorithmic errors. Despite the rigor of the formal methods, the achieved performance approaches that of the best hand-optimized implementations. A key achievement consists in the development of a two-layer architecture for verified finite field arithmetic, which permits the extensive reuse of proofs across different curves and parameters. As part of the research, an explicit multiplication formula for the Curve25519 10 curve in a 10-limb representation with weights 2 ⌈25.5i⌉ was synthesized and formally verified for the first time. This formula is identical to the classic high-performance implementation by Bernstein and Schwabe.    Conclusions. An end-to-end Coq → Frama-C pipeline was successfully built and tested, providing an end-to-end correctness guarantee: from the mathematical specification of elliptic curves to optimized C code verified for overflows, array index out-of-bounds error, and timing variability. The feasibility of the proposed approach is confirmed by the final performance of the synthesized code, which falls within 7 % of the best manually optimized implementations on the target architecture.