Малейшая ошибка в криптографическом коде может обрушить целые системы: от Windows до облачных сервисов. Microsoft ищет способ исключить такие ошибки, используя формальную верификацию и искусственный интелнет. Компания опубликовала статью о новом подходе к проверке криптографических алгоритмов в SymCrypt — своей основной библиотеке для Windows и Azure.
Криптографический код лежит в основе современных вычислений, защищая операционные системы, облачные сервисы и протоколы. Малейшая арифметическая ошибка, пропуск проверки границ или неверный переход состояния могут подорвать безопасность всей системы. Тестирования и аудита недостаточно, так как реализации часто оптимизированы, низкоуровневы и специфичны для архитектуры. Формальная верификация устраняет этот пробел, используя машинно-проверяемые доказательства вместо одного лишь тестирования.
Microsoft объявила, что новые криптографические реализации для SymCrypt теперь пишутся на безопасном Rust. Их верификация происходит в фреймворке доказательств Lean с помощью инструментария Aeneas. Rust исключает целые классы ошибок безопасности памяти, а доказательства Lean устанавливают функциональную корректность кода относительно формальных спецификаций, полученных из стандартов. Для масштабирования процесса и создания проверяемых доказательств используются ИИ-агенты.
Это позволяет верифицировать код по мере его написания, сохраняя при этом производительность и обеспечивая масштабируемость процесса доказательства, который должен успевать за изменениями в кодовой базе. Microsoft открыла GitHub-ветку, которая включает формальные спецификации и доказательства, доступные вместе с реализациями алгоритмов на Rust.
Первый релиз включает полные доказательства для кода ML-KEM и SHA-3 на Rust, которые уже используются в инсайдерских сборках Windows. Microsoft расширяет этот подход на другие алгоритмы, написанные на Rust, и интегрирует их в продакшен-версии для Windows и Linux. В планах — верификация кода для:
- AES-GCM
- FrodoKEM
- ML-DSA
Первым шагом в этом процессе является формализация алгоритма. Источником истины служат публичные стандарты, такие как спецификации NIST или RFC IETF. На их основе создаётся точная спецификация для Lean.
Новый подход Microsoft сочетает гарантии безопасности Rust с математической строгостью формальной верификации, масштабируя процесс за счёт ИИ-агентов. Это не только повышает надёжность криптографических алгоритмов, но и устанавливает новую планку для разработки критического системного кода, особенно в условиях перехода к постквантовой криптографии.