Изследователи от Държавен институт за изследвания в информатиката и автоматизацията (INRIA), Представени бяха Microsoft Research и University of Carnegie Mellon първото пробно издание на крипто библиотеката EverCrypt разработена в рамките на проекта Everest и използваща математически методи за официална проверка на надеждността.
За своите възможности и производителност, EverCrypt е много близо до съществуващите крипто библиотеки (OpenSSL), но това, за разлика от тях, предлага допълнителни гаранции за надеждност и сигурност.
Например процесът на проверка се свежда до дефиниране на подробни спецификации които описват цялото поведение на програмата и математическото доказателство, че написаният код отговаря на подготвените спецификации.
За разлика от доказателствените методи за контрол на качеството, проверката предоставя надеждни гаранции че програмата ще работи само по предназначение на разработчиците и няма конкретни видове грешки.
Например спазване на спецификацията гарантира безопасна работа с памет и липса на грешки, които водят до препълване на буфера, за посочване на указатели, за достъп до вече освободени области на паметта или за двойно освобождаване на блокове памет.
Какво е EverCrypt?
EverCrypt осигурява надеждна проверка на типа и стойността- Компонентът никога няма да предаде параметри на другия несъответстващ компонент и няма да получи достъп до вътрешните състояния на другите компоненти.
Поведението на входа / изхода напълно отговаря на прости действия по математическа функция, които са дефинирани в криптографски стандарти.
За защита срещу атаки в канали на трети страни, поведение по време на изчисления (например продължителността на изпълнението или наличието на достъп до определена памет) това не зависи от секретните данни, които се обработват.
Кодът на проекта е написана на функционалния език F * (F звезда) , което осигурява система от зависими типове и усъвършенствания, които позволяват да се установят точни спецификации (математически модел) за програмите и да се гарантира коректността и липсата на грешки при изпълнението с помощта на SMT формули и помощни тестови инструменти.
Кодът във F * се разпространява под лиценза Apache 2.0, а крайните модули в C и асемблера под лиценза MIT.
Въз основа на референтния код F *, асемблер, C, OCaml, генерира се JavaScript и кода за уеб сглобяване.
Някои части от кода подготвен от проекта вече се използват във Firefox, ядрото на Windows , блокчейнът на Tezos и VPN Wireguard.
EverCrypt компоненти
По същество, EverCrypt комбинира два по-рано различни проекта от HACL * и Vale, предоставяйки унифициран API, базиран на тях и ги прави подходящи за използване в реални проекти.
HACL * е написан на ниско* и целта му е да осигури криптографски примитиви за използване в C програми, които те използват API на Libsodium и NaCL стил.
Проектът Вале разработи специфичен език домейн за създаване на проверки в асемблера.
Около 110 хиляди реда код HACL * на език Low * и 25 хиляди реда код за Vale са комбинирани и те са пренаписани в около 70 хиляди реда код на универсалния език F *, който също се разработва като част от проекта Еверест.
Първата версия на библиотеката EverCrypt разполага с проверени изпълнения на следните криптографски алгоритми предложена в C или асемблерна версия (когато се използва.
От тях на страницата на проекта се открояват следните:
- Хешови алгоритми: всички варианти на SHA2, SHA3, SHA1 и MD5
- Кодове за удостоверяване: HMAC през SHA1, SHA2-256, SHA2-384 и SHA2-512 за удостоверяване на източник на данни
- Алгоритъм за генериране на ключове HKDF (базирана на HMAC функция за извличане и разширяване на ключ за разширяване)
- Криптиране на потока ChaCha20 (налична е неоптимизирана версия C)
- Алгоритъм за удостоверяване на съобщения Poly1305 (MAC) (версия C и асемблер)
- Протокол Diffie-Hellman на елиптични криви Curve25519 (C и асемблерни версии с оптимизации, базирани на BMI2 и ADX инструкции)
- Режим на блоков шифър AEAD (удостоверен шифър) ChachaPoly (версия C не е оптимизирана)
- AEAD AES-GCM режим на шифроване на блокове (версия на асемблер с AES-NI оптимизации).
В първия алфа версия, проверката на кода вече е завършена до голяма степен, но все още има някои непокрити области.
Освен това, API все още не е стабилизиран, която ще бъде разширена в следните алфа версии (Планира се унифициране на структури за всички API.
Сред недостатъците е подчертана и поддръжката на архитектурата x86_64 (на първия етап основната цел е надеждността, докато оптимизацията и платформите ще бъдат внедрени на второ място).
Fuente: https://jonathan.protzenko.fr