Microsoft использует AI-агентов для математического доказательства отсутствия ошибок в коде шифрования
Команда, стоящая за криптографической библиотекой Windows и Azure, делает что-то необычное: не просто тестирует код, но доказывает его корректность для каждого возможного входа, используя формальные математические доказательства, частично написанные AI.
Ключевые моменты
- Библиотека SymCrypt корпорации Microsoft, криптографический движок, используемый в Windows и Azure, проходит формальную верификацию с использованием набора инструментов, объединяющих Rust, Lean и Aeneas, начиная с середины 2024 года.
- Первые выпущенные проверенные алгоритмы — SHA-3, стандарт для создания цифровых отпечатков данных, и ML-KEM, пост-квантовая схема шифрования, разработанная для защиты от атак будущих квантовых компьютеров.
- AI-агенты, программное обеспечение, способное самостоятельно выполнять многоэтапные задачи, пишут шаги математических доказательств, которые затем проверяют инженеры-люди.
- Microsoft опубликовала проверенный код, спецификации и доказательства в открытой ветке SymCrypt, сделав работу доступной для независимой проверки.
- Будущие алгоритмы, планируемые для такой же обработки, включают AES-GCM, FrodoKEM и ML-DSA, все из которых сегодня защищают данные в Windows и Linux.
Криптографический код, программное обеспечение, которое шифрует и защищает данные во всех приложениях, браузерах и операционных системах, славится своей неумолимостью. Даже одна пропущенная проверка границ, то есть невозможность подтвердить, что число находится в безопасном диапазоне, может взломать на вид надежную безопасность. Тестирование обнаруживает множество ошибок. Но оно не обнаруживает все ошибки.
Microsoft Research работает над другим подходом: доказать математически, что код правильный, еще до его выпуска.
Проект сосредоточен на SymCrypt, открытой криптографической библиотеке Microsoft, которая работает внутри Windows и Azure Linux. Инженеры теперь пишут новые криптографические алгоритмы на Rust, языке программирования, который по своей конструкции исключает целые семейства ошибок безопасности памяти. Затем они пропускают эти программы Rust через инструмент Aeneas, который переводит код в форму, которую может анализировать помощник доказательств под названием Lean.
Lean — это не чатбот. Это формальный фреймворк доказательства, программное обеспечение, которое проверяет математические аргументы так же, как калькулятор проверяет арифметику, только оно проверяет доказательства, и оно никогда не ошибается.
Цель состоит в том, чтобы создать теорему: для каждого допустимого входа эта реализация возвращает ровно тот результат, который указывает опубликованный стандарт. Не обычно. Всегда.
Первый публичный выпуск охватывает SHA-3, стандартный алгоритм для создания уникального цифрового отпечатка любого фрагмента данных, и ML-KEM, схему обмена ключами пост-квантовой криптографии. Пост-квантовая криптография означает алгоритмы, созданные для сохранения безопасности даже против квантовых компьютеров, машин, которые могут взломать многие современные методы шифрования.
Как AI вписывается в математическое доказательство?
Написание формальных доказательств — медленный процесс. Именно здесь появляются AI-агенты.
Агенты обрабатывают повторяющиеся промежуточные этапы, составляя фрагменты доказательств, которые связывают промежуточные результаты. Инженеры-люди сосредоточены на частях, требующих настоящего суждения: проверка того, что формальная спецификация действительно соответствует опубликованному стандарту, и рассмотрение высокоуровневых свойств, которые должен удовлетворять код. Проверка самого доказательства полностью автоматизирована и детерминирована, что означает, что машина либо принимает доказательство, либо отклоняет его. Нет места для блефа агента.
Microsoft описывает это как чистое разделение: агенты пишут, люди проверяют, проверяющий доказательства решает.
Для людей, использующих Windows, Azure или любой сервис, основанный на стеке безопасности Microsoft, практический смысл ясен. Шифрование, защищающее ваши файлы, облачные данные и учетные данные для входа, соответствует более высокому стандарту, чем может обеспечить одно только тестирование. Если доказательства пройдены, код делает именно то, что требует стандарт.
Открытая ветка позволяет внешним исследователям проверять как код Rust, так и доказательства рядом, поэтому утверждения — это не просто слово Microsoft.
Следите за: объявлениями о достижении формально проверенных сборок в стабильные выпуски Windows и тем, принимают ли другие криптографические библиотеки аналогичные рабочие процессы доказательства с поддержкой AI. Это будет означать реальный сдвиг в том, как индустрия думает о корректности программного обеспечения.
