DeepMind за месяц проверила часть криптографии Signal с помощью ИИ

У вас проходят тесты, ревью не находит проблем, а уверенности в критическом коде всё равно нет. Для криптографии это особенно неприятно: редкое сочетание условий может оказаться важнее тысячи успешных прогонов. По сообщению ZDNET, Google DeepMind применила AlphaProof Code к части криптографического кода Signal и выполнила проверку за месяц. Практический интерес здесь — в попытке сократить ручную работу по построению математических доказательств.

Сразу обозначим границу результата: из публикации не следует, что исследователи доказали безопасность всего мессенджера. Речь идёт об отдельных частях реализации и свойствах, которые команда решила проверить. Для разработчика это принципиальная разница: доказательство отвечает на конкретный вопрос о программе, а не выдаёт универсальный сертификат надёжности.

Что проверяют математически

Представьте функцию, которая обновляет криптографическое состояние после обработки сообщения. Обычный тест передаёт ей выбранные данные и сравнивает результат с ожидаемым. Можно добавить случайные входы, пограничные значения и длинные последовательности вызовов. Но каждый такой прогон всё равно проверяет конкретный сценарий.

При формальной верификации сначала записывают точное требование к поведению функции. Затем доказывают, что код выполняет его для всех случаев, охваченных заданной моделью. Условный пример: операция должна сохранять определённое соотношение между старым и новым состоянием. Это иллюстрация метода, а не описание конкретного свойства, доказанного командой DeepMind.

Самая дорогая часть такой работы часто начинается ещё до доказательства. Нужно решить, что именно обещает программа, какие предположения допустимы и где заканчивается проверяемый участок. Если требование составлено неверно или неполно, даже корректное доказательство не ответит на реальный вопрос о безопасности продукта.

Как распределили работу между людьми и агентами

По изложению ZDNET, исследователи опирались на предыдущую работу Signal Foundation. Люди вместе с агентами определяли, какие утверждения предстоит доказать. Затем несколько агентов строили доказательства; отдельно система помогала проверять результат и выделяла участки, требующие внимания человека.

Издание сообщает, что для повторной ручной проверки было отмечено около 1% кодовой базы. Эту цифру нужно читать осторожно: из текста неясно, как определялся знаменатель и что именно считалось проверенным участком. Она не означает, что ИИ самостоятельно подтвердил безопасность остальных 99% всего приложения Signal.

Ещё один заявленный результат — работа с двумя ранее исправленными ошибками Signal. Такие проверки полезны: инструмент должен различать корректную реализацию и реализацию с дефектом. Однако краткого пересказа недостаточно, чтобы восстановить эксперимент, понять его условия и оценить, какие классы ошибок система действительно умеет выявлять.

Месячный срок тоже требует контекста. ZDNET сравнивает его с работой, которая могла бы занять у экспертов годы, но не приводит сопоставимого проекта, затрат вычислений и подробного учёта человеческого труда. Поэтому обещать командам такое же ускорение пока рано.

Что делать разработчику и продакту

Если подход подтвердится на доступных материалах, он будет особенно интересен для небольших модулей, где ошибка дорого обходится, а требования можно сформулировать точно. Начать можно с одной функции, описать её допустимые входы, ожидаемые свойства и зависимости. После этого станет понятнее, есть ли здесь задача для формальной проверки и какой результат команда сможет принять.

Продакту полезно заранее определить границы обещания пользователю. Доказанное свойство криптографического модуля ничего автоматически не говорит о защите устройства, интерфейсе, резервных копиях или корректности обновлений. Эти вопросы требуют собственных проверок.

По данным публикации, DeepMind планирует открыть код AlphaProof Code. Для оценки пригодности инструмента понадобятся сам репозиторий, спецификации, проверяемые доказательства и описание ограничений. Пока это содержательный пример применения ИИ к инженерной задаче: агенты могут помогать готовить доказательства, но качество требований и границы результата остаются ответственностью людей.