Исследователи Google DeepMind показали, что система ИИ способна математически доказать важные свойства безопасности протокола обмена сообщениями Signal. Команда использовала новую систему AlphaProof Code, чтобы формально проверить несколько криптографических гарантий. Работа заняла около четырёх недель и проводилась в рамках исследовательского проекта, а не разработки коммерческого продукта. В проверенных фрагментах новых ошибок не обнаружили, а при анализе прежних версий протокола ИИ правильно выявил известные уязвимости, которые уже были устранены.
Формальная верификация — это проверка с помощью математики того, что программное обеспечение работает именно так, как задумано, без скрытых уязвимостей. Раньше для этого специалистам приходилось составлять подробные спецификации, переводить их в формулы, а затем строить доказательство — трудоёмкая работа, которая могла занимать месяцы. Поручив значительную часть этой работы агентному ИИ — системе, способной самостоятельно ставить подцели и добиваться их выполнения, — DeepMind сократила сроки до нескольких недель. По словам исследователей, на ключевых этапах ИИ всё ещё требовался контроль человека, но система могла самостоятельно предлагать доказательства и исправлять их.
Технический директор Signal Эрен Крет отметил, что предыдущие работы по верификации охватывали лишь небольшие фрагменты кода. По его словам, подход DeepMind позволяет значительно расширить круг проверяемых участков. Команда публикует разработанные спецификацию и доказательство, чтобы другие группы могли продолжить работу. Результаты обнадёживают, однако DeepMind предупреждает: проверка целых приложений или всей цепочки поставок программного обеспечения по-прежнему остаётся сложной задачей. Стоимость такой верификации с помощью ИИ не раскрывается.
Почему это важно
Если ИИ сможет надёжно доказывать безопасность криптографических протоколов, пользователи Signal, Google Messages, WhatsApp и подобных приложений получат больше оснований доверять тому, что их переписка остаётся приватной. Для организаций, зависящих от защищённой связи, — банков, медицинских учреждений и журналистов — эта технология со временем может дать юридически подтверждаемые гарантии того, что в их программном обеспечении нет критических уязвимостей.
Почему это важно
Для обычных пользователей это означает, что шифрование их переписки дополнительно проверили математическими методами, что снижает вероятность скрытых ошибок. Для компаний, которым нужно подтверждать соответствие требованиям законодательства о защите конфиденциальности, верификация с помощью ИИ может стать новым способом демонстрировать безопасность без длительных ручных проверок.
