È stata annunciata la conclusione con successo dell'iniziativa per sostituire le implementazioni degli algoritmi crittografici proposti nei moduli hashlib e hmac in Python con opzioni con prova matematica di affidabilità, predisposte dal progetto "HACL*". Il lavoro per passare a funzioni con prova matematica di affidabilità è iniziato nel 2022 ed è stato avviato dopo la scoperta di un overflow del buffer nell'implementazione dell'algoritmo SHA3 utilizzata nel modulo hashlib di Python.
Nel repository principale del progetto CPython è stato accettato il codice con le nuove implementazioni delle funzioni hash crittografiche e degli algoritmi HMAC (meccanismo per la verifica dell'integrità dei messaggi). Tutte le funzioni hash e HMAC predefinite in Python sono state sostituite con varianti verificate. Tra le altre cose, è stata aggiunta l'implementazione di HMAC-BLAKE2, che utilizza istruzioni SIMD AVX2 per accelerare i calcoli. Si prevede che il codice verificato sarà parte del rilascio autunnale di Python 3.14.
Le nuove implementazioni delle funzioni crittografiche sono state trasferite dalla libreria HACL*, sviluppata dai ricercatori dell'Istituto Nazionale di Ricerca in Informatica e Automatica (INRIA) francese, da Microsoft Research e dall'Università Carnegie Mellon. La libreria HACL* supporta funzioni crittografiche standard sufficienti per TLS 1.3 e il supporto completo dell'API NaCl (Networking and Cryptography library), come Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC e HKDF. Per prestazioni, la libreria HACL* è paragonabile a OpenSSL, ma a differenza di quest'ultima fornisce ulteriori garanzie di affidabilità e sicurezza.
Il codice HACL* è scritto in un sottoinsieme del linguaggio funzionale F*, che offre un sistema di tipi dipendenti e annotazioni in grado di definire specifiche precise (modelli matematici) e garantire l'assenza di errori nell'implementazione attraverso formule SMT e strumenti di prova ausiliari. Il codice di riferimento in F* viene tradotto in codice C tramite il compilatore KaRaMeL ed è disponibile per l'integrazione con altri progetti.
La verifica implica la definizione di specifiche dettagliate che descrivono tutti i possibili comportamenti del programma e la formulazione di una prova matematica che attesti che il codice scritto corrisponde completamente alle specifiche preparate. La verifica garantisce che il programma verrà eseguito solo come previsto dagli sviluppatori e che non contenga determinate classi di errori, come overflow del buffer, dereferenziazione di puntatori, accesso a zone di memoria già liberate o doppia liberazione di blocchi di memoria. Durante il processo di compilazione viene effettuato un rigoroso controllo dei tipi e dei valori — un componente non fornirà mai a un altro componente parametri non conformi alle specifiche e non avrà accesso agli stati interni di altri componenti.
Il processo di transizione al codice verificato ha richiesto due anni e mezzo e ha richiesto miglioramenti alla libreria HACL*, la cui funzionalità è stata ampliata con le caratteristiche necessarie per una sostituzione trasparente delle funzionalità esistenti in hashlib. Ad esempio, in HACL* è stato aggiunto il supporto per la modalità di funzionamento in streaming di HMAC, forniti ulteriori modi di operare per gli algoritmi Blake2, implementato una nuova API per SHA3 che copre tutte le varianti degli algoritmi della famiglia Keccak, garantite le necessarie segnalazioni di errore (ad esempio, in caso di problemi di allocazione della memoria), e sviluppati script per automatizzare il trasferimento nel repository Python delle nuove versioni di HACL*.
Fonte: opennet.ru
