On kinnitatud, et Pythonis on edukalt lõpetatud algatus asendada krüptograafiliste algoritmide rakendused, mis on saadaval hashlib ja hmac moodulites, matemaatilise usaldusväärsuse tõenditega versioonidega, mille on ette valmistanud projekt "HACL*". Üleminek matemaatilise usaldusväärsuse tõenditega funktsioonidele algas 2022. aastal ja algatati pärast SHA3 algoritmi rakenduses, mida kasutatakse Python moodulis hashlib, tuvastatud mälupuhvri ületäitumist.
Põhiprojekti SPython hoidlast on vastu võetud kood uute krüptograafiliste räsifunktsioonide ja HMAC (sõnumite autentimise mehhanismi) rakendustega. Kõik vaikimisi Pythonis saadaval olevad räsifunktsioonid ja HMAC on asendatud kinnitatud variantidega. Muuhulgas on lisatud HMAC-BLAKE2 rakendus, mis kasutab AVX2 SIMDi instruktsioone arvutuste kiirendamiseks. Eeldatakse, et kinnitatud kood kuulub Python 3.14 sügisel väljaandmise koosseisu.
Uued krüptograafiliste funktsioonide teostused on üle kantud HACL* raamatukogust, mida arendavad Prantsuse riikliku infotehnoloogia ja automatiseerimise teadusinstituudi (INRIA), Microsoft Research’i ja Carnegie Mellon’i ülikooli teadlased. HACL* raamatukogu toetab standardseid krüptograafilisi funktsioone, mida piisab TLS 1.3 tööks ja NaCl (Networking and Cryptography library) API täielikuks toetamiseks, nagu Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC ja HKDF. HACL* raamatukogu jõudlus on lähedane OpenSSL-le, kuid erinevalt sellest pakub see täiendavaid usaldusväärsuse ja turvalisuse garantii.
HACL* kood on kirjutatud F* funktsionaalse keele alamhulgas, mis pakub sõltuvate tüüpide ja täpsete spetsifikatsioonide (matemaatilise mudeli) määratlemiseks vajalikke tuge, tagades samas, et rakenduses ei esine vigu SMT-valemite ja abistavate tõenditöötlusvahendite abil. F* referentkood tõlgitakse C keele koodiks KaRaMeL kompilaatori abil ning on saadaval integratsiooniks teiste projektidega.
Verifitseerimise protsess hõlmab detailsete spetsifikatsioonide määratlemist, mis kirjeldavad programmi käitumise kõiki variante, ja matemaatilise tõenduse loomist, et kirjutatud kood vastab täielikult koostatud spetsifikatsioonidele. Verifitseerimine tagab, et programm töötab ainult nii, nagu arendajad on ette näinud, ning et selles ei esine teatud tüüpi vigu, nagu mälupuhvri ülevool, näidikute dereferentsimine, juba vabastatud mällu pääsemine või mäluplokkide kahekordne vabastamine. Kompileerimise käigus tagatakse rangete tüüpide ja väärtuste kontroll — üks komponent ei edasta kunagi teisele komponendile parameetreid, mis ei vasta spetsifikatsioonile, ega pääse teiste komponentide siseseisunditesse.
Üleminekuprotsess kinnitatud koodi juurde kestis kaks ja pool aastat ning nõudis HACL* teegi täiustamist, mille funktsionaalsust suurendati olemasoleva hashlib funktsionaalsuse sujuvaks asendamiseks vajalike võimalustega. Näiteks lisati HACL* s HMAC-i voolurežiimi tugi, lisati algoritmide Blake2 täiendavad töörežiimid, rakendati uus API SHA3 jaoks, mis katab kogu Keccaqi perekonna algoritmide valiku, ning tagati vajalikud veateated (näiteks mälu jagamise probleemide korral), samuti töötati välja skriptid HACL* uute versioonide Pythonisse ületoomiseks automatiseerimiseks.
Allikas: opennet.ru
