Google DeepMind подтвердила безопасность сквозного шифрования Signal с помощью ИИ

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

Исследователи Google DeepMind успешно завершили формальную верификацию безопасности протокола обмена сообщениями Signal, что является первым случаем, когда ИИ помог разработать доказательство, связывающее гарантии безопасности на уровне протокола с широко используемой криптографической реализацией. Этот протокол считается золотым стандартом для сквозного шифрования и применяется не только в приложении Signal, но и в WhatsApp, а также Google Messages.

AlphaProof Code: гибридный подход к верификации

Для достижения этой цели был использован AlphaProof Code - мультиагентный фреймворк, предназначенный для формальной спецификации и верификации программного обеспечения. AlphaProof Code задействует агента, управляемого человеком, который создает спецификацию Lean, оценивает семантику машинного кода и формирует доказательство, проверяемое ядром Lean на соответствие спецификации. В рамках данного проекта AlphaProof Code верифицировал рукопожатие PQXDH и Triple Ratchet протокола Signal, подтвердив таким образом надежность его прямой секретности, аутентификации, безопасности после компрометации и секретности рукопожатия.

Процесс AlphaProof Code включает преобразование целей безопасности Signal в математическую спецификацию, которая затем просматривается человеком. На основе этой спецификации агенты Gemini Carbon генерировали код Lean, доказывающий корректность реализации libsignal. После генерации 6,5 миллионов строк кода Lean агенты проводили аудит, отмечая фрагменты, требующие человеческого вмешательства. Хотя результат является теоретическим и предполагает идеальную криптографию, не гарантируя вычислительную секретность байтов, он является значимым подтверждением корректности.

Сокращение затрат и будущие перспективы

По словам Сварата Чаудхури, научного сотрудника Google DeepMind и профессора Техасского университета в Остине, AlphaProof Code - это система, изначально разработанная для совместной работы человека и ИИ. Традиционно доказательство теорем начиналось с четко определенных проблем, сформулированных математиком и затем передаваемых ИИ для решения. В данном случае исследователям пришлось самим определить, что именно нужно доказывать.

«В формальных методах всегда существовало убеждение, что верификация - это самая сложная часть», - отметил Чаудхури. «Существует тридцать или сорок лет работы по масштабированию верификации. Теперь мы можем это сделать. Так что теперь вопрос в том, что мы верифицируем? … Этот процесс фундаментально предполагает участие человека, но мы разработали процесс, позволяющий масштабировать его максимально возможным образом с помощью ИИ». Как отмечают Чаудхури и его коллеги в своей исследовательской работе «AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level», формальная верификация ранее требовала колоссальных усилий. Например, формальная верификация микроядра seL4 заняла 20 человеко-лет, а разработка верифицированного компилятора CompCert C - шесть лет.

Команда Google/DeepMind, состоящая из Сварата Чаудхури, Эндрю Феррауоло, Антона Ковшарова, Теджа Чаджеда, Сэма Шлезингера, Карна Сета, Джонатана Каца, Чарльза Саттона и Пушмита Коли, считает, что AlphaProof Code может значительно сократить стоимость формальной верификации. Несмотря на то, что работа над Signal заняла четыре недели у команды из пяти человек и потребовала «довольно много токенов», это значительный прогресс. «Мечта, безусловно, состоит в том, чтобы масштабировать это», - сказал Чаудхури, указывая на рост наступательных возможностей ИИ и обилие незащищенных систем в мире. Следующим шагом является применение этой технологии на этапе проектирования программного обеспечения, не только к криптографическим протоколам, но и к коду в целом. В этом контексте новые инициативы в области ИИ, такие как Kora, демонстрируют растущий интерес к интеграции ИИ в фундаментальные аспекты разработки ПО.