{"id":123602,"date":"2025-04-19T15:05:06","date_gmt":"2025-04-19T13:05:06","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti"},"modified":"2025-04-19T15:05:06","modified_gmt":"2025-04-19T13:05:06","slug":"v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti","status":"publish","type":"post","link":"https:\/\/prohoster.info\/it\/blog\/novosti-interneta\/v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti","title":{"rendered":"Python utilizza funzioni crittografiche con prova matematica di affidabilit\u00e0","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
\u00c8 stato annunciato il completamento con successo dell'iniziativa per la sostituzione delle implementazioni degli algoritmi crittografici disponibili nei moduli hashlib e hmac in Python, con varianti con prova matematica di solidit\u00e0, sviluppate dal progetto «HACL*». Il lavoro per la transizione a funzioni con prova matematica di solidit\u00e0 \u00e8 iniziato nel 2022 ed \u00e8 stato avviato dopo l'individuazione di un overflow nel buffer nell'implementazione dell'algoritmo SHA3 utilizzato nel modulo hashlib di Python. <\/p>\n
Nel repository principale del progetto CPython \u00e8 stato accettato il codice con le nuove implementazioni delle funzioni hash crittografiche e degli algoritmi HMAC (meccanismo per la verifica dell'integrit\u00e0 dei messaggi). Tutte le funzioni hash e HMAC predefinite in Python sono state sostituite con varianti verificate. Tra le altre cose, \u00e8 stata aggiunta l'implementazione di HMAC-BLAKE2, che utilizza istruzioni SIMD AVX2 per accelerare i calcoli. Si prevede che il codice verificato sar\u00e0 parte del rilascio autunnale di Python 3.14. <\/p>\n
Le nuove implementazioni delle funzioni crittografiche sono state trasferite dalla libreria HACL*, sviluppata dai ricercatori dell'Institut National de Recherche en Informatique et en Automatique (INRIA), di Microsoft Research e della Carnegie Mellon University. La libreria HACL* supporta funzioni crittografiche standard sufficienti per il funzionamento di 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. In termini di prestazioni, la libreria HACL* \u00e8 comparabile a OpenSSL, ma a differenza di quest'ultima fornisce garanzie aggiuntive di solidit\u00e0 e sicurezza. <\/p>\n
Il codice HACL* \u00e8 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 \u00e8 disponibile per l'integrazione con altri progetti. <\/p>\n
La verifica implica la definizione di specifiche dettagliate che descrivono tutti i possibili comportamenti del programma e la formazione di una prova matematica che dimostri che il codice scritto corrisponde completamente alle specifiche elaborate. La verifica garantisce che il programma venga eseguito solo come previsto dagli sviluppatori e che non ci siano determinate classi di errori, come overflow del buffer, dereferenziazione di puntatori, accesso ad aree di memoria gi\u00e0 liberate o doppia liberazione di blocchi di memoria. Durante la compilazione viene garantita una rigorosa verifica di tipi e valori: un componente non passer\u00e0 mai parametri non conformi alle specifiche a un altro componente e non avr\u00e0 accesso agli stati interni di altri componenti. <\/p>\n
Il processo di transizione al codice verificato ha richiesto due anni e mezzo e ha richiesto miglioramenti alla libreria HACL*, la cui funzionalit\u00e0 \u00e8 stata ampliata con le caratteristiche necessarie per una sostituzione trasparente delle funzionalit\u00e0 esistenti in hashlib. Ad esempio, in HACL* \u00e8 stato aggiunto il supporto per la modalit\u00e0 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*. \n Fonte: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"