Det er blevet annonceret, at initiativet til at erstatte implementeringerne af kryptografiske algoritmer i Python-modulerne hashlib og hmac med pålidelige matematiske beviser for sikkerhed, udviklet af projektet „HACL*”, er lykkedes. Arbejdet med at overgå til funktioner med matematiske beviser for sikkerhed er blevet udført siden 2022 og blev iværksat efter opdagelsen af en buffer-overløb i implementeringen af algoritmen SHA3, der anvendes i Python-modulet hashlib.
Ny kode med implementeringer af kryptografiske hash-funktioner og HMAC-algoritmer (mekanisme til at verificere meddelelsers autenticitet) er blevet accepteret i hovedrepositoryet for CPython-projektet. Alle de hash-funktioner og HMAC'er, der leveres som standard i Python, er blevet erstattet med verificerede varianter. Blandt andet er der tilføjet en implementering af HMAC-BLAKE2, der bruger SIMD-instruktioner AVX2 for at øge beregningernes hastighed. Den forventes at indgå i efterårsudgivet Python 3.14.
De nye implementeringer af kryptografiske funktioner er overført fra HACL*-biblioteket, som udvikles af forskere fra det franske nationale institut for forskninger inden for computerteknologi og automatisering (INRIA), en afdeling af Microsoft Research og Carnegie Mellon University. HACL*-biblioteket understøtter standard kryptografiske funktioner, der er tilstrækkelige til at arbejde med TLS 1.3 og fuld understøttelse af NaCl API (Networking and Cryptography library), såsom Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC og HKDF. HACL*-biblioteket er næsten ligesom OpenSSL i ydeevne, men adskiller sig ved at tilbyde yderligere garantier for pålidelighed og sikkerhed.
HACL*-koden er skrevet i et undergruppe af funktionelt sprog F*, som tilbyder et system af afhængige typer og præciseringer, hvilket gør det muligt at angive præcise specifikationer (matematisk model) og garantere, at der ikke er fejl i implementeringen gennem SMT-formler og hjælpeværktøjer til bevis. Referencekoden i F* kompilretter til C-kode ved hjælp af KaRaMeL-kompilatoren og er tilgængelig for integration med andre projekter.
Verifikation indebærer at definere detaljerede specifikationer, der beskriver alle mulige opførsler af programmet, og at danne et matematisk bevis på, at den skrevne kode fuldt ud svarer til de udarbejdede specifikationer. Verifikation giver garanti for, at programmet kun vil fungere som udviklerne har tiltænkt, og at det er fri for bestemte klasser af fejl, såsom buffer overflow, dereferering af pegere, adgang til allerede frigivne hukommelsesområder eller dobbeltfrigivelse af hukommelsesenheder. Under kompilering sikres en streng kontrol af typer og værdier – en komponent vil aldrig overføre parametre til en anden komponent, der ikke stemmer overens med specifikationen, og vil ikke få adgang til interne tilstande for andre komponenter.
Overgangen til den verificerede kode tog to og en halv år og krævede opdatering af HACL*-biblioteket, hvis funktionalitet blev udvidet med de nødvendige funktioner til en gennemsigtig erstatning af den eksisterende funktionalitet i hashlib. For eksempel blev der tilføjet support for streaming-mode af HMAC i HACL*, yderligere driftsformer for Blake2-algoritmer blev præsenteret, en ny API til SHA3 blev implementeret, som dækker alle varianter af Keccak-familien, nødvendige fejlmeddelelsesværktøjer blev sikret (f.eks. ved hukommelsesallokeringsproblemer), og scripts til automatisering af overførsel af nye versioner af HACL* til Python-repositoriet blev udviklet.
Kilde: opennet.ru
