Amazon внедрила формально верифицированный AES-XTS: первый AES-алгоритм с математическим доказательством корректности

Компания Amazon впервые в мире внедрила в библиотеку s2n-bignum формально верифицированную реализацию алгоритма AES-XTS. Это означает, что код шифрования математически доказан как соответствующий спецификации, что исключает целые классы уязвимостей, связанных с ошибками реализации. Разработка велась командой AWS под руководством старшего учёного Грэма Стила, и результаты уже используются в ключевых продуктах Amazon, включая AWS Key Management Service (KMS) и TLS-библиотеку s2n-tls. Для пользователей облачных сервисов это шаг к абсолютной уверенности в защите данных в покое.

Формальная верификация AES-XTS: как это работает

Формальная верификация — это процесс математического доказательства того, что программа ведёт себя в точности как описано в спецификации. В случае AES-XTS, алгоритм шифрования дисков (XTS) используется для защиты данных в покое, например, в облачных хранилищах Amazon S3 и EBS. Ошибки в реализации AES-XTS могут привести к утечке данных или нарушению их целостности. Команда Amazon Science, возглавляемая старшим учёным Грэмом Стилом (Graham Steel), модифицировала ассемблерный код для основных операций AES-XTS, упростив его и сделав более ясным. Это позволило применить автоматизированные инструменты верификации, которые доказали корректность каждой инструкции.

Ключевым нововведением стало переписывание ядра AES — операции SubBytes, ShiftRows, MixColumns и AddRoundKey — на более чистый ассемблерный код, который легче поддаётся формальному анализу. Верификация проводилась с помощью инструмента HOL Light (доказательство теорем) и s2n-bignum's собственных фреймворков. В результате удалось не только доказать корректность, но и сохранить производительность на уровне существующих оптимизированных реализаций. Это особенно важно, так как AES-XTS критичен для производительности хранилищ: он используется для каждого блока данных при чтении и записи.

Предыстория и контекст: почему это важно

Библиотека s2n-bignum (safe-to-NOT-use) изначально создавалась для реализации криптографии на ассемблере с акцентом на безопасность и верификацию. Она включает формально верифицированные реализации больших чисел (bignum), используемых в RSA и ECC. Однако до сих пор в ней не было ни одного симметричного шифра, такого как AES. Причина — сложность формальной верификации для алгоритмов с нелинейными операциями, как SubBytes (S-блоки). Ранее верификация AES была возможна только на уровне C-кода или с использованием менее строгих методов, таких как тестирование и аудит. Интеграция AES-XTS в s2n-bignum закрывает этот пробел: теперь математически доказано, что реализация не содержит ошибок, связанных с неправильным использованием инструкций или некорректной обработкой ключей.

Этот результат вписывается в более широкий тренд — движение к "формально верифицированному софту" в критически важных системах. Например, Google использует формальную верификацию для своей криптобиблиотеки BoringSSL (часть Chrome), а Amazon — для s2n-tls. Однако AWS пошла дальше, верифицируя не только протокол, но и базовые криптографические примитивы на уровне ассемблера. Это особенно актуально в контексте атак на цепочку поставок (supply chain attacks), когда вредоносный код может быть внедрён на этапе компиляции. Ассемблерная реализация, прошедшая формальную верификацию, не может содержать скрытых уязвимостей или бэкдоров.

Чем эта реализация отличается от других AES-XTS?

Основное отличие — математическое доказательство корректности. Большинство существующих реализаций AES-XTS (например, в OpenSSL, Linux kernel) проходят только функциональное тестирование и аудит кода. Это оставляет вероятность ошибок, которые могут быть не обнаружены даже при тщательном тестировании. Верифицированная реализация Amazon гарантирует, что для любого входа (ключа, открытого текста) выход строго соответствует спецификации IEEE 1619 (стандарт XTS). Дополнительно, код оптимизирован для современных процессоров x86-64 с поддержкой AES-NI (инструкции аппаратного ускорения AES). Верификация показала, что использование этих инструкций корректно, что важно, так как ошибки при работе с AES-NI могут привести к утечке ключей через побочные каналы.

Технические подробности: как упрощение кода помогло верификации

Ключевая инновация команды — не в создании нового алгоритма, а в рефакторинге ассемблерного кода для облегчения формального доказательства. Исходная реализация AES-XTS в s2n-bignum была написана с акцентом на производительность, что привело к запутанному коду с переплетением циклов и неочевидными оптимизациями. Стил и его коллеги переписали ядро AES, разделив операции на более мелкие, логически завершённые блоки. Например, операция SubBytes (замена байтов через S-блок) была выделена в отдельную процедуру с явными таблицами замен. Это позволило применить автоматическую верификацию с помощью HOL Light, который проверил, что каждый байт заменяется строго по таблице AES.

Дополнительным результатом стало то, что верификация автоматически выявила несколько потенциальных проблем в исходной реализации, которые не были обнаружены при стандартном тестировании. Например, некорректная обработка частичных блоков (когда размер данных не кратен 16 байтам) могла привести к утечке данных в зашифрованном виде. Исправленная версия теперь корректно обрабатывает все граничные случаи.

Кого затронет и как

Нововведение в первую очередь затрагивает разработчиков и инженеров, работающих с криптографией в AWS. Библиотека s2n-bignum уже используется в AWS KMS, Amazon S3, EBS и других сервисах, где требуется высокопроизводительное шифрование дисков. Для пользователей это означает повышенную гарантию, что их данные в покое защищены от ошибок реализации. Также это важно для аудиторов и регуляторов: формальная верификация может служить доказательством соответствия стандартам безопасности, таким как FIPS 140-3.

В более широком контексте, успех верификации AES-XTS открывает путь для включения других симметричных шифров в s2n-bignum, например, AES-GCM (гаммирование с аутентификацией) и ChaCha20-Poly1305. Это может усилить позиции Amazon в области безопасных облачных вычислений и повлиять на индустрию: другие компании могут последовать примеру, внедряя формальную верификацию для критичных криптографических примитивов.

Что будет дальше

Команда Amazon Science планирует продолжить верификацию других криптографических алгоритмов, включая AES-GCM и SHA-3. Кроме того, они работают над инструментами, которые автоматизируют процесс верификации для ассемблерного кода, чтобы снизить порог входа. В ближайшее время ожидается публикация полного формального доказательства в открытом доступе, что позволит сообществу проверить результаты. Также возможно, что верифицированная реализация AES-XTS будет включена в upstream-версии Linux kernel или OpenSSL, что сделает её доступной для всех.

Итог

Интеграция формально верифицированного AES-XTS в s2n-bignum — значительный шаг вперёд для безопасности облачных вычислений. Математическое доказательство корректности кода устраняет риск ошибок реализации, которые могут быть использованы злоумышленниками. Для пользователей AWS это означает дополнительный уровень доверия к защите данных в покое. Следите за развитием темы: вероятно, в ближайшие годы формальная верификация станет стандартом для критически важного криптографического кода.