EverCrypt: eng kryptographesch Verifikatiounsbibliothéik

everest Projet

Fuerscher aus Staatlechen Institut fir Fuerschung an Informatik an Automatiséierung (INRIA), Microsoft Research a Carnegie Mellon University presentéiert déi éischt Test Editioun vum der EverCrypt Krypto Bibliothéik am Kader vum Everest Projet entwéckelt a mat mathematesche Methode vun der formeller Zouverlässegkeet Verifikatioun benotzt.

Fir seng Fäegkeeten a Performance, EverCrypt ass ganz no bei existente Krypto Bibliothéiken (OpenSSL) awer dat, am Géigesaz zu hinnen, bitt zousätzlech Garantien fir Zouverlässegkeet a Sécherheet.

Zum Beispill, de Verifikatiounsprozess geet op d'Definitioun vun detailléierte Spezifikatiounen déi all d'Behuele vum Programm beschreiwen an de mathematesche Beweis datt de geschriwwene Code entsprécht virbereet Spezifikatiounen.

Am Géigesaz zu evidenzbaséierter Qualitéitskontrollmethoden, Verifikatioun bitt zouverléisseg Garantien datt de Programm nëmme leeft wéi d'Entwéckler virgesinn an et gi keng spezifesch Klasse vu Feeler.

Zum Beispill d'Konformitéit mat der Spezifikatioun garantéiert sécher Aarbecht mat Gedächtnis an d'Feele vu Feeler, déi zu Puffer Iwwerlaf féieren, fir Dereferenzzeechner, fir Zougang zu scho befreitene Gedächtnisberäicher, oder fir d'duebel Befreiung vu Gedächtnisblocken.

Wat ass EverCrypt?

EverCrypt stellt robuste Typ a Wäertkontroll- Eng Komponent wäert ni Parameteren un déi aner net konform Komponent weiderginn a kritt keen Zougang zu den internen Zoustänn vun den anere Komponenten.

Den Input / Output Verhalen voll entsprécht einfache mathematesche Funktiounsaktiounen, déi a kryptographesche Standarden definéiert sinn.

Fir géint Attacken ze schützen an Drëtt Partei Kanäl, Verhalen während Berechnungen (zum Beispill d'Dauer vun der Ausféierung oder d'Präsenz vun Zougang zu gewësse Gedächtnis) et hänkt net vun de geheime Daten of, déi veraarbecht ginn.

De Projet Code ass an der funktioneller Sprooch F * geschriwwe ginn (F Stär) , deen e System vun ofhängegen Typen a Verfeinerunge bitt, déi et erlaben exakt Spezifikatioune festzeleeën (mathematescht Modell) fir d'Programmer an d'Korrektheet an d'Feele vu Feeler bei der Ëmsetzung duerch SMT Formelen an Hëllefstestinstrumenter ze garantéieren.

De Code am F * gëtt ënner der Apache 2.0 Lizenz verdeelt, an de leschte Moduler an C an dem Assembléeur ënner der MIT Lizenz.

Baséiert op de Referenzcode F *, assembler, C, OCaml, JavaScript gëtt generéiert an de Web Versammlungscode.

E puer Deeler vum Code virbereet vum Projet gi schonn am Firefox benotzt, de Windows Kernel , d'Blockchain vun Tezos a VPN Wireguard.

EverCrypt Komponenten

Am Wesentlechen, EverCrypt kombinéiert zwee virdrun disparéiert Projete vun HACL * a Vale, eng vereenegt API ze baséieren op Basis vun hinnen a se gëeegent fir ze benotzen an echte Projeten.

HACL * ass a Low geschriwwen* a säin Zil ass kryptographesch Primitiven ze bidden fir se an C Programmer ze benotzen déi si benotze Libsodium an NaCL Stil APIen.

De Projet Vale huet eng spezifesch Sprooch entwéckelt Domain fir Verifikatiounen am Versammler ze kreéieren.

Ongeféier 110 Dausend Linnen HACL * Code a Low * Sprooch a 25 Dausend Linne Code fir Vale sinn kombinéiert a si sinn a 70 Tausend Zeilen Code ëmgeschriwwe ginn an der universeller Sprooch F *, déi och entwéckelt gëtt als Deel vum Everest Projet.

Déi éischt Versioun vun der EverCrypt Bibliothéik Features verifizéiert Implementatiounen vun de folgenden kryptographeschen Algorithmen proposéiert an C oder Versammlungsversiounen (wann Dir de benotzt.

Vun dësen, falen déi folgend op der Projetssäit eraus:

  • Hash Algorithmen: all Varianten vu SHA2, SHA3, SHA1, an MD5
  • Authentifikatiounscoden: HMAC iwwer SHA1, SHA2-256, SHA2-384, an SHA2-512 fir Datenquell Authentifizéierung
  • HKDF Schlëssel Generatioun Algorithmus (HMAC-baséiert Extraktioun an Expansioun Schlëssel Derivatioun Funktioun)
  • ChaCha20 Stream Verschlësselung (net optimiséiert C Versioun verfügbar)
  • Poly1305 Message Authentifizéierung Algorithmus (MAC) (C an Assembler Versioun)
  • Diffie-Hellman Protokoll op elliptesche Kéieren Curve25519 (C an Assembler Versiounen mat Optimiséierungen baséiert op BMI2 an ADX Instruktiounen)
  • Block Chiffer Mode AEAD (authentifizéierten Chiffer) ChachaPoly (Versioun C net optimiséiert)
  • AEAD AES-GCM Block Verschlësselungsmodus (Versammlungsversioun mat AES-NI Optimisatiounen).

An der éischter alfa Versioun, Code Verifikatioun ass scho fäerdeg gréisstendeels, awer et sinn nach e puer Beräicher opgedeckt.

Och, API ass nach net stabiliséiert, déi ausgebaut ginn an de folgenden Alpha Versiounen (Et ass geplangt Strukturen fir all APIen ze vereenegen.

Ënner de Mängel gëtt d'Ënnerstëtzung fir d'x86_64 Architektur och beliicht (an der éischter Etapp ass d'Haaptziel Zouverlässegkeet, wärend Optimiséierung a Plattformen op der zweeter Plaz ëmgesat ginn).

Source: https://jonathan.protzenko.fr


Den Inhalt vum Artikel hält sech un eis Prinzipie vun redaktionnell Ethik. Fir e Feeler ze mellen klickt hei.

Gitt d'éischt fir ze kommentéieren

Gitt Äre Kommentar

Är Email Adress gëtt net publizéiert ginn. Néideg Felder sinn markéiert mat *

*

*

  1. Responsabel fir d'Daten: Miguel Ángel Gatón
  2. Zweck vun den Donnéeën: Kontroll SPAM, Kommentarmanagement.
  3. Legitimatioun: Är Zoustëmmung
  4. Kommunikatioun vun den Donnéeën: D'Donnéeë ginn net un Drëttubidder matgedeelt ausser duerch legal Verpflichtung.
  5. Datenspeicher: Datebank gehost vun Occentus Networks (EU)
  6. Rechter: Zu all Moment kënnt Dir Är Informatioun limitéieren, recuperéieren an läschen.