Forskere av Statens institutt for forskning i informatikk og automatisering (INRIA), Microsoft Research og Carnegie Mellon University presenterte den første prøveutgaven av EverCrypt-kryptobiblioteket utviklet innenfor rammen av Everest-prosjektet og ved hjelp av matematiske metoder for formell pålitelighetsverifisering.
For dets evner og ytelse, EverCrypt er veldig nær eksisterende kryptobiblioteker (OpenSSL), men som, i motsetning til dem, gir ytterligere garantier for pålitelighet og sikkerhet.
Eg bekreftelsesprosessen går ut på å definere detaljerte spesifikasjoner som beskriver all oppførselen til programmet og det matematiske beviset på at den skrevne koden oppfyller utarbeidede spesifikasjoner.
I motsetning til bevisbaserte kvalitetskontrollmetoder, verifisering gir pålitelige garantier at programmet kun vil kjøre som utviklerne hadde til hensikt, og at det ikke er noen spesifikke feilklasser.
For eksempel samsvar med spesifikasjonen sørger for sikkert arbeid med minne og fravær av feil som fører til bufferoverløp, til henvisningspekere, for å få tilgang til allerede frigjorte minneområder, eller til dobbel frigjøring av minneblokker.
Hva er EverCrypt?
EverCrypt gir robust type og verdikontroll- En komponent vil aldri overføre parametere til den andre ikke-samsvarende komponenten og vil ikke få tilgang til de interne tilstandene til de andre komponentene.
Input / output atferd samsvarer helt med enkle matematiske funksjonshandlinger, som er definert i kryptografiske standarder.
For å beskytte mot angrep i tredjepartskanaler, oppførsel under beregninger (for eksempel varigheten av utførelsen eller tilstedeværelsen av tilgang til bestemt minne) det avhenger ikke av de hemmelige dataene som behandles.
Prosjektkoden er skrevet på funksjonsspråket F * (F-stjerne) , som gir et system av avhengige typer og forbedringer, som gjør det mulig å etablere eksakte spesifikasjoner (matematisk modell) for programmene og garantere korrekthet og fravær av feil i implementeringen ved hjelp av SMT-formler og hjelpetestverktøy.
Koden i F * distribueres under Apache 2.0-lisensen, og de endelige modulene i C og montøren under MIT-lisensen.
Basert på referansekoden F *, assembler, C, OCaml, JavaScript genereres og nettmonteringskoden.
Noen deler av koden forberedt av prosjektet brukes allerede i Firefox, Windows-kjernen , blockchain av Tezos og VPN Wireguard.
EverCrypt-komponenter
I hovedsak, EverCrypt kombinerer to tidligere forskjellige prosjekter fra HACL * og Vale, gir en samlet API basert på dem og gjør dem egnet til bruk i ekte prosjekter.
HACL * er skrevet i Lavt* og målet er å gi kryptografiske primitiver for bruk i C-programmer som de bruker libsodium og NaCL stil APIer.
Prosjektet Vale utviklet et bestemt språk domene for å opprette bekreftelser i samleren.
Cirka 110 tusen linjer med HACL * -kode på lavt * språk og 25 tusen linjer med kode for Vale er kombinert og de blir omskrevet i rundt 70 tusen kodelinjer på det universelle språket F *, som også utvikles som en del av Everest-prosjektet.
Den første versjonen av EverCrypt-biblioteket har bekreftede implementeringer av følgende kryptografiske algoritmer foreslått i C- eller monteringsversjoner (når du bruker.
Av disse skiller seg følgende ut på prosjektsiden:
- Hash-algoritmer: alle varianter av SHA2, SHA3, SHA1 og MD5
- Autentiseringskoder: HMAC over SHA1, SHA2-256, SHA2-384 og SHA2-512 for datakildeautentisering
- HKDF-nøkkelgenereringsalgoritme (HMAC-basert ekstrakt og utvid nøkkelavledningsfunksjon)
- ChaCha20-streamkryptering (ikke-optimalisert C-versjon tilgjengelig)
- Poly1305 Message Authentication Algorithm (MAC) (C and assembler version)
- Diffie-Hellman-protokoll om elliptiske kurver Curve25519 (C- og assemblerversjoner med optimaliseringer basert på BMI2- og ADX-instruksjoner)
- Blokkér krypteringsmodus AEAD (godkjent kryptering) ChachaPoly (versjon C er ikke optimalisert)
- AEAD AES-GCM blokkrypteringsmodus (assemblerversjon med AES-NI-optimaliseringer).
I det første alfaversjon, er kodeverifisering allerede fullført i stor grad, men det er fortsatt noen områder som er avdekket.
Videre API er ikke stabilisert ennå, som skal utvides i de følgende alfaversjonene (Det er planlagt å forene strukturer for alle API-er.
Blant feilene er også støtte for x86_64-arkitekturen fremhevet (i første fase er hovedmålet pålitelighet, mens optimalisering og plattformer vil bli implementert på andreplass).
Fuente: https://jonathan.protzenko.fr