Forscher Staatliches Institut für Informatik- und Automatisierungsforschung (INRIA), Microsoft Research und Carnegie Mellon University vorgestellt die erste Testausgabe von die EverCrypt-Kryptobibliothek entwickelt im Rahmen des Everest-Projekts und unter Verwendung mathematischer Methoden zur formalen Zuverlässigkeitsüberprüfung.
Für seine Fähigkeiten und Leistung, EverCrypt ist sehr nah an vorhandenen Kryptobibliotheken (OpenSSL) bietet jedoch im Gegensatz zu ihnen zusätzliche Garantien für Zuverlässigkeit und Sicherheit.
Zum Beispiel Der Überprüfungsprozess läuft darauf hinaus, detaillierte Spezifikationen zu definieren das beschreibt alle Verhaltensweisen des Programms und der mathematische Beweis, dass der geschriebene Code erfüllt vorbereitete Spezifikationen.
Im Gegensatz zu evidenzbasierten Qualitätskontrollmethoden Die Überprüfung bietet zuverlässige Garantien dass das Programm nur wie von den Entwicklern beabsichtigt ausgeführt wird und es keine spezifischen Fehlerklassen gibt.
Zum Beispiel die Einhaltung der Spezifikation sorgt für sicheres Arbeiten mit dem Speicher und das Fehlen von Fehlern, die zu einem Pufferüberlauf führen, um Zeiger zu dereferenzieren, auf bereits freigegebene Speicherbereiche zuzugreifen oder Speicherblöcke doppelt freizugeben.
Was ist EverCrypt?
EverCrypt Bietet zuverlässige Typprüfung und Wertprüfung- Eine Komponente übergibt niemals Parameter an die andere nicht konforme Komponente und erhält keinen Zugriff auf die internen Zustände der anderen Komponenten.
Das Eingabe- / Ausgabeverhalten entspricht vollständig einfachen mathematischen Funktionsaktionen, die in kryptografischen Standards definiert sind.
Zum Schutz vor Angriffen in Kanälen von Drittanbietern, Verhalten bei Berechnungen (zum Beispiel die Dauer der Ausführung oder das Vorhandensein von Zugriffen auf einen bestimmten Speicher) es hängt nicht von den geheimen Daten ab, die verarbeitet werden.
Der Projektcode ist in der Funktionssprache F * geschrieben (F-Stern) , Dies bietet ein System von abhängigen Typen und Verfeinerungen, die es ermöglichen, genaue Spezifikationen (mathematisches Modell) für die Programme festzulegen und die Richtigkeit und das Fehlen von Fehlern bei der Implementierung mittels SMT-Formeln und zusätzlichen Testwerkzeugen zu gewährleisten.
Der Code in F * wird unter der Apache 2.0-Lizenz verteilt, die endgültigen Module in C und der Assembler unter der MIT-Lizenz.
Basierend auf dem Referenzcode F *, Assembler, C, OCaml, JavaScript wird generiert und den Webassemblierungscode.
Einige Teile des Codes vorbereitet vom Projekt werden bereits in Firefox der Windows-Kernel verwendet , die Blockchain von Tezos und VPN Wireguard.
EverCrypt-Komponenten
Im Wesentlichen, EverCrypt kombiniert zwei bisher unterschiedliche Projekte von HACL * und ValeBereitstellung einer darauf basierenden einheitlichen API, die für die Verwendung in realen Projekten geeignet ist.
HACL * ist in Low geschrieben* und sein Ziel ist es, kryptografische Grundelemente zur Verwendung in C-Programmen bereitzustellen, die Sie verwenden die APIs im libsodium- und NaCL-Stil.
Das Projekt Vale entwickelte eine bestimmte Sprache Domäne zum Erstellen von Überprüfungen im Assembler.
Etwa 110 Zeilen HACL * -Code in der Sprache Low * und 25 Codezeilen für Vale werden kombiniert und sie werden in rund 70 Codezeilen in der universellen Sprache F * umgeschrieben, die ebenfalls entwickelt wird als Teil des Everest-Projekts.
Die erste Version der EverCrypt-Bibliothek verfügt über verifizierte Implementierungen der folgenden kryptografischen Algorithmen vorgeschlagen in C- oder Assembler-Versionen (bei Verwendung der.
Davon fallen auf der Projektseite folgende auf:
- Hash-Algorithmen: Alle Varianten von SHA2, SHA3, SHA1 und MD5
- Authentifizierungscodes: HMAC über SHA1, SHA2-256, SHA2-384 und SHA2-512 für die Datenquellenauthentifizierung
- HKDF-Schlüsselgenerierungsalgorithmus (HMAC-basierte Funktion zum Extrahieren und Erweitern von Schlüsseln)
- ChaCha20-Stream-Verschlüsselung (nicht optimierte C-Version verfügbar)
- Poly1305-Nachrichtenauthentifizierungsalgorithmus (MAC) (C- und Assembler-Version)
- Diffie-Hellman-Protokoll für elliptische Kurven Curve25519 (C- und Assembler-Versionen mit Optimierungen basierend auf BMI2- und ADX-Anweisungen)
- Blockverschlüsselungsmodus AEAD (authentifizierte Verschlüsselung) ChachaPoly (Version C nicht optimiert)
- AEAD AES-GCM-Blockverschlüsselungsmodus (Assembler-Version mit AES-NI-Optimierungen).
In der ersten Alpha-Version, Codeüberprüfung ist bereits abgeschlossen weitgehend, aber es gibt noch einige Bereiche, die nicht abgedeckt sind.
Zusätzlich API ist noch nicht stabilisiert, die erweitert wird in den folgenden Alpha-Versionen (Es ist geplant, Strukturen für alle APIs zu vereinheitlichen.
Unter den Fehlern wird auch die Unterstützung der x86_64-Architektur hervorgehoben (in der ersten Phase ist das Hauptziel die Zuverlässigkeit, während die Optimierung und die Plattformen an zweiter Stelle implementiert werden).
Quelle: https://jonathan.protzenko.fr