Raziskovalci Državni inštitut za raziskave v informatiki in avtomatizaciji (INRIA), Predstavila sta se Microsoft Research in Carnegie Mellon University prva preizkusna izdaja kripto knjižnico EverCrypt razvit v okviru projekta Everest in z uporabo matematičnih metod formalnega preverjanja zanesljivosti.
Zaradi svojih zmogljivosti in zmogljivosti EverCrypt je zelo blizu obstoječih kripto knjižnic (OpenSSL), vendar to za razliko od njih ponuja dodatna jamstva za zanesljivost in varnost.
Npr postopek preverjanja se nanaša na določanje podrobnih specifikacij ki opisujejo vsa vedenja programa in matematični dokaz, da je napisana koda ustreza pripravljenim specifikacijam.
Za razliko od metod nadzora kakovosti, ki temeljijo na dokazih, preverjanje zagotavlja zanesljiva jamstva da se bo program zagnal samo tako, kot so predvideli razvijalci, in da ni posebnih vrst napak.
Na primer skladnost s specifikacijo zagotavlja varno delo s pomnilnikom in odsotnost napak, ki vodijo do prelivanja medpomnilnika, na usmerjevalne kazalce, na dostop do že osvobojenih pomnilniških območij ali na dvojno sprostitev pomnilniških blokov.
Kaj je EverCrypt?
EverCrypt zagotavlja zanesljivo preverjanje vrste in vrednosti- Komponenta nikoli ne bo posredovala parametrov drugi neskladni komponenti in ne bo dobila dostopa do notranjih stanj drugih komponent.
Vhodno / izhodno vedenje v celoti ustreza preprostim dejanjem matematičnih funkcij, ki so opredeljeni v kriptografskih standardih.
Za zaščito pred napadi v tujih kanalih, vedenje med izračuni (na primer trajanje izvedbe ali prisotnost dostopa do določenega pomnilnika) ni odvisno od tajnih podatkov, ki se obdelujejo.
Koda projekta je napisano v funkcionalnem jeziku F * (Zvezda F) , ki zagotavlja sistem odvisnih vrst in izboljšav, ki omogočajo določitev natančnih specifikacij (matematični model) za programe ter zagotavljanje pravilnosti in odsotnosti napak pri izvedbi s pomočjo formul SMT in pomožnih testnih orodij.
Koda v F * se distribuira pod licenco Apache 2.0, končni moduli pa v jeziku C in asembler pod licenco MIT.
Na podlagi referenčne kode F *, ustvarjen je asembler, C, OCaml, JavaScript in kodo spletnega sestavljanja.
Nekateri deli kode pripravljen po projektu že uporabljajo v Firefoxu, jedru sistema Windows , veriga blokov Tezos in VPN Wireguard.
Komponente EverCrypt
V bistvu, EverCrypt združuje dva različna projekta HACL * in Vale, ki zagotavlja poenoten API na njihovi osnovi in jih naredi primerne za uporabo v resničnih projektih.
HACL * je zapisan z nizko* in njegov cilj je zagotoviti kriptografske primitive za uporabo v programih C, ki uporabljajo API-je za libodij in NaCL.
Projekt Vale je razvil poseben jezik domeno za ustvarjanje preverjanj v sestavljalniku.
Združi se približno 110 tisoč vrstic kode HACL * v jeziku Low * in 25 tisoč vrstic kode za Vale in so prepisani v približno 70 tisoč vrstic kode v univerzalnem jeziku F *, ki se prav tako razvija v okviru projekta Everest.
Prva različica knjižnice EverCrypt vsebuje preverjene izvedbe naslednjih kriptografskih algoritmov predlagano v različici C ali asemblerju (pri uporabi.
Od tega na strani projekta izstopajo:
- Razpršeni algoritmi: vse različice SHA2, SHA3, SHA1 in MD5
- Kode za preverjanje pristnosti: HMAC prek SHA1, SHA2-256, SHA2-384 in SHA2-512 za overjanje virov podatkov
- Algoritam generiranja ključa HKDF (funkcija izpeljave ključa za razširitev in ekstrakcijo ključa na osnovi HMAC)
- Šifriranje toka ChaCha20 (na voljo ne-optimizirana različica C)
- Algoritem za preverjanje pristnosti sporočil Poly1305 (MAC) (različica C in asembler)
- Diffie-Hellmanov protokol na eliptičnih krivuljah Curve25519 (različice C in asemblerja z optimizacijami na podlagi navodil BMI2 in ADX)
- Način blokirne šifre AEAD (overjena šifra) ChachaPoly (različica C ni optimizirana)
- Način šifriranja AEAD AES-GCM (različica sestavljavca z optimizacijami AES-NI).
V prvem različica alfa, je preverjanje kode že končano v glavnem pa je še vedno nekaj odkritih področij.
Poleg tega, API še ni stabiliziran, ki bo razširjena v naslednjih različicah alfa (Načrtuje se poenotenje struktur za vse API-je.
Med napakami je izpostavljena tudi podpora za arhitekturo x86_64 (v prvi fazi je glavni cilj zanesljivost, na drugem mestu pa bodo uvedene optimizacija in platforme).
vir: https://jonathan.protzenko.fr