Объявлено об успешном завершении инициативы по замене в Python реализаций криптографических алгоритмов, предлагаемых в модулях hashlib и hmac, на варианты с математическим доказательством надёжности, подготовленные проектом "HACL*". Работа по переходу на функции с математическим доказательством надёжности велась с 2022 года и была инициирована после выявления переполнения буфера в реализации алгоритма SHA3, используемой в Python-модуле hashlib.

В основной репозиторий проекта С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), такие как Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC и HKDF. По производительности библиотека HACL* близка к OpenSSL, но в отличие от последней предоставляет дополнительные гарантии надёжности и безопасности.

Код HACL* написан на подмножестве функционального языка F*, предлагающем систему зависимых типов и уточнений, позволяющих задавать точные спецификации (математическую модель) и гарантировать отсутствие ошибок в реализации при помощи SMT-формул и вспомогательных инструментов доказательства. Эталонный код на F* транслируется в код на языке Си при помощи компилятора KaRaMeL и доступен для интеграции с другими проектами.

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

Процесс перехода на верифицированный код занял два с половиной года и потребовал доработки библиотеки HACL*, функциональность которой была расширена возможностями, необходимыми для прозрачной замены имеющейся функциональности hashlib. Например, в HACL* была добавлена поддержка потокового режима работы HMAC, предоставлены дополнительные режимы работы алгоритмов Blake2, реализован новый API для SHA3, охватывающий все варианты алгоритмов семейства Keccak, обеспечены необходимые средства уведомления об ошибках (например, при проблемах с выделением памяти), разработаны скрипты для автоматизации переноса в репозиторий Python новых версий HACL*.