Исследователи Google DeepMind завершили формальную верификацию безопасности обмена сообщениями Signal. Они утверждают, что это первый случай, когда ИИ помог разработать доказательство, связывающее гарантии безопасности на уровне протокола с широко используемой криптографической реализацией.
Для этого они использовали AlphaProof Code — фреймворк с несколькими агентами для формальной спецификации и верификации программного обеспечения. AlphaProof Code полагается на управляемого человеком агента, который пишет спецификацию на Lean, оценивает семантику машинного кода и создает доказательство, сгенерированное агентом, которое ядро Lean проверяет по спецификации.
В данном случае AlphaProof Code проверил постквантовый рукопожатие PQXDH и Triple Ratchet от Signal, тем самым подтвердив безопасность протокола Signal в отношении прямой секретности, аутентификации, безопасности после компрометации и секретности рукопожатия, реализованных в libsignal.
Таким образом, команда Google/DeepMind — Сварат Чаудхури, Эндрю Ферраиоло, Антон Ковшаров, Тедж Чаджед, Сэм Шлезингер, Карн Сет, Джонатан Кац, Чарльз Саттон и Пушмит Коли — сделала шаг к вызову, брошенному Beneficial AI Foundation в апреле, по формальной верификации протокола Signal и приложения Signal с помощью Lean.
Процесс AlphaProof Code включает работу с различными моделями для преобразования целей безопасности Signal в математическую спецификацию, проверенную человеком. На основе этой спецификации исследователи поручили агентам Gemini Carbon сгенерировать код на Lean, доказывающий корректность реализации libsignal. После того как агенты сгенерировали 6,5 миллионов строк кода на Lean, они провели аудит и отметили фрагменты, требующие проверки человеком.
Результат носит теоретический характер, поскольку он предполагает идеальную криптографию и не гарантирует вычислительную секретность байтов. Но это все равно значимое утверждение о корректности.
«Это система, которая фундаментально построена для сотрудничества человека и ИИ», — сказал Сварат Чаудхури, научный сотрудник Google DeepMind и профессор Техасского университета в Остине, в интервью The Register.
Традиционно, по словам Чаудхури, доказательство теорем начиналось с четко определенных проблем, сформулированных математиком, которые затем передавались агенту ИИ для доказательства. В данном случае исследователям пришлось самим определять, что именно доказывать.
«В формальных методах мы всегда верили, что верификация — это самая сложная часть, — сказал он. — Существует тридцать или сорок лет работы над масштабированием верификации. Теперь мы можем это делать. Так что теперь вопрос в том, что именно мы верифицируем? … Этот процесс фундаментально включает человека, но мы разработали процесс, чтобы масштабировать его в максимально возможной степени с помощью ИИ».
Как отмечают Чаудхури и его коллеги в своей исследовательской работе «AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level», формальная верификация раньше требовала героических усилий. Формальная верификация микроядра seL4 заняла 20 человеко-лет, а разработка верифицированного компилятора C CompCert — шесть лет.
По их мнению, AlphaProof Code может значительно снизить стоимость формальной верификации, хотя работа над Signal все равно заняла четыре недели для команды из пяти человек и «довольно много токенов».
«Мечта — определенно масштабировать это, — сказал Чаудхури. — Вы знаете, произошел всплеск наступательных возможностей ИИ, верно? Во всем мире существует множество небезопасных систем, и они будут эксплуатироваться.
«Поэтому нам действительно нужно применить эту технологию к коду в целом по всему миру и выяснить, от чего именно нужно защищаться? Как писать эти свойства, как мы их специфицируем? Это будет чрезвычайно важно, но нам еще предстоит это выяснить».
Ссылаясь на связанный проект DeepMind, AlphaProof Nexus, который ориентирован на математику, Чаудхури сказал, что следующим шагом будет применение этой технологии в процессе проектирования программного обеспечения — не только к криптографическим протоколам, но и к коду в целом.
«Мы действительно верим, что следующей границей в такого рода исследованиях будет не доказательство, а спецификация, — сказал он. — И именно поэтому мы взялись за эту область, где это действительно была сложная проблема. И я думаю, что у нас есть несколько действительно хороших идей о том, как подойти к этому, хотя и далеко не окончательных».
Всегда имейте в виду, что редакции могут придерживаться предвзятых взглядов в освещении новостей.
Автор – Thomas Claburn
