ИИтог

F*: язык с доказательствами корректности, на котором написана боевая криптография Firefox и Linux

безопасностьРедакция ИИтогHacker News🔥56Рейтинг ИИтог56Влияние50Новизна30Релевантность65Неожиданность25Участники75Достоверность85

F* (читается «эф стар»), язык программирования общего назначения, ориентированный на доказательства: он поддерживает и чисто функциональный, и императивный стиль программирования, сочетая зависимые типы с автоматизацией доказательств на базе SMT-решателей и тактическим интерактивным доказательством теорем. Проекты на F* по умолчанию компилируются в OCaml; отдельные фрагменты можно извлечь в F#, в C или Wasm через инструмент KaRaMeL, либо в ассемблер через набор инструментов Vale. Сам F* реализован на F* и бутстрапится через OCaml. Язык распространяется под лицензией Apache 2.0, разработка ведётся открыто на GitHub силами Microsoft Research, Inria и сообщества.

Главный практический результат F*, проект Project Everest, который занимается созданием защищённого коммуникационного ПО с доказанной корректностью. Внутри него выросли: HACL*, библиотека высоконадёжных криптографических примитивов, написанная на F* и извлечённая в код на C; ValeCrypt, формально доказанные реализации криптопримитивов на языке Vale, встроенном в F*; EverCrypt, криптопровайдер, объединяющий HACL* и ValeCrypt в единое целое. Код из этих проектов уже используется в продакшене в Mozilla Firefox, ядре Linux, Python, mbedTLS, блокчейне Tezos, SDK электронного голосования ElectionGuard и VPN WireGuard.

Отдельный инструмент, EverParse, генерирует парсеры бинарных форматов: он производит C-код, извлечённый из формально доказанного описания на F*. Парсеры EverParse используются в продакшене в нескольких проектах, включая Windows Hyper-V, где каждый сетевой пакет, проходящий через облачную платформу Azure, сначала разбирается и проверяется кодом, сгенерированным EverParse. EverParse применяется и в других продакшен-сценариях, включая ebpf-for-windows.

F* остаётся активной темой исследований в сообществах языков программирования, формальных методов, безопасности и систем: на сайте перечислены десятки статей на конференциях PLDI, POPL, ICFP, CCS, USENIX Security и других, от семантики монад Дейкстры, лежащих в основе системы эффектов F*, до верифицированных реализаций TLS 1.3, QUIC, протокола Signal и стандарта ACME.

Ключевые факты

  • F* сочетает зависимые типы с автоматизацией доказательств через SMT-решатели и интерактивное доказательство теорем; компилируется в OCaml по умолчанию, с извлечением в F#, C/Wasm (через KaRaMeL) или ассемблер (через Vale)
  • Открытый исходный код на GitHub под лицензией Apache 2.0, разработка ведётся Microsoft Research, Inria и сообществом
  • Библиотеки HACL* (верифицированные криптопримитивы, извлекаются в C) и ValeCrypt (верифицированный ассемблер) объединяются в криптопровайдер EverCrypt, их код уже работает в продакшене в Firefox, ядре Linux, Python, mbedTLS, блокчейне Tezos, SDK ElectionGuard и VPN WireGuard
  • Генератор парсеров EverParse производит верифицированный C-код для разбора бинарных форматов; в Windows Hyper-V им проверяется каждый сетевой пакет, проходящий через облако Azure
  • F*, активная тема исследований формальных методов и безопасности: десятки статей на PLDI, POPL, ICFP, CCS, USENIX Security по верификации TLS 1.3, QUIC, протокола Signal и стандарта ACME

Почему это важно

F* позволяет математически доказать корректность и безопасность программы ещё до того, как её код попадёт в продакшен, это редкая возможность для языков общего назначения. Для криптографии и разбора сетевых протоколов, где одна ошибка превращается в уязвимость, это не теория: код, доказанный в F*, уже работает внутри Firefox, ядра Linux и облака Azure.

Кому это важно

Исследователям в области языков программирования и формальных методов, инженерам по безопасности, которые пишут криптографические библиотеки или реализации протоколов, системным командам крупных компаний вроде Microsoft и Mozilla, а также open-source проектам, которым нужны формально проверенные компоненты в критичных по безопасности местах.

Как это применить

F* можно поставить готовыми бинарниками для Windows, Linux и macOS, через OPAM, Docker или Nix, либо собрать из исходников. Для изучения есть онлайн-книга «Proof-oriented Programming In F*» с примерами прямо в браузере. Для низкоуровневого кода есть подмножество Low*, компилируемое в C через KaRaMeL, а для верифицированного ассемблера, инструментарий Vale.

Можно ли доверять

Текст, это домашняя страница самого проекта F*, а не независимый разбор, поэтому перечень продакшен-внедрений (Firefox, ядро Linux и другие), самоотчёт разработчиков. Но лежащие в основе результаты (HACL*, EverCrypt, EverParse) опубликованы и рецензированы на профильных конференциях по безопасности, S&P, CCS, USENIX Security, что даёт независимую проверку качества, даже если сама страница не приводит ни цифр, ни версии, ни даты последнего обновления.

Риски и подводные камни

Формальная верификация, нишевая дисциплина: зависимые типы, SMT-решатели и интерактивное доказательство теорем требуют специальной подготовки и заметно поднимают порог входа по сравнению с обычными языками программирования. На сайте нет ни тестов производительности, ни сравнения с другими средствами формальной верификации вроде Coq, Lean или Dafny, ни данных о том, какая доля кода этих продакшен-проектов реально проверена F*, а какая, обычный, неверифицированный код вокруг него.