Kryptografiska funktioner med matematiskt bevis för säkerhet används i Python

Det har meddelats att initiativet för att ersätta implementationerna av kryptografiska algoritmer som erbjuds i modulerna hashlib och hmac i Python har avslutats framgångsrikt. Arbetet med att övergå till funktioner med matematiska säkerhetsbevis har pågått sedan 2022 och initierades efter att en buffertöverskridning upptäcktes i implementationen av algoritmen SHA3, som används i Python-modulen hashlib.

Kod med nya implementationer av kryptografiska hash-funktioner och HMAC-algoritmer (mekanism för meddelandebekräftelse) har antagits i huvudarkivet för projektet CPython. Alla standardhash-funktioner och HMAC i Python har ersatts med verifierade alternativ. Bland annat har en implementering av HMAC-BLAKE2 lagts till, som använder SIMD-instruktioner AVX2 för att påskynda beräkningarna. Det förväntas att den verifierade koden kommer att inkluderas i höstlanseringen av Python 3.14.

De nya implementationerna av kryptografiska funktioner har överförts från biblioteket HACL*, som utvecklas av forskare från det franska statliga forskningsinstitutet för datavetenskap och automatiken (INRIA), en del av Microsoft Research och Carnegie Mellon University. Biblioteket HACL* stöder typiska kryptografiska funktioner, tillräckliga för att arbeta med TLS 1.3 och fullständig stöd för API NaCl (Networking and Cryptography library), såsom Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC och HKDF. När det gäller prestanda är biblioteket HACL* nära OpenSSL, men i motsats till det senare ger det ytterligare garantier för tillförlitlighet och säkerhet.

Koden för HACL* är skriven i en delmängd av det funktionella språket F*, som erbjuder ett system med beroende typer och specificeringar som gör det möjligt att ställa exakta specifikationer (matematisk modell) och garantera frånvaron av fel i implementationen med hjälp av SMT-formler och stödverktyg för bevisande. Referenskoden på F* översätts till C-kod med hjälp av kompileraren KaRaMeL och är tillgänglig för integration med andra projekt.

Verifiering innebär att fastställa detaljerade specifikationer som beskriver alla möjliga beteenden hos programmet, samt att skapa ett matematiskt bevis för att koden som skrivits helt överensstämmer med de framtagna specifikationerna. Verifiering garanterar att programmet endast kommer att köras som utvecklarna avsett och att det saknar vissa klasser av fel, såsom buffertöverflöd, pekardereferering, åtkomst till redan frigjorda minnesområden eller dubbel frigöring av minnesblock. Under kompileringen genomförs en strikt typ- och värdekontroll — en komponent kommer aldrig att överföra parametrar som inte överensstämmer med specifikationen till en annan komponent eller få tillgång till interna tillstånd av andra komponenter.

Övergången till verifierad kod tog två och ett halvt år och krävde revidering av biblioteket HACL*, vars funktionalitet utvidgades med de nödvändiga möjligheterna för en transparent ersättning av den befintliga funktionaliteten i hashlib. Till exempel lades stöd för HMAC-strömmanvändning till i HACL*, ytterligare driftslägen för Blake2-algoritmer infördes, en ny API för SHA3 implementerades som omfattade alla varianter av Keccak-familjen, nödvändiga felmeddelandefunktioner tillhandahölls (till exempel vid problem med minnesallokering), och skript utvecklades för att automatisera överföringen av nya versioner av HACL* till Python-repot.

Källa: opennet.ru