Apple годами прятала свою криптографию от посторонних глаз. А теперь наконец опубликовала. И вот почему это важно…
NewsMakerИменно так выглядит подготовка к атаке, которой ещё не существует.
Apple решила вынести одну из самых закрытых частей своей защиты на публичную проверку. Компания опубликовала код квантово-устойчивой криптографии и инструменты, с помощью которых проверяла его математическую корректность. Такой шаг должен помочь не только самой Apple, но и другим участникам отрасли, готовящимся к эпохе мощных квантовых компьютеров.
В открытый доступ попали реализации двух алгоритмов, ML-KEM и ML-DSA, а также библиотеки и средства формальной проверки. Apple утверждает, что добилась одного из самых надёжных способов подтверждения корректности для рабочих реализаций таких алгоритмов.
Алгоритмы уже встроены в corecrypto, криптографическую библиотеку Apple, которая работает в операционных системах компании и обслуживает более 2,5 млрд активных устройств. Квантово-устойчивую защиту Apple начала внедрять в iMessage в 2024 году, а затем расширила применение технологии на VPN-сервисы и сетевые протоколы TLS.
Среди опубликованных инструментов есть транслятор Cryptol-to-Isabelle. Он переводит криптографические модели между формальными языками и помогает проверить, соответствует ли код официальным стандартам. Для такой проверки Apple использовала Cryptol, разработанный Galois, и Isabelle, созданный при участии Кембриджского университета и Технического университета Мюнхена.
Формальная проверка уже помогла найти ошибку, которую обычные тесты могли не заметить. В коде ML-DSA специалисты Apple обнаружили пропущенный вычислительный шаг. Такая ошибка могла незаметно нарушать работу цифровых подписей, из-за чего сообщения в iMessage выглядели бы подлинными, хотя защита работала бы неправильно.
Apple признаёт, что одних математических доказательств недостаточно. Часть кода всё равно приходится тестировать обычными методами и проверять в составе всей системы. Компания считает наиболее надёжным смешанный подход, когда формальная проверка подтверждает основные вычисления, а обычное тестирование снижает остальные риски.
ML-KEM и ML-DSA выбрали из числа стандартизированных квантово-устойчивых алгоритмов из-за баланса безопасности, скорости и компактности параметров. Такие алгоритмы должны защитить данные от будущих квантовых компьютеров, которые могут взламывать многие современные схемы шифрования .
Apple решила вынести одну из самых закрытых частей своей защиты на публичную проверку. Компания опубликовала код квантово-устойчивой криптографии и инструменты, с помощью которых проверяла его математическую корректность. Такой шаг должен помочь не только самой Apple, но и другим участникам отрасли, готовящимся к эпохе мощных квантовых компьютеров.
В открытый доступ попали реализации двух алгоритмов, ML-KEM и ML-DSA, а также библиотеки и средства формальной проверки. Apple утверждает, что добилась одного из самых надёжных способов подтверждения корректности для рабочих реализаций таких алгоритмов.
Алгоритмы уже встроены в corecrypto, криптографическую библиотеку Apple, которая работает в операционных системах компании и обслуживает более 2,5 млрд активных устройств. Квантово-устойчивую защиту Apple начала внедрять в iMessage в 2024 году, а затем расширила применение технологии на VPN-сервисы и сетевые протоколы TLS.
Среди опубликованных инструментов есть транслятор Cryptol-to-Isabelle. Он переводит криптографические модели между формальными языками и помогает проверить, соответствует ли код официальным стандартам. Для такой проверки Apple использовала Cryptol, разработанный Galois, и Isabelle, созданный при участии Кембриджского университета и Технического университета Мюнхена.
Формальная проверка уже помогла найти ошибку, которую обычные тесты могли не заметить. В коде ML-DSA специалисты Apple обнаружили пропущенный вычислительный шаг. Такая ошибка могла незаметно нарушать работу цифровых подписей, из-за чего сообщения в iMessage выглядели бы подлинными, хотя защита работала бы неправильно.
Apple признаёт, что одних математических доказательств недостаточно. Часть кода всё равно приходится тестировать обычными методами и проверять в составе всей системы. Компания считает наиболее надёжным смешанный подход, когда формальная проверка подтверждает основные вычисления, а обычное тестирование снижает остальные риски.
ML-KEM и ML-DSA выбрали из числа стандартизированных квантово-устойчивых алгоритмов из-за баланса безопасности, скорости и компактности параметров. Такие алгоритмы должны защитить данные от будущих квантовых компьютеров, которые могут взламывать многие современные схемы шифрования .