A fost anunțat finalizarea cu succes a inițiativei de înlocuire în Python a implementărilor algoritmilor criptografici oferite în modulele hashlib și hmac, cu variante dovedite matematic a fi fiabile, pregătite de proiectul „HACL*”. Lucrările pentru tranziția la funcțiile cu dovezi matematice de fiabilitate au început în 2022 și au fost inițiate după descoperirea unei vulnerabilități de tip buffer overflow în implementarea algoritmului SHA3, utilizată în modulul Python hashlib.
În depozitul principal al proiectului CPython a fost acceptat codul cu noile implementări ale funcțiilor de hash criptografic și algoritmilor HMAC (mecanism de autentificare a mesajelor). Toate funcțiile de hash și HMAC oferite implicit în Python au fost înlocuite cu variante verificate. Printre altele, a fost adăugată implementarea HMAC-BLAKE2, care utilizează instrucțiuni SIMD AVX2 pentru a accelera calculul. Se estimează că codul verificat va face parte din lansarea de toamnă Python 3.14.
Noile implementări ale funcțiilor criptografice au fost transferate din biblioteca HACL*, dezvoltată de cercetători de la institutul național de cercetare în informatică și automatică din Franța (INRIA), o divizie a Microsoft Research și Universitatea Carnegie Mellon. Biblioteca HACL* susține funcții criptografice standard, suficiente pentru funcționarea TLS 1.3 și suport complet pentru API-ul NaCl (Networking and Cryptography library), cum ar fi Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC și HKDF. În ceea ce privește performanța, biblioteca HACL* este comparabilă cu OpenSSL, dar spre deosebire de aceasta, oferă garanții suplimentare de fiabilitate și securitate.
Codul HACL* este scris într-un subset al limbajului funcțional F*, care oferă un sistem de tipuri dependente și tipuri adnotate, permițând formularea de specificații precise (model matematic) și garantarea absenței erorilor în implementare prin formule SMT și instrumente auxiliare de demonstrație. Codul de referință în F* este transformat în cod C prin intermediul compilatorului KaRaMeL și este disponibil pentru integrare cu alte proiecte.
Verificarea implică stabilirea specificațiilor detaliate care descriu toate variantele de comportament ale programului și formarea unei dovezi matematice că codul scris corespunde pe deplin specificațiilor pregătite. Verificarea garantează că programul va funcționa doar așa cum au intentat dezvoltatorii și că nu sunt prezente anumite clase de erori, cum ar fi depășirea bufferului, dereferințierea pointerilor, accesarea zonelor de memorie deja eliberate sau eliberarea dublă a blocurilor de memorie. În timpul compilării, se asigură o verificare strictă a tipurilor și valorilor — un component nu va transmite niciodată altui component parametrii care nu corespund specificației și nu va avea acces la stările interne ale altor componente.
Procesul de tranziție la codul verificat a durat două ani și jumătate și a necesitat actualizarea bibliotecii HACL*, a cărei funcționalitate a fost extinsă cu caracteristici necesare pentru înlocuirea transparentă a funcționalității existente hashlib. De exemplu, în HACL* a fost adăugată suport pentru modul de operare pe flux HMAC, au fost furnizate moduri suplimentare de operare pentru algoritmii Blake2, a fost implementat un nou API pentru SHA3, acoperind toate variantele algoritmilor din familia Keccak, și au fost asigurate instrumentele necesare pentru notificarea erorilor (de exemplu, în caz de probleme cu alocarea memoriei), au fost dezvoltate scripturi pentru automatizarea transferului noilor versiuni HACL* în repository-ul Python.
Sursa: opennet.ro
