В Python подготовлены криптоалгоритмы с математическим доказательством надёжности

Разработчик Джонатан Проценко из Microsoft Research сообщил об успешном завершении инициативы по замене в Python реализаций криптографических алгоритмов, предлагаемых в модулях hashlib и hmac, на варианты с математическим (формальным) доказательством надёжности, подготовленные проектом HACL*. Работа по переходу на функции с математическим доказательством надёжности велась с 2022 года и была инициирована после выявления переполнения буфера в реализации алгоритма SHA3, используемой в Python‑модуле hashlib.

По информации OpenNET, в основной репозиторий проекта СPython принят код с новыми реализациями криптографических хэш‑функций и алгоритмов HMAC (механизм проверки подлинности сообщений). Все предоставляемые по умолчанию в Python хэш‑функции и HMAC заменены на варианты, для которых предоставлено формальное доказательство соответствия (формальная верификация). Среди прочего, добавлена реализация HMAC‑BLAKE2, использующая SIMD‑инструкции AVX2 для ускорения вычислений. Предполагается, что верифицированный код войдёт в состав осеннего релиза Python 3.14.

Новые реализации криптографических функций перенесены из библиотеки HACL*, развиваемой исследователями из французского государственного института исследований в информатике и автоматике (INRIA), подразделения Microsoft Research и университета Карнеги — Меллона. Библиотека HACL* поддерживает типовые криптографические функции, которых достаточно для работы TLS 1.3 и полной поддержки API NaCl (Networking and Cryptography library), такие как Curve25 519, Ed25 519, AES‑GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC и HKDF. По производительности библиотека HACL* близка к OpenSSL, но в отличие от последней предоставляет дополнительные гарантии надёжности и безопасности.

Код HACL*