Викиновости

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

6 апреля 2019 года

Исследователи из французского государственного института исследований в информатике и автоматике (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 (на первом этапе главной целью является надёжность, а оптимизации и платформы будут реализованы во вторую очередь).

Источники

править


 
 
Creative Commons
Эта статья содержит материалы из статьи «Новая криптографическая библиотека EverCrypt с математическим доказательством надёжности», опубликованной OpenNET и распространяющейся на условиях лицензии Creative Commons Attribution (CC BY) — указание автора, источник и лицензию.
 
Эта статья загружена автоматически ботом NewsBots в архив и ещё не проверялась редакторами Викиновостей.
Любой участник может оформить статью: добавить иллюстрации, викифицировать, заполнить шаблоны и добавить категории.
Любой редактор может снять этот шаблон после оформления и проверки.

Комментарии

Викиновости и Wikimedia Foundation не несут ответственности за любые материалы и точки зрения, находящиеся на странице и в разделе комментариев.



Источник — https://ru.wikinews.org/w/index.php?title=Новая_криптографическая_библиотека_EverCrypt_с_математическим_доказательством_надёжности&oldid=8727995