Apple внедрила quantum-secure cryptography в iMessage и теперь публикует код. Вместе с релизом corecrypto компания выложила реализации ML-KEM и ML-DSA — двух алгоритмов, стандартизированных NIST как FIPS 203 и FIPS 204. Но главное не сами алгоритмы, а то, как Apple доказала их корректность.
Компания разработала новый метод формальной верификации для corecrypto — фундаментальной криптобиблиотеки, которая работает на 2,5 миллиарда активных устройств. Ошибка в ней может подорвать безопасность всех зависящих приложений, поэтому Apple включила ML-KEM и ML-DSA только после жёсткой проверки по четырём критериям: алгоритм должен улучшать безопасность, иметь надёжную теоретическую основу, быть высокопроизводительным на любом чипе Apple и не перегружать память компактными ключами.
Когда эти условия выполнены, реализацию пишут на портативном C, а критичные участки переписывают вручную на ARM64 ассемблере для максимальной производительности и защиты от side-channel атак. Для верификации Apple использовала связку старых и новых инструментов: Isabelle (уже применяли для верификации чипов), SAW от Galois и язык Cryptol. Специально по заказу Apple Galios сделала переводчик cryptol-to-isabelle, чтобы модели на Cryptol можно было сравнивать со спецификациями в Isabelle.
Итог — более 50 тысяч шагов доказательств. Верификация выявила проблемы, которые обычное тестирование не ловит. Например, пропущенный шаг в ранней версии ML-DSA, который в редких случаях давал некорректный результат, и ошибку в стороннем доказательстве. Такие баги могли тихо ломать криптографию без предупреждения.
Apple не утверждает, что система идеальна — есть ограничения, например, SAW не покрывает все размеры сообщений для ML-DSA, а верификация предполагает корректную работу компилятора. Но компания уверена, что сочетание формальных методов, ручной оптимизации и классического тестирования даёт самую высокую гарантию корректности для production-реализаций ML-KEM и ML-DSA на сегодня.
Код corecrypto с этими доказательствами опубликован 22 мая 2026 года. Apple выложила Isabelle-теории, модели на ARM64, библиотеки лемм и сам переводчик Galois. Всё это можно воспроизвести, проверить и использовать независимо.