В Python се активират криптофункции с математическо доказателство за надеждност.

Обявено е успешното завършване на инициативата за замяна на криптографските алгоритми в 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* се трансформира в код на C с помощта на компилатора KaRaMeL и е наличен за интеграция с други проекти.

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

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

Източник: opennet.ru