Google DeepMind с помощью агентного ИИ математически доказала ключевые криптографические гарантии протокола Signal, на котором построены Signal, Google Messages и WhatsApp. Эксперимент занял четыре недели и опирался на новый фреймворк AlphaProof Code. Результат важен потому, что он показывает способность ИИ выполнять формальную верификацию, которая раньше требовала долгой ручной работы.
Проект проверки Signal за четыре недели
Анализ подтвердил изученные свойства и не выявил новых уязвимостей в этих частях протокола. Для контроля исследователи запустили AlphaProof Code на старых версиях Signal с известными и давно исправленными ошибками. Система корректно признала их недоказуемыми, что подтвердило способность метода отличать защищенный код от незащищенного. DeepMind публикует спецификацию и доказательство для поддержки дальнейшей работы по верификации.
Проект строился как совместная работа человека и ИИ, где агенты вносили вклад и исправляли себя почти на каждом этапе, а люди проверяли ключевые точки. Научный сотрудник Swarat Chaudhuri сказал, что команда не хотела, чтобы ИИ сам ставил цели и доказывал тесты собственного сочинения. Поэтому агенты работали в рамках заданных людьми свойств и контрольных точек, а не действовали автономно. Такая схема привязала доказательство к заявленным гарантиям безопасности.
Команда получила преимущество благодаря прошлой работе Signal Foundation по формальной верификации. Ранние усилия охватывали меньшие фрагменты кода, а DeepMind с помощью ИИ расширила охват проверки. Технический директор Signal Ehren Kret сказал, что подход позволяет существенно расширить проверяемый код. Он связал работу с ростом угроз с применением ИИ и укреплением уверенности в гарантиях приватности.
Что ИИ-верификация дает бизнесу
Для компаний, зависящих от обмена сообщениями, платежей и документами, проверенная криптография снижает риск скрытых дефектов в базовом уровне доверия. Банки и другие регулируемые организации смогут ссылаться на доказанные свойства, а не только на покрытие тестами. Крупные организации, вероятно, сначала проверят модули аутентификации, обмена ключами и платежей. Небольшие компании выиграют косвенно, когда массовые протоколы и библиотеки получат более сильные гарантии.
Метод пока ограничен по охвату и стоимости. DeepMind не проверяла все мобильное приложение Signal, а исследователи назвали результат одной вехой в долгой работе. Анализ выполнен бесплатно как исследовательский проект, Google не раскрыла его стоимость и не комментирует планы коммерческого продукта. Поэтому заказчикам стоит спрашивать поставщиков, какой код охвачен, какие свойства доказаны и как люди проверяли результат.
Показателем станет повторение такой проверки на другом массовом протоколе за сопоставимый срок. Вторая публичная работа со спецификацией, доказательством и независимой проверкой покажет переносимость метода за пределы Signal. Без такого повторения проект останется сильной демонстрацией, а не воспроизводимым сервисом.
