Сквозная верификация криптографических примитивов на эллиптических кривых от спецификации к безопасному коду

   Цели. Цель работы – разработка и обоснование методологии синтеза высокопроизводительных и одновременно верифицированных реализаций криптосистем на эллиптических кривых.

   Ключевой задачей является обеспечение не только математической корректности, но и инженерной безопасности кода, что достигается путем интеграции машинно-проверяемых доказательств с автоматической инспекцией.

   Методы. Работа опирается на формальную верификацию в интерактивной среде Coq¹ (ребрендинг с марта 2025 г.) с применением тактик ring² и nsatz³ для автоматизации алгебраических доказательств, а также на разработанные одним из авторов методы синтеза на основе свертки. Для анализа безопасности на низком уровне используются статический анализ диапазонов и дедуктивная верификация на платформе Frama-C⁴. Эффективность полученных решений оценивается путем сравнительного анализа арифметической сложности и времени выполнения.

   Результаты. Предложен и реализован подход, при котором исполняемый код на языке C создается вместе с формальным доказательством его соответствия простой математической спецификации, что гарантирует отсутствие алгоритмических ошибок. Несмотря на строгость формальных методов, достигнутая производительность приближается к лучшим ручным реализациям. Ключевым достижением является разработка двухуровневой архитектуры верифицированной арифметики конечных полей, которая позволяет многократно переиспользовать доказательства для различных кривых и параметров. В рамках исследования впервые синтезирована и формально верифицирована явная формула умножения для кривой Curve25519⁵ в 10-лимбовом представлении с весами 2^⌈25.5i⌉, которая полностью идентична классической высокооптимизированной реализации Бернштейна – Швабе.

   Выводы. Построен и успешно апробирован сквозной конвейер Coq → Frama-C, обеспечивающий сквозную гарантию корректности: от математической спецификации эллиптических кривых до оптимизированного кода на C, проверенного на отсутствие переполнений, выходов за границы массивов и непостоянство времени. Итоговая производительность синтезированного кода составляет не более 7 % потерь по сравнению с лучшими ручными реализациями на целевой архитектуре, что доказывает практическую применимость предложенной методологии.

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