Istraživači iz Državni istraživački institut za računarstvo i automatizaciju (INRIA), Predstavljen Microsoft Research i Carnegie Mellon University prvo probno izdanje kriptografsku biblioteku EverCrypt razvijen u okviru projekta Everest i korišćenjem matematičkih metoda formalne verifikacije pouzdanosti.
Zbog svojih mogućnosti i performansi, EverCrypt je vrlo blizak postojećim kripto bibliotekama (OpenSSL), ali, za razliku od njih, nudi dodatne garancije pouzdanosti i sigurnosti.
Na primjer, proces verifikacije se svodi na definisanje detaljnih specifikacija koji opisuju sva ponašanja programa već matematički dokaz da je pisani kod zadovoljava pripremljene specifikacije.
Za razliku od metoda kontrole kvaliteta zasnovanih na testovima, verifikacija pruža pouzdane garancije da će program raditi samo onako kako su programeri namjeravali i da nema posebnih klasa grešaka.
Na primjer, usklađenost sa specifikacijom osigurava siguran rad s memorijom i odsustvo grešaka koje dovode do prekoračenja bafera, za dereferenciranje pokazivača, za pristup već oslobođenim memorijskim područjima ili za dvostruko oslobađanje memorijskih blokova.
Šta je EverCrypt?
EverCrypt pruža snažnu provjeru tipa i vrijednosti- Komponenta nikada neće prenijeti parametre drugoj komponenti koji ne zadovoljavaju specifikacije i neće dobiti pristup internim stanjima drugih komponenti.
Ponašanje ulaska/izlaska u potpunosti odgovara radnjama jednostavnih matematičkih funkcija, koji su definirani u kriptografskim standardima.
Za zaštitu od napada na kanalima trećih strana, ponašanje tokom proračuna (na primjer, trajanje izvršenja ili prisutnost pristupa određenoj memoriji) ne zavisi od tajnih podataka koji se obrađuju.
Kod projekta Napisano je funkcionalnim jezikom F* (F zvjezdica) , koji obezbeđuje sistem zavisnih tipova i usavršavanja, koji omogućavaju uspostavljanje tačnih specifikacija (matematičkog modela) za programe i osiguravanje ispravnosti i odsustva grešaka u implementaciji korišćenjem SMT formula i pomoćnih alata za testiranje.
Kod u F* se distribuira pod licencom Apache 2.0, a konačni moduli u C-u i asembler pod licencom MIT.
Na osnovu F* referentnog koda, generira se asembler, C, OCaml, JavaScript i web asemblerski kod.
Neki dijelovi koda pripremljeni od strane projekta se već koriste u Firefoxu, Windows kernelu , blockchain Tezos i Wireguard VPN.
EverCrypt komponente
U suštini, EverCrypt kombinuje dva prethodno različita projekta iz HACL* i Valea, pružajući jedinstveni API zasnovan na njima i čini ih pogodnim za upotrebu u stvarnim projektima.
HACL * je napisan niskim* i ima za cilj da obezbedi kriptografske primitive za upotrebu u C programima koji oni koriste libsodium i NaCL stil API-je.
Projekat Vale je razvio specifičan jezik domenu za kreiranje provjera u asembleru.
Kombinovano je oko 110 hiljada linija HACL koda * na Low * jeziku i 25 hiljada linija koda za Vale i prepisane su u oko 70 hiljada linija koda na univerzalnom jeziku F*, koji se također razvija u sklopu projekta Everest.
Prva verzija EverCrypt biblioteke ima provjerene implementacije sljedećih kriptografskih algoritama koji su predloženi u C ili asemblerskim verzijama (kada koristite biblioteku.
Od njih se na stranici projekta ističu sljedeće:
- Haš algoritmi: sve varijante SHA2, SHA3, SHA1 i MD5
- Kodovi za autentifikaciju: HMAC preko SHA1, SHA2-256, SHA2-384 i SHA2-512 za autentifikaciju izvora podataka
- HKDF (HMAC-bazirana funkcija ekstrakcije i proširenja ključeva) algoritam za generiranje ključeva
- ChaCha20 stream šifra (dostupna neoptimizirana C verzija)
- Poly1305 algoritam za provjeru autentičnosti poruke (MAC) (C i asemblerska verzija)
- Diffie-Hellman protokol na eliptičnim krivuljama Curve25519 (C i asemblerske verzije s optimizacijama zasnovanim na BMI2 i ADX uputama)
- AEAD način blok šifriranja (provjerena šifra) ChachaPoly (neoptimizirana C verzija)
- AEAD AES-GCM režim blok šifriranja (assembler verzija sa AES-NI optimizacijama).
U prvom alfa verzija, provjera koda je već završena uglavnom, ali još uvijek ima nekih nepokrivenih područja.
Takođe, API još nije stabiliziran, koji će biti proširen u sljedećim alfa verzijama (planirano je objediniti strukture za sve API-je.
Među nedostacima ističe se i podrška za arhitekturu x86_64 (u prvoj fazi je glavni cilj pouzdanost, dok će se u drugoj implementirati optimizacija i platforme).
Izvor: https://jonathan.protzenko.fr