ĂshtĂ« njoftuar pĂ«r pĂ«rfundimin me sukses tĂ« iniciativĂ«s pĂ«r zĂ«vendĂ«simin nĂ« Python tĂ« implementimeve tĂ« algoritmeve kriptografikĂ«, tĂ« ofruara nĂ« modulĂ«t hashlib dhe hmac, me variante me provĂ« matematike tĂ« besueshmĂ«risĂ«, pĂ«rgatitur nga projekti "HACL*". Puna pĂ«r kalimin nĂ« funksione me provĂ« matematike tĂ« besueshmĂ«risĂ« ka filluar qĂ« nga viti 2022 dhe Ă«shtĂ« iniciuar pas zbulesĂ«s sĂ« mbushjes sĂ« tamponit nĂ« implementimin e algoritmit SHA3, i pĂ«rdorur nĂ« modulĂ«n Python hashlib.
Kodi me realizimet e reja të funksioneve hash kriptografike dhe algoritmeve HMAC (mekanizmi i verifikimit të autenticitetit të mesazheve) është pranuar në repositorin kryesor të projektit CPython. Të gjitha funksionet hash dhe HMAC që ofrohen si par default në Python janë zëvendësuar me variante të verifikuara. Ndër të tjera, është shtuar implementimi HMAC-BLAKE2, i cili përdor instrukcionet SIMD AVX2 për të përshpejtuar llogaritjet. Pritet që kodi i verifikuar të përfshihet në lansimin e vjeshtës Python 3.14.
Implementimet e reja të funksioneve kriptografike janë transferuar nga biblioteka HACL*, e zhvilluar nga kërkuesit e Institutit Kombëtar të Kërkimeve të Informatikës dhe Automatizimit (INRIA) të Francës, një degë e Microsoft Research dhe Universitetit Carnegie Mellon. Biblioteka HACL* mbështet funksionet standarde kriptografike të nevojshme për funksionimin e TLS 1.3 dhe mbështetje të plotë për API-në NaCl (Libraria e Networking dhe Kriptografisë), si Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC dhe HKDF. Sipas performancës, biblioteka HACL* është afërsisht në nivelin e OpenSSL, por ndryshe nga kjo e fundit, ofron garanci të shtesë për besueshmëri dhe siguri.
Kodi HACL* është shkruar në një nëngrup të gjuhës funksionale F*, e cila ofron një sistem të tipeve të varura dhe sqarimeve që lejojnë përcaktimin e specifikimeve të sakta (modeli matematikor) dhe garantojnë mungesën e gabimeve në implementim përmes formulave SMT dhe mjeteve ndihmëse të provës. Kodi referues në F* transpektohet në kod në gjuhën C përmes kompilatorit KaRaMeL dhe është i disponueshëm për integrim me projekte të tjera.
Verifikimi përfshin përcaktimin e specifikimeve të detajuara që përshkruajnë të gjitha variacione e sjelljes së programit, dhe formimin e një dëshmie matematikore që kodi i shkruar plotësisht i përkon specifikacioneve të përgatitura. Verifikimi jep garanci se programi do të ekzekutohet vetëm siç e kanë menduar zhvilluesit dhe se nuk ka klasa të caktuara gabimesh, të tilla si mbipopullimi i tamponëve, dereferencimi i treguesve, aksesimi i hapësirave të kujtesës që janë çliruar tashmë ose çlirimi i dyfishtë i blloqeve të kujtesës. Gjatë kompilimit, sigurohet një kontroll i fortë i llojeve dhe vlerave - një komponent kurrë nuk do t'i kalojë një komponenti tjetër parametra që nuk i përprohet specifikacioneve, dhe nuk do të ketë akses në gjendjet e brendshme të komponentëve të tjerë.
Procesi i kalimit në kod të verifikuar mori dy vite e gjysmë dhe kërkoi përmirësimin e bibliotekës HACL*, funksionaliteti i së cilës u zgjerua me mundësitë e nevojshme për zëvendësimin e qartë të funksionalitetit ekzistues hashlib. Për shembull, në HACL* u shtua mbështetje për funksionin e punës HMAC në mënyrë të rrjedhshme, u ofruan mënyra të tjera të punës për algoritmet Blake2, u realizua një API i ri për SHA3, duke përfshirë të gjitha variantet e algoritmeve të familjes Keccak, u siguruan mjetet e nevojshme për njoftimin për gabime (për shembull, në rast të problemeve me ndarjen e kujtesës), dhe u zhvilluan skenarët për automatizimin e transferimit të versioneve të reja HACL* në depozitën Python.
Burimi: opennet.ru
