Studiuesit nga Instituti Shtetëror për Kërkime në Informatikë dhe Automatizim (INRIA), Microsoft Research dhe Carnegie Mellon University prezantuan edicioni i parë në provë i biblioteka kripto EverCrypt zhvilluar brenda kornizës së projektit Everest dhe duke përdorur metoda matematikore të verifikimit zyrtar të besueshmërisë.
Për aftësitë dhe performancën e tij, EverCrypt është shumë afër bibliotekave ekzistuese të kriptove (OpenSSL) por që, ndryshe nga ata, ofron garanci shtesë të besueshmërisë dhe sigurisë.
P.sh. procesi i verifikimit përfundon në përcaktimin e specifikimeve të hollësishme që përshkruajnë të gjitha sjelljet e programit dhe prova matematikore se kodi i shkruar plotëson specifikimet e përgatitura.
Ndryshe nga metodat e kontrollit të cilësisë të bazuara në prova, verifikimi ofron garanci të besueshme që programi do të ekzekutohet vetëm siç kanë menduar zhvilluesit dhe nuk ka klasa specifike të gabimeve.
Për shembull, pajtueshmëria me specifikimet siguron punë të sigurt me kujtesën dhe mungesën e gabimeve që çojnë në tejmbushjen e bufferit, te treguesit e referimit, për të hyrë në zonat e kujtesës tashmë të çliruara, ose për të çliruar dyfishin e blloqeve të kujtesës.
Çfarë është EverCrypt?
EverCrypt ofron kontroll të fortë dhe të vlerës së llojit- Një komponent nuk do të kalojë kurrë në parametrat e komponentit tjetër jo-në përputhje dhe nuk do të ketë qasje në gjendjet e brendshme të komponentëve të tjerë.
Sjellja e hyrjes / daljes përputhet plotësisht me veprimet e thjeshta të funksionit të matematikës, të cilat përcaktohen në standardet kriptografike.
Për të mbrojtur nga sulmet në kanalet e palëve të treta, sjellja gjatë llogaritjeve (për shembull, kohëzgjatja e ekzekutimit ose prania e akseseve në memorje të caktuara) nuk varet nga të dhënat sekrete që përpunohen.
Kodi i projektit është shkruar në gjuhën funksionale F * (Ylli F) , i cili siguron një sistem të llojeve dhe rafinimeve të varura, që lejojnë krijimin e specifikimeve të sakta (modelin matematikor) për programet dhe garantimin e korrektësisë dhe mungesës së gabimeve në zbatim me anë të formulave SMT dhe mjeteve ndihmëse të provës.
Kodi në F * shpërndahet nën licencën Apache 2.0, dhe modulet përfundimtare në C dhe montuesi nën licencën MIT.
Bazuar në kodin referues F *, gjenerohet assembler, C, OCaml, JavaScript dhe kodin e montimit në internet.
Disa pjesë të kodit përgatitur nga projekti janë përdorur tashmë në Firefox, kernelin e Windows , blockchain e Tezos dhe VPN Wireguard.
Komponentët EverCrypt
Në esencë, EverCrypt kombinon dy projekte të mëparshme të ndryshme nga HACL * dhe Vale, duke siguruar një API të unifikuar bazuar në to dhe duke i bërë ato të përshtatshme për përdorim në projekte reale.
HACL * është shkruar në Low* dhe qëllimi i tij është të sigurojë primitivë kriptografikë për përdorim në programet C që ata përdorin libsodium dhe API-të e stilit NaCL.
El Proyecto Vale zhvilloi një gjuhë specifike domain për të krijuar verifikime në asembler.
Kombinohen rreth 110 mijë rreshta të kodit HACL * në gjuhë të ulët * dhe 25 mijë rreshta të kodit për Vale dhe ato rishkruhen në rreth 70 mijë rreshta kodi në gjuhën universale F *, e cila gjithashtu është duke u zhvilluar si pjesë e projektit Everest.
Versioni i parë i bibliotekës EverCrypt përmban zbatime të verifikuara të algoritmeve kriptografikë të mëposhtëm propozuar në C ose versionet e mbledhësit (kur përdorni.
Nga këto, më poshtë bien në sy faqja e projektit:
- Algoritmet Hash: të gjitha variantet e SHA2, SHA3, SHA1 dhe MD5
- Kodet e vërtetimit: HMAC mbi SHA1, SHA2-256, SHA2-384 dhe SHA2-512 për vërtetimin e burimit të të dhënave
- Algoritmi i Gjenerimit të Çelësave HKDF (Funksioni Kryesor i Zgjerimit dhe Nxjerrjes me HMAC)
- Kriptimi i transmetimit ChaCha20 (disponohet versioni jo i optimizuar C)
- Algoritmi i Vërtetimit të Mesazhit Poly1305 (MAC) (C dhe versioni i montuesit)
- Protokolli Diffie-Hellman në lakoret eliptike Curve25519 (Versione C dhe montuese me optimizime të bazuara në udhëzimet BMI2 dhe ADX)
- Bllokoni mënyrën e shifrimit AEAD (shifër e vërtetuar) ChachaPoly (versioni C nuk është i optimizuar)
- Modaliteti i kriptimit të bllokut AEAD AES-GCM (versioni i mbledhësit me optimizime të AES-NI).
Ne fillim version alfa, verifikimi i kodit është përfunduar tashmë kryesisht, por ka ende disa zona të zbuluara.
Përveç kësaj, API nuk është stabilizuar ende, e cila do të zgjerohet në versionet vijuese alfa (Plannedshtë planifikuar të unifikohen strukturat për të gjitha API-të.
Ndër të metat, theksohet gjithashtu mbështetja për arkitekturën x86_64 (në fazën e parë, qëllimi kryesor është besueshmëria, ndërsa optimizimi dhe platformat do të zbatohen në vendin e dytë).
Fuente: https://jonathan.protzenko.fr