{"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\/news\/v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti","title":{"rendered":"In Python sono state implementate funzioni crittografiche con prove matematiche di affidabilit\u00e0","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
\u00c8 stata annunciata la conclusione con successo dell'iniziativa per la sostituzione delle implementazioni degli algoritmi crittografici offerti nei moduli hashlib e hmac in Python con opzioni con prove matematiche di affidabilit\u00e0, preparate dal progetto \u00abHACL*\u00bb. I lavori per il passaggio a funzioni con prove matematiche di affidabilit\u00e0 sono iniziati nel 2022, dopo la scoperta di un buffer overflow nell'implementazione dell'algoritmo SHA3 utilizzato nel modulo hashlib di Python. <\/p>\n
Nel repository principale del progetto CPython \u00e8 stato accolto il codice con nuove implementazioni delle funzioni hash crittografiche e degli algoritmi HMAC (meccanismo di verifica dell'autenticit\u00e0 dei messaggi). Tutte le funzioni hash e HMAC fornite di default in Python sono state sostituite con varianti verificate. Tra l'altro, \u00e8 stata aggiunta l'implementazione HMAC-BLAKE2, che utilizza le istruzioni SIMD AVX2 per accelerare i calcoli. Si prevede che il codice verificato entrer\u00e0 a far 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'istituto nazionale francese per la ricerca in informatica e automazione (INRIA), dal dipartimento di Microsoft Research e dall'universit\u00e0 Carnegie Mellon. La libreria HACL* supporta le funzioni crittografiche standard necessarie 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. In termini di prestazioni, la libreria HACL* \u00e8 simile a OpenSSL, ma a differenza di quest'ultima offre ulteriori garanzie di affidabilit\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 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 \u00e8 disponibile per l'integrazione con altri progetti. <\/p>\n
La verifica implica la definizione di specifiche dettagliate che descrivono tutti i comportamenti possibili del programma e la formulazione di una prova matematica che dimostri che il codice scritto corrisponde completamente alle specifiche preparate. La verifica garantisce che il programma venga eseguito solo come previsto dagli sviluppatori e che non contenga determinate classi di errori, come buffer overflow, dereferenziazione di puntatori, accesso a aree di memoria gi\u00e0 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 trasferir\u00e0 mai a un altro componente parametri non conformi alle specifiche e non acceder\u00e0 agli stati interni di altri componenti. <\/p>\n
Il processo di transizione al codice verificato ha richiesto due anni e mezzo e ha richiesto integrazioni alla libreria HACL*, la cui funzionalit\u00e0 \u00e8 stata ampliata con capacit\u00e0 necessarie per una sostituzione trasparente delle funzionalit\u00e0 esistenti di hashlib. Ad esempio, in HACL* \u00e8 stato aggiunto il supporto per il funzionamento in modalit\u00e0 streaming di HMAC, sono state fornite modalit\u00e0 di funzionamento aggiuntive per gli algoritmi Blake2, \u00e8 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*. \n Fonte: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"