Исследователи из государственного института исследований в информатике и автоматике (INRIA), подразделения Microsoft Research и университета Карнеги — Меллона представили (https://jonathan.protzenko.fr/2019/04/02/evercrypt-alpha1.html) первый тестовый выпуск (https://github.com/project-everest/hacl-star/releases) криптографической библиотеки EverCrypt (https://github.com/project-everest/hacl-star/blob/fstar-mast... развиваемой в рамках проекта Everest (https://project-everest.github.io/) и применяющей математические методы формальной верификации надёжности. По своим возможностям и производительности EverCrypt очень близка к существующим криптографическим библиотекам (OpenSSL), но в отличие от них предоставляет дополнительные гарантии надёжности и безопасности. Суть проведённой версификации в определении подробных спецификаций, описывающих все варианты поведения программы, и формировании математического доказательства, что написанный код полностью соответствует подготовленным спецификациям. В отличие от методов проверки качества на основе тестирования, верификация даёт надёжные гарантии, что программа будет выполняться только как задумали разработчики и в ней отсутствуют определённые классы ошибок.
Например, соответствие спецификации гарантирует безопасную работу с памятью и отсутствие ошибок, приводящих к переполнению буфера, разыменованию указателей, обращению к уже освобождённым областям памяти или двойное освобождение блоков памяти. В EverCrypt обеспечивается жесткая проверка типов и значений - один компонент никогда не передаст другому компоненту параметры, не соответствующие спецификации и не получит доступ ко внутренним состояниям других компонентов. Поведение при вводе/выводе полностью описано при помощи простых математических функций, описание которых определено в криптографических стандартах. Для защиты от атак по сторонним каналам поведение при вычислениях (например, время выполнения или обращение к памяти) никак не зависит от характера обрабатываемых секретных данных.
Код проекта написан на функциональном языке F* (https://www.fstar-lang.org/), предоставляющем (https://arxiv.org/abs/1703.00053) систему зависимых типов и уточнений, позволяющих задавать точные спецификации (математическую модель) для программ и гарантировать корректность и отсутствие ошибок в реализации при помощи SMT-формул (https://ru.wikipedia.org/wiki/%D0%97%D0%... и вспомогательных инструментов (https://en.wikipedia.org/wiki/Proof_assistant) доказательства. На основании эталонного кода на языке F* затем генерируется код на ассемблере, Си, OCaml, JavaScript и Web Assembly.
Код на языке F* распространяется (https://github.com/project-everest/hacl-star/) под лицензией Apache 2.0, а итоговые модули на Си и ассемблере под лицензией MIT. Некоторые части подготовленного проектом кода уже используются в Firefox (https://bugzilla.mozilla.org/show_bug.cgi?id=1387183), ядре Windows (https://www.microsoft.com/en-us/research/blog/evercrypt-cryp... блокчейне Tezos (https://www.reddit.com/r/tezos/comments/8hrsz2/tezos_switche... и VPN Wireguard (https://lwn.net/Articles/770750/).
Отмечается, что верификация позволяет избавиться от многих ошибок, но не исключает всех проблем:
- Используемый при разработке инструментарий остаётся не верифицированным, в том числе возможно существование ошибок в F*, KreMLin (https://github.com/FStarLang/kremlin) (верифицирующий транслятор из языка F* в Си) и в компиляторах для сборки кода на Си (если не использовать верифицированный CompCert (http://compcert.inria.fr/compcert-C.html)).
- Очень трудно правильно и точно воспроизвести спецификации. Например, где-то можно допустить опечатку, а где-то упустить вопрос преобразование порядка следования байтов. Поэтому до того как приступать к созданию оптимизированных версий реализации проводится доскональный аудит и тестирование спецификаций;
- Применяемые модели верификации не учитывают такие угрозы, как атаки
Spectre и Meltdown, а также не защищают от новых классов ещё не известных атак, которые могут появиться в будущем;
По сути EverCrypt объединяет два ранее разрозненных проекта HACL* (https://github.com/mitls/hacl-star) и Vale (https://github.com/project-everest/vale), предоставляя на их основе унифицированный API и делая их пригодными для применения в реальных проектах. HACL* написан на языке Low* и нацелен на предоставление криптопримитивов для использования в программах на языке Си с использованием API в стиле libsodium и NaCL. Проект Vale развивал предметно-ориентированный язык для создания верифицированных криптографических примитивов на ассемблере. Около 110 тысяч кода проекта HACL* на языке Low* и 25 тысяч строк кода на Vale объединены и переписаны в примерно 70 тысяч строк кода на универсальном языке F*, который также развивается в рамках проекта Everest. На базе созданных верифицированных примитивов проектом Everest дополнительно развивается стек miTLS (https://mitls.org/) с верифицированной реализацией TLSv1.3.
В первом выпуске библиотеки EverCrypt представлены верифицированные реализации следующих криптографических алгоритмов, которые предложены в вариантах на Си или ассемблере (при использовании библиотеки автоматически выбирается оптимальная для текущей платформы реализация):
- Алгоритмы хэшировния: все вариаенты SHA2, SHA3, SHA1 и MD5;
- Коды проверки подлинности: HMAC поверх SHA1, SHA2-256, SHA2-384 и SHA2-512 для аутентификации источника данных;
- Алгоритм формирования ключей HKDF (https://en.wikipedia.org/wiki/HKDF) (HMAC-based Extract-and-Expand Key Derivation Function);
- Потоковый шифр ChaCha20 (http://cr.yp.to/chacha.html) (доступна не оптимизированная версия на Си)
- Алгоритм аутентификации сообщений (MAC) Poly1305 (http://cr.yp.to/mac.html) (версии на Си и ассемблере),
- Протокол Диффи-Хеллмана на эллиптических кривых 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 (на первом этапе главной целью является надёжность, а оптимизации и платформы будут реализованы во вторую очередь).
URL: https://news.ycombinator.com/item?id=19563073
Новость: https://www.opennet.ru/opennews/art.shtml?num=50470
