Objavljeno je uspješno završavanje inicijative za zamjenu kriptografskih algoritama u Pythonu, koji se nude u modulima hashlib i hmac, s varijantama koje imaju matematički dokaz sigurnosti, pripremljenim projektom 'HACL*'. Rad na prijelazu na funkcije s matematičkim dokazom sigurnosti započeo je 2022. godine, nakon otkrivanja preljeva bafera u implementaciji algoritma SHA3 koji se koristi u Pythonovom modulu hashlib.
U glavni repozitorij projekta CPython prihvaćen je kod s novim implementacijama kriptografskih hash-funkcija i HMAC algoritama (mehanizam provjere autentičnosti poruka). Sve hash-funkcije i HMAC-ovi koji se po defaultu nude u Pythonu zamijenjeni su ovjerenim varijantama. Između ostalog, dodana je implementacija HMAC-BLAKE2 koja koristi SIMD instrukcije AVX2 za ubrzanje izračuna. Predviđa se da će ovjereni kod ući u jesensko izdanje Pythona 3.14.
Nove implementacije kriptografskih funkcija prebačene su iz biblioteke HACL*, koju razvijaju istraživači iz francuskog nacionalnog instituta za istraživanje u računalstvu i automatizaciji (INRIA), odjeljenja Microsoft Research i Sveučilišta Carnegie Mellon. Biblioteka HACL* podržava tipične kriptografske funkcije dovoljne za rad sa TLS 1.3 i punu podršku za NaCl API (biblioteku za umrežavanje i kriptografiju), kao što su Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC i HKDF. Po performansama, biblioteka HACL* je bliska OpenSSL-u, ali za razliku od posljednjeg pruža dodatne garancije sigurnosti i pouzdanosti.
Kod HACL* napisan je u podskupu funkcionalnog jezika F*, koji nudi sustav zavisnih tipova i preciziranja koji omogućuju postavljanje točnih specifikacija (matematički model) i jamče odsustvo grešaka u implementaciji pomoću SMT formula i pomoćnih alata za dokazivanje. Referentni kod u F* transpilira se u kod na jeziku C putem kompajlera KaRaMeL i dostupan je za integraciju s drugim projektima.
Verifikacija podrazumijeva definiranje detaljnih specifikacija koje opisuju sve varijante ponašanja programa, kao i formiranje matematičkog dokaza da napisani kod u potpunosti odgovara pripremljenim specifikacijama. Verifikacija jamči da će se program izvršavati samo onako kako su programeri zamislili i da ne sadrži određene klase grešaka, kao što su prekomjerna pohrana, dereferenciranje pokazivača, pristup već oslobođenim dijelovima memorije ili dvostruko oslobađanje blokova memorije. Tijekom kompilacije osigurava se rigorozna provjera tipova i vrijednosti — jedan komponent nikada neće predati drugom komponenti parametre koji ne odgovaraju specifikaciji te neće imati pristup unutarnjim stanjima drugih komponenti.
Proces prelaska na verificirani kod trajao je dvije i pol godine i zahtijevao reviziju HACL* biblioteke, čija je funkcionalnost proširena mogućnostima potrebnim za transparentnu zamjenu postojeće funkcionalnosti hashlib. Na primjer, u HACL* je dodana podrška za rad u stream modu HMAC, pruženi su dodatni načini rada algoritama Blake2, implementiran je novi API za SHA3 koji pokriva sve varijante algoritama porodice Keccak, osigurana su potrebna sredstva za obavještavanje o greškama (na primjer, u slučaju problema s alokacijom memorije), razvijeni su skripti za automatizaciju premještanja novih verzija HACL* u Python repozitorij.
Izvor: opennet.ru
