Ogłoszono pomyślne zakończenie inicjatywy mającej na celu wymianę w Pythonie implementacji algorytmów kryptograficznych dostarczanych przez moduły hashlib i hmac na wersje z dowodem matematycznym ich niezawodności, opracowane przez projekt „HACL*”. Prace nad przejściem na funkcje z dowodem matematycznym ich niezawodności rozpoczęły się w 2022 roku po ujawnieniu problemu z przepełnieniem bufora w implementacji algorytmu SHA3, używanego w module hashlib w Pythonie.
Do głównego repozytorium projektu CPython przyjęto kod z nowymi implementacjami kryptograficznych funkcji haszujących i algorytmów HMAC (mechanizm weryfikacji autentyczności wiadomości). Wszystkie domyślnie dostarczane w Pythonie funkcje haszujące i HMAC zostały zastąpione zweryfikowanymi wersjami. Wśród nich dodano implementację HMAC-BLAKE2, wykorzystującą instrukcje SIMD AVX2 do przyspieszenia obliczeń. Zakłada się, że zweryfikowany kod wejdzie w skład jesiennej wersji Pythona 3.14.
Nowe implementacje funkcji kryptograficznych zostały przeniesione z biblioteki HACL*, rozwijanej przez badaczy z francuskiego państwowego instytutu badań w informatyce i automatyce (INRIA), działu Microsoft Research oraz Uniwersytetu Carnegiego — Melona. Biblioteka HACL* obsługuje typowe funkcje kryptograficzne, które są wystarczające do pracy z TLS 1.3 i pełną obsługą API NaCl (Networking and Cryptography library), takie jak Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC i HKDF. Pod względem wydajności biblioteka HACL* jest zbliżona do OpenSSL, ale w przeciwieństwie do niej zapewnia dodatkowe gwarancje niezawodności i bezpieczeństwa.
Kod HACL* został napisany w podzbiorze funkcjonalnego języka F*, który oferuje system typów zależnych i udoskonaleń, umożliwiających ustalanie dokładnych specyfikacji (matematyczny model) i zapewnienie braku błędów w implementacji przy użyciu formuł SMT i wspomagających narzędzi dowodzenia. Referencyjny kod w F* jest transkodowany do kodu w języku C za pomocą kompilatora KaRaMeL i jest dostępny do integracji z innymi projektami.
Weryfikacja polega na określeniu szczegółowych specyfikacji opisujących wszelkie możliwe zachowania programu oraz na stworzeniu dowodu matematycznego, że napisany kod w pełni odpowiada przygotowanym specyfikacjom. Weryfikacja gwarantuje, że program będzie działał tylko w sposób zamierzony przez twórców i że nie zawiera pewnych klas błędów, takich jak przepełnienie bufora, dereferencja wskaźników, dostęp do już zwolnionych obszarów pamięci lub podwójne zwolnienie bloków pamięci. Proces kompilacji zapewnia ścisłą kontrolę typów i wartości - jeden komponent nigdy nie przekaże drugiemu komponentowi parametrów, które nie odpowiadają specyfikacji, i nie uzyska dostępu do wewnętrznych stanów innych komponentów.
Proces przejścia na zweryfikowany kod zajął dwa i pół roku i wymagał dopracowania biblioteki HACL*, której funkcjonalność została rozszerzona o możliwości niezbędne do bezproblemowej wymiany istniejącej funkcjonalności hashlib. Na przykład, w HACL* dodano wsparcie dla trybu strumieniowego HMAC, udostępniono dodatkowe tryby działania algorytmów Blake2, wprowadzono nowe API dla SHA3, obejmujące wszystkie warianty algorytmów rodziny Keccak, zapewniono odpowiednie środki powiadamiania o błędach (np. w przypadku problemów z alokacją pamięci), opracowano skrypty do automatyzacji przenoszenia nowych wersji HACL* do repozytorium Python.
Źródło: opennet.ru
