Badacze z Państwowy Instytut Badań w Informatyce i Automatyzacji (INRIA), Przedstawiono Microsoft Research i Carnegie Mellon University pierwsze wydanie próbne biblioteka kryptograficzna EverCrypt opracowany w ramach projektu Everest z wykorzystaniem matematycznych metod formalnej weryfikacji niezawodności.
Ze względu na swoje możliwości i wydajność, EverCrypt jest bardzo zbliżony do istniejących bibliotek kryptograficznych (OpenSSL), ale w przeciwieństwie do nich daje dodatkowe gwarancje niezawodności i bezpieczeństwa.
Np. proces weryfikacji sprowadza się do określenia szczegółowych specyfikacji opisujące wszystkie zachowania programu oraz matematyczny dowód, że napisany kod spełnia przygotowane specyfikacje.
W przeciwieństwie do opartych na dowodach metod kontroli jakości, weryfikacja zapewnia rzetelne gwarancje że program będzie działał tylko zgodnie z zamierzeniami programistów i nie ma określonych rodzajów błędów.
Na przykład zgodność ze specyfikacją zapewnia bezpieczną pracę z pamięcią i brak błędów prowadzących do przepełnienia bufora, do wskaźników wyłuskiwania, dostępu do już zwolnionych obszarów pamięci lub do podwójnego zwalniania bloków pamięci.
Co to jest EverCrypt?
EverCrypt zapewnia niezawodne sprawdzanie typów i wartości- Komponent nigdy nie przekaże parametrów do innego niezgodnego komponentu i nie uzyska dostępu do stanów wewnętrznych innych komponentów.
Zachowanie wejścia / wyjścia w pełni odpowiada prostym działaniom funkcji matematycznych, które są zdefiniowane w standardach kryptograficznych.
Aby chronić przed atakami w kanałach zewnętrznych, zachowanie podczas obliczeń (na przykład czas trwania wykonania lub obecność dostępów do określonej pamięci) nie zależy od tajnych danych, które są przetwarzane.
Kod projektu jest napisany w języku funkcjonalnym F * (Gwiazda F) , który zapewnia system zależnych typów i udoskonaleń, które pozwalają ustalić dokładne specyfikacje (model matematyczny) programów oraz zagwarantować poprawność i brak błędów w realizacji za pomocą wzorów SMT oraz pomocniczych narzędzi testowych.
Kod w F * jest rozpowszechniany na licencji Apache 2.0, a końcowe moduły w C i assembler na licencji MIT.
Na podstawie kodu referencyjnego F *, asembler, C, OCaml, JavaScript i kod asemblera internetowego.
Niektóre części kodu przygotowane przez projekt są już używane w przeglądarce Firefox, jądrze systemu Windows , łańcuch bloków Tezos i VPN Wireguard.
Komponenty EverCrypt
W istocie EverCrypt łączy dwa wcześniej odmienne projekty z HACL * i Vale, dostarczając zunifikowane API oparte na nich i czyniąc je odpowiednimi do wykorzystania w rzeczywistych projektach.
HACL * jest napisane niskim* a jego celem jest dostarczenie prymitywów kryptograficznych do użycia w programach C. używają interfejsów API w stylu libsodium i NaCL.
Projekt Vale opracował specyficzny język domain do tworzenia weryfikacji w asemblerze.
Łącznie około 110 tysięcy wierszy kodu HACL * w języku Low * i 25 tysięcy wierszy kodu dla Vale i są przepisywane w około 70 tysiącach wierszy kodu w uniwersalnym języku F *, który również jest rozwijany w ramach projektu Everest.
Pierwsza wersja biblioteki EverCrypt zawiera sprawdzone wdrożenia następujących algorytmów kryptograficznych proponowane w wersjach C lub assembler (w przypadku korzystania z.
Spośród nich na stronie projektu wyróżniają się:
- Algorytmy skrótu: wszystkie warianty SHA2, SHA3, SHA1 i MD5
- Kody uwierzytelniania: HMAC przez SHA1, SHA2-256, SHA2-384 i SHA2-512 do uwierzytelniania źródła danych
- Algorytm generowania klucza HKDF (funkcja wyodrębniania i rozszerzania klucza opartego na HMAC)
- Szyfrowanie strumienia ChaCha20 (dostępna niezoptymalizowana wersja C)
- Algorytm uwierzytelniania wiadomości Poly1305 (MAC) (wersja C i assembler)
- Protokół Diffie-Hellmana na krzywych eliptycznych Curve25519 (wersje C i assembler z optymalizacjami opartymi na instrukcjach BMI2 i ADX)
- Tryb szyfrowania blokowego AEAD (szyfrowanie uwierzytelnione) ChachaPoly (wersja C niezoptymalizowana)
- Tryb szyfrowania blokowego AEAD AES-GCM (wersja asemblera z optymalizacją AES-NI).
Na początku wersja alfa, weryfikacja kodu została już zakończona w dużej mierze, ale nadal istnieją odkryte obszary.
Ponadto, API nie jest jeszcze ustabilizowane, który zostanie rozbudowany w kolejnych wersjach alfa (Planowane jest ujednolicenie struktur dla wszystkich interfejsów API.
Wśród wad wskazana jest również kompatybilność z architekturą x86_64 (w pierwszym etapie głównym celem jest niezawodność, na drugim miejscu zaimplementowana zostanie optymalizacja i platformy).
źródło: https://jonathan.protzenko.fr