EverCrypt: biblioteka za kriptografsku provjeru

everest projekt

Istraživači iz Državni institut za istraživanje informatike i automatizacije (INRIA), Predstavili su Microsoft Research i Sveučilište Carnegie Mellon prvo probno izdanje kriptoteka EverCrypt razvijen u okviru projekta Everest i koristeći matematičke metode formalne provjere pouzdanosti.

Zbog svojih mogućnosti i performansi, EverCrypt je vrlo blizu postojećim kripto knjižnicama (OpenSSL), ali to, za razliku od njih, nudi dodatna jamstva pouzdanosti i sigurnosti.

Npr. postupak provjere svodi se na definiranje detaljnih specifikacija koji opisuju sva ponašanja programa i matematički dokaz da je napisani kod zadovoljava pripremljene specifikacije.

Za razliku od metoda kontrole kvalitete temeljenih na dokazima, provjera pruža pouzdana jamstva da će se program izvoditi samo onako kako su programeri namjeravali i da nema specifičnih vrsta pogrešaka.

Na primjer, usklađenost sa specifikacijama osigurava siguran rad s memorijom i odsutnost pogrešaka koje dovode do prepunjenja međuspremnika, na pokazivače za preusmjeravanje, pristup već oslobođenim memorijskim područjima ili dvostruko oslobađanje memorijskih blokova.

Što je EverCrypt?

EverCrypt pruža robusnu provjeru tipa i vrijednosti- Komponenta nikada neće proslijediti parametre drugoj nesukladnoj komponenti i neće dobiti pristup unutarnjim stanjima ostalih komponenata.

Ponašanje ulaz / izlaz u potpunosti odgovara jednostavnim radnjama matematičke funkcije, koji su definirani u kriptografskim standardima.

Za zaštitu od napada na kanalima treće strane, ponašanje tijekom izračuna (na primjer, trajanje izvršenja ili prisutnost pristupa određenoj memoriji) ne ovisi o tajnim podacima koji se obrađuju.

Kod projekta napisan je u funkcionalnom jeziku F * (F zvijezda) , koji pruža sustav ovisnih tipova i usavršavanja, koji omogućuju uspostavljanje točnih specifikacija (matematički model) za programe i jamče ispravnost i odsutnost pogrešaka u implementaciji pomoću SMT formula i pomoćnih alata za testiranje.

Kôd u F * distribuira se pod licencom Apache 2.0, a konačni moduli u C i asembler pod licencom MIT.

Na temelju referentnog koda F *, asembler, C, OCaml, generira se JavaScript i kod web okupljanja.

Neki dijelovi koda pripremljena po projektu se već koriste u Firefoxu, Windows jezgri , blockchain od Tezos i VPN Wireguard.

EverCrypt komponente

U suštini, EverCrypt kombinira dva prethodno različita projekta od HACL * i Valea, pružajući na njima jedinstveni API i čineći ih pogodnima za upotrebu u stvarnim projektima.

HACL * napisan je malim slovom* i njegov je cilj pružiti kriptografske primitive za upotrebu u C programima koji koriste API-je za libsodium i NaCL.

Projekt Vale je razvio specifičan jezik domena za stvaranje provjera u asembleru.

Kombinira se oko 110 tisuća redaka HACL * koda na jeziku Low * i 25 tisuća redaka koda za Vale a prepisani su u oko 70 tisuća redaka koda na univerzalnom jeziku F *, koji se također razvija u sklopu projekta Everest.

Prva verzija knjižnice EverCrypt značajke provjerene implementacije sljedećih kriptografskih algoritama predložen u C ili asemblerskoj verziji (kada se koristi.

Od njih se na stranici projekta ističu:

  • Hash algoritmi: sve inačice SHA2, SHA3, SHA1 i MD5
  • Autentifikacijski kodovi: HMAC preko SHA1, SHA2-256, SHA2-384 i SHA2-512 za provjeru autentičnosti izvora podataka
  • Algoritam generiranja ključa HKDF (funkcija izvlačenja i proširenja ključa temeljena na HMAC-u)
  • Šifriranje streama ChaCha20 (dostupna je neoptimizirana C verzija)
  • Poly1305 algoritam provjere autentičnosti poruka (MAC) (C i asemblerska verzija)
  • Diffie-Hellmanov protokol na eliptičnim krivuljama Curve25519 (verzije C i asemblera s optimizacijama na temelju BMI2 i ADX uputa)
  • Način blok-šifre AEAD (ovjerena šifra) ChachaPoly (verzija C nije optimizirana)
  • AEAD AES-GCM način šifriranja bloka (asemblerska verzija s AES-NI optimizacijama).

U prvom alfa verzija, provjera koda je već završena uglavnom, ali još uvijek postoje neka područja koja nisu otkrivena.

Osim toga, API još nije stabiliziran, koji će se proširiti u sljedećim alfa verzijama (Planirano je objedinjavanje struktura za sve API-je.

Među nedostacima je također istaknuta kompatibilnost s arhitekturom x86_64 (u prvoj je fazi glavni cilj pouzdanost, dok će optimizacija i platforme biti implementirane na drugom mjestu).

izvor: https://jonathan.protzenko.fr


Budite prvi koji će komentirati

Ostavite svoj komentar

Vaša email adresa neće biti objavljen. Obavezna polja su označena s *

*

*

  1. Za podatke odgovoran: Miguel Ángel Gatón
  2. Svrha podataka: Kontrola neželjene pošte, upravljanje komentarima.
  3. Legitimacija: Vaš pristanak
  4. Komunikacija podataka: Podaci se neće dostavljati trećim stranama, osim po zakonskoj obvezi.
  5. Pohrana podataka: Baza podataka koju hostira Occentus Networks (EU)
  6. Prava: U bilo kojem trenutku možete ograničiti, oporaviti i izbrisati svoje podatke.