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

   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⁶, the study employs ring⁷ 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⁹. 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¹⁰ 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.

1. Nakibly G., Schcolnik J., Rubin Y. Website-Targeted False Content Injection by Network Operators. In: Proceedings of the 25^th USENIX Conference on Security Symposium (SEC 2016). USENIX Association, USA. 2016. P. 227–244. doi: 10.48550/arXiv.1602.07128

2. Van der Velden L. Forensic devices for activism: Metadata tracking and public proof. Big Data & Society. 2015;2(2). doi: 10.1177/2053951715612823

3. Bolognini L., Bistolfi C. Pseudonymization and impacts of Big (personal/anonymous) Data processing in the transition from the Directive 95/46/EC to the new EU General Data Protection Regulation. Computer Law & Security Rev. 2017;33(2):171–181. doi: 10.1016/j.clsr.2016.11.002

4. Telang R. Policy Framework for Data Breaches. IEEE Security & Privacy. 2015;13(1):77–79. doi: 10.1109/MSP.2015.12

5. Zhang X., Jin S., He Y., Hassan A., Mao Z.M., Qian F., et al. QUIC is not Quick Enough over Fast Internet. In: Proceedings of the ACM Web Conference 2024 (WWW 2024). New York, NY, USA: Association for Computing Machinery. 2024. P. 2713–2722. doi: 10.1145/3589334.3645323

6. Holz R., Hiller J., Amann J., Razaghpanah A., Jost T., Vallina-Rodriguez N., Hohlfeld O. Tracking the deployment of TLS 1.3 on the web: a story of experimentation and centralization. SIGCOMM Comput. Commun. Rev. 2020;50(3):3–15. doi: 10.1145/3411740.3411742

7. Simpson A., Alshaali M., Tu W., Asghar R. Quick UDP Internet Connections and Transmission Control Protocol in unsafe networks: A comparative analysis. IET Smart Cities. 2024;6(4):351–360. doi: 10.1049/smc2.12083

8. Kubota T., Kakutani Y., Kato G., Kawano Y., Sakurada H. Semi-automated verification of security proofs of quantum cryptographic protocols. J. Symb. Comput. 2016;73:192–220. doi: 10.1016/j.jsc.2015.05.001

9. Daniel A., Krishnaraj N., Venkatraman S., Maheswaravenkatesh P. Post-quantum lightweight cryptography algorithms and approaches for IoT and block chain security. In: Raj P., Saini K., Gupta B.B. (Eds.). Advances in Computers. Elsevier; 2025. V. 138. P. 349–376. doi: 10.1016/bs.adcom.2025.03.001

10. Montenegro J.A., Rios R., Lopez-Cerezo J. A performance evaluation framework for post-quantum TLS. Future Gener. Comput. Syst. 2026;175:108062. doi: 10.1016/j.future.2025.108062

11. Polubelova M., Bhargavan K., Protzenko J., Beurdouche B., Fromherz A., Kulatova N., Zanella-Béguelin S. HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms). In: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security (CCS 2020). Association for Computing Machinery, New York, NY, USA. 2020. P. 899–918. doi: 10.1145/3372297.3423352

12. Erbsen A., Philipoom J., Jamner D., Lin A., Gruetter S., Pit-Claudel C., et al. Foundational Integration Verification of a Cryptographic Server. In: Proceedings of the ACM Programming Languages. 2024;8(PLDI):1704–1729. doi: 10.1145/3656446

13. Busi M., Focardi R., Luccio F.L. Strands Rocq: Why is a Security Protocol Correct, Mechanically? In: 2025 IEEE 38^th Computer Security Foundations Symposium (CSF), Santa Cruz, CA, USA. 2025. P. 33–48. doi: 10.1109/CSF64896.2025.00022

14. Rao V., Ilioaea I., Ondricek H., Kalla P., Enescu F. Word-Level Multi-Fix Rectifiability of Finite Field Arithmetic Circuits. In: 2021 22^nd International Symposium on Quality Electronic Design (ISQED). Santa Clara, CA, USA: IEEE; 2021. P. 41–47. doi: 10.1109/ISQED51717.2021.9424286

15. Bhargavan K., Jacomme C., Kiefer F., Schmidt R. Formal verification of the PQXDH post-quantum key agreement protocol for end-to-end secure messaging. In: Proceedings of the 33^rd USENIX Conference on Security Symposium (SEC 2024). USENIX Association, USA. 2024. V. 27. P. 469–486.

16. Affeldt R. On construction of a library of formally verified low-level arithmetic functions. In: Proceedings of the 27^th Annual ACM Symposium on Applied Computing (SAC 2012). New York, NY, USA: Association for Computing Machinery; 2012. P. 1326–1331. doi: 10.1145/2245276.2231986

17. Delaware B., Suriyakarn S., Pit-Claudel C., Ye Q., Chlipala A. Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. In: Proceedings of the ACM on Programming Languages. 2019;3(ICFP):1–29. doi: 10.1145/3341686

18. Pit-Claudel C., Wang P., Delaware B., Gross J., Chlipala A. Extensible extraction of efficient imperative programs with foreign functions, manually managed memory, and proofs. In: Peltier N., Sofronie-Stokkermans V. (Eds.). Automated Reasoning. IJCAR 2020. Lecture Notes in Computer Science. 2020. V. 12167. P. 119–137. doi: 10.1007/978-3-030-51054-1_7

19. Chlipala A., Delaware B., Duchovni S., Gross J., Pit-Claudel C., Suriyakarn S., et al. The End of History? Using a Proof Assistant to Replace Language Design with Library Design. In: LIPIcs-Leibniz International Proceedings in Informatics. 2017;71:3.1–3.15. doi: 10.4230/LIPIcs.SNAPL.2017.3

20. Kosmatov N., Prevosto V., Signoles J. Guide to Software Verification with Frama-C: Core Components, Usages, and Applications. 1^st ed. Cham: Springer International Publishing; 2024, 697 p. (Computer Science Foundations and Applied Logic). doi: 10.1007/978-3-031-55608-1

21. Volkov G., Mandrykin M., Efremov D. Lemma Functions for Frama-C: C Programs as Proofs. 2018. P. 31–38. doi: 10.48550/arXiv.1811.05879

22. Ye Q., Delaware B. A verified protocol buffer compiler. In: Proceedings of the 8^th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019). Association for Computing Machinery, New York, NY, USA. 2019. P. 222–233. doi: 10.1145/3293880.3294105