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

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

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

Новите реализации на криптографските функции са пренесени от библиотеката HACL*, развивана от изследователи от френския държавен институт за изследвания в информатиката и автоматизацията (INRIA), подразделение на Microsoft Research и университета Карнеги — Мелон. Библиотеката HACL* поддържа типовите криптографски функции, необходими за работа с TLS 1.3 и пълна поддръжка на API NaCl (Библиотека за мрежова свързаност и криптография), като 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