Новая криптографическая библиотека EverCrypt с математическим доказательством надёжности

[лаки лучано 7]

Исследователи из государственного института исследований в информатике и автоматике (INRIA), подразделения Microsoft Research и университета Карнеги — Меллона представили первый тестовый выпуск криптографической библиотеки EverCrypt, развиваемой в рамках проекта Everest и применяющей математические методы формальной верификации надёжности. По своим возможностям и производительности EverCrypt очень близка к существующим криптографическим библиотекам (OpenSSL), но в отличие от них предоставляет дополнительные гарантии надёжности и безопасности.

Процесс верификации сводится к определению подробных спецификаций, описывающих все варианты поведения программы, и формированию математического доказательства, что написанный код полностью соответствует подготовленным спецификациям. В отличие от методов проверки качества на основе тестирования, верификация даёт надёжные гарантии, что программа будет выполняться только как задумали разработчики и в ней отсутствуют определённые классы ошибок.

Например, соответствие спецификации гарантирует безопасную работу с памятью и отсутствие ошибок, приводящих к переполнению буфера, разыменованию указателей, обращению к уже освобождённым областям памяти или двойному освобождению блоков памяти. В EverCrypt обеспечивается жёсткая проверка типов и значений - один компонент никогда не передаст другому компоненту параметры, не соответствующие спецификации и не получит доступ ко внутренним состояниям других компонентов. Поведение при вводе/выводе полностью укладывается в действия простых математических функций, описание которых определено в криптографических стандартах. Для защиты от атак по сторонним каналам поведение при вычислениях (например, продолжительность выполнения или наличие обращений к определённой памяти) никак не зависит от характера обрабатываемых секретных данных.

Код проекта написан на функциональном языке F*, предоставляющем систему зависимых типов и уточнений, позволяющих задавать точные спецификации (математическую модель) для программ и гарантировать корректность и отсутствие ошибок в реализации при помощи SMT-формул и вспомогательных инструментов доказательства. На основании эталонного кода на языке F* затем генерируется код на ассемблере, Си, OCaml, JavaScript и Web Assembly. Код на языке F* распространяется под лицензией Apache 2.0, а итоговые модули на Си и ассемблере под лицензией MIT. Некоторые части подготовленного проектом кода уже используются в Firefox, ядре Windows, блокчейне Tezos и VPN Wireguard.

Отмечается, что верификация позволяет избавиться от многих ошибок, но не исключает всех проблем:

• Используемый при разработке инструментарий остаётся не верифицированным, в том числе возможно существование ошибок в F*, KreMLin (верифицирующий транслятор из языка F* в Си) и в компиляторах для сборки кода на Си (если не использовать верифицированный CompCert).

• Очень трудно правильно и точно воспроизвести спецификации. Например, где-то можно допустить опечатку, а где-то упустить вопрос преобразование порядка следования байтов. Поэтому до того как приступать к созданию оптимизированных версий реализации проводится доскональный аудит и тестирование спецификаций.

• Применяемые модели верификации не учитывают такие угрозы, как атаки Spectre и Meltdown, а также не защищают от новых классов ещё не известных атак, которые могут появиться в будущем.

По сути EverCrypt объединяет два ранее разрозненных проекта HACL* и Vale, предоставляя на их основе унифицированный API и делая их пригодными для применения в реальных проектах. HACL* написан на языке Low* и нацелен на предоставление криптопримитивов для использования в программах на языке Си с использованием API в стиле libsodium и NaCL. Проект Vale развивал предметно-ориентированный язык для создания верифицированных криптографических примитивов на ассемблере. Около 110 тысяч строк кода проекта HACL* на языке Low* и 25 тысяч строк кода на Vale объединены и переписаны в примерно 70 тысяч строк кода на универсальном языке F*, который также развивается в рамках проекта Everest. На базе созданных верифицированных примитивов проектом Everest дополнительно развивается стек miTLS с верифицированной реализацией TLSv1.3.

В первом выпуске библиотеки EverCrypt представлены верифицированные реализации следующих криптографических алгоритмов, которые предложены в вариантах на Си или ассемблере (при использовании библиотеки автоматически выбирается оптимальная для текущей платформы реализация):

• Алгоритмы хэшировния: все варианты SHA2, SHA3, SHA1 и MD5;
Коды проверки подлинности: HMAC поверх SHA1, SHA2-256, SHA2-384 и SHA2-512 для аутентификации источника данных.

•Алгоритм формирования ключей HKDF (HMAC-based Extract-and-Expand Key Derivation Function).

• Потоковый шифр ChaCha20 (доступна неоптимизированная версия на Си).

• Алгоритм аутентификации сообщений (MAC) Poly1305 (версии на Си и ассемблере).

• Протокол Диффи-Хеллмана на эллиптических кривых Curve25519 (версии на Си и ассемблере с оптимизациями на базе инструкций BMI2 и ADX).

• AEAD режим блочного шифрования (аутентифицированное шифрование) ChachaPoly (неоптимизированная версия на Си)

• AEAD режим блочного шифрования AES-GCM (версия на ассемблере с оптимизациями AES-NI).

В первом альфа-выпуске уже в основной массе завершена верификация кода, но ещё остаются некоторые неохваченные области. Пока не верифицированы и не включены в поставку оптимизированные при помощи инструкций SHA-EXT и AVX варианты SHA2-256 и Poly130. Обещанный уровень производительности в текущий момент обеспечен только для алгоритма Curve25519.

Также ещё не стабилизирован API, который будет расширяться в следующих альфа-версиях (планируется унифицировать структуры для всех API по примеру наиболее зрелого EverCrypt_Hash.h и унифицировать коды ошибок в EverCrypt.Error). Из недоработок также отмечается поддержка только архитектуры x86_64 (на первом этапе главной целью является надёжность, а оптимизации и платформы будут реализованы во вторую очередь).

• Source: https://jonathan.protzenko.fr/2019/04/02/evercrypt-alpha1.html

• Source: https://github.com/project-everest/hacl-star/releases