È stata annunciata la conclusione con successo dell'iniziativa per sostituire in Python le implementazioni degli algoritmi crittografici proposti nei moduli hashlib e hmac con varianti con prove matematiche di affidabilità, preparate dal progetto "HACL*". Il lavoro per passare a funzioni con prove matematiche di affidabilità è iniziato nel 2022 ed è stato avviato dopo l'identificazione di un overflow di buffer nell'implementazione dell'algoritmo SHA3, utilizzato nel modulo hashlib di Python.
Nel repository principale del progetto CPython è stato accolto il codice con nuove implementazioni delle funzioni hash crittografiche e degli algoritmi HMAC (meccanismo di verifica dell'autenticità dei messaggi). Tutte le funzioni hash e HMAC fornite di default in Python sono state sostituite con varianti verificate. Tra l'altro, è stata aggiunta l'implementazione HMAC-BLAKE2, che utilizza le istruzioni SIMD AVX2 per accelerare i calcoli. Si prevede che il codice verificato entrerà a far parte del rilascio autunnale di Python 3.14.
Le nuove implementazioni delle funzioni crittografiche sono state trasferite dalla libreria HACL*, sviluppata da ricercatori dell'INRIA, dell'unità Microsoft Research e dell'Università Carnegie Mellon. La libreria HACL* supporta funzioni crittografiche standard, sufficienti per il funzionamento di TLS 1.3 e il pieno supporto 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* è vicina a OpenSSL, ma a differenza di quest'ultima offre garanzie aggiuntive di affidabilità e sicurezza.
Il codice HACL* è scritto in un sottoinsieme del linguaggio funzionale F*, che offre un sistema di tipi dipendenti e specifiche che permettono di definire specifiche esatte (modello matematico) e garantire l'assenza di errori nell'implementazione utilizzando formule SMT e strumenti ausiliari di dimostrazione. Il codice di riferimento in F* viene tradotto in codice in linguaggio C utilizzando 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 creazione di una dimostrazione matematica che il codice scritto soddisfi completamente le specifiche preparate. La verifica garantisce che il programma verrà eseguito solo come progettato dagli sviluppatori e non conterrà determinate classi di errori, come il buffer overflow, la dereferenziazione di puntatori, l'accesso a aree di memoria già liberate o il doppio rilascio di blocchi di memoria. In fase di compilazione, viene eseguito un rigoroso controllo dei tipi e dei valori: un componente non passerà mai a un altro componente parametri che non corrispondono alle specifiche e non accederà agli stati interni di altri componenti.
Il processo di transizione al codice verificato ha richiesto due anni e mezzo e ha richiesto integrazioni alla libreria HACL*, la cui funzionalità è stata ampliata con capacità necessarie per una sostituzione trasparente delle funzionalità esistenti di hashlib. Ad esempio, in HACL* è stato aggiunto il supporto per il funzionamento in modalità streaming di HMAC, sono state fornite modalità di funzionamento aggiuntive per gli algoritmi Blake2, è stata implementata una nuova API per SHA3, che copre tutte le varianti degli algoritmi della famiglia Keccak, sono stati forniti gli strumenti necessari per la notifica degli errori (ad esempio, in caso di problemi di allocazione della memoria), sono stati sviluppati script per automatizzare il trasferimento nel repository Python delle nuove versioni di HACL*.
Fonte: opennet.ru
