Google DeepMind объявила о результате формальной верификации криптографической реализации Signal, используемой в рабочей среде, утверждая, что ИИ теперь способен закрыть опасный разрыв между проектированием протокола и машинным кодом, который фактически выполняется на устройствах. Компания заявляет, что AlphaProof Code, использующий агентов на базе Gemini Carbon под контролем людей, за четыре недели доказал выбранные свойства безопасности основного кода — процесс, который, по её словам, исторически занял бы у экспертных команд годы.¹

Сроки имеют значение, поскольку криптографические протоколы защищают всё — от личных сообщений до банковских транзакций, — а уязвимости часто возникают на этапе реализации, а не в абстрактном проекте. В своём заявлении DeepMind сообщила, что агенты сгенерировали более шести миллионов строк кода доказательств Lean, тогда как эксперты-люди ставили цели и проверяли результаты. Компания также вновь внесла две старые, уже исправленные ошибки Signal; система корректно показала, что обе изменённые версии небезопасны.¹

Signal приветствовал результат как нечто большее, чем лабораторный эксперимент. Технический директор Эрен Крет заявил, что этот подход обеспечивает «значительное расширение» по сравнению с прежними, более узкими усилиями по верификации и даёт организации «ещё большую уверенность» в гарантиях конфиденциальности Signal.² Генеральный директор DeepMind Демис Хассабис подчеркнул важность достижения в X, назвав его доказательством ключевых свойств безопасности машинного кода, лежащего в основе протокола обмена сообщениями Signal.Demis Hassabis (demishassabis)³

Генеральный директор Google Сундар Пичаи подчеркнул, что работа верифицировала протокол вплоть до скомпилированного кода устройств — уровня, на котором теоретические гарантии в противном случае могут не выдержать столкновения с реальным ПО.Sundar Pichai (sundarpichai)⁴

Однако этот прорыв не означает, что Signal или ПО в целом неуязвимы. В материалах о проекте отмечается, что DeepMind не проводила формальную верификацию всего мобильного приложения Signal и что главный вопрос заключается в том, можно ли распространить верификацию с помощью ИИ на огромные кодовые базы при приемлемых затратах. Научный сотрудник Сварат Чаудхури прямо сформулировал это ограничение: «нам предстоит пройти долгий путь, прежде чем мы сможем масштабировать это на всё программное обеспечение мира».²

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