Аудит за недели: DeepMind верифицировала криптографию Signal через Lean
Исследователи Google DeepMind задействовали ИИ-агентов на базе Gemini, чтобы сгенерировать более шести миллионов строк на языке Lean для математического доказательства ключевых свойств безопасности кода протокола Signal. Криптографические механизмы Signal защищают миллиарды диалогов в таких продуктах, как Google Messages и сам Signal. Проект решил давнюю проблему индустрии: математическое подтверждение надежности скомпилированного кода на уровне промышленной эксплуатации.
Формальная верификация дает математическое доказательство того, что программное обеспечение работает корректно и без сбоев. Если исторически проверка протоколов останавливалась на этапе архитектурного проектирования, то реальные уязвимости часто возникают из-за разрыва между архитектурным планом и реализацией. Как зафиксировала исследовательская группа DeepMind, устранение этой бреши делает доказательства несоизмеримо сложнее, однако автоматизированная среда сузила объем обязательного человеческого контроля до незначительной доли.
«Наш процесс верификации занял всего четыре недели — задача, которая исторически требует от команд экспертов многих лет работы, — доказав, что базовый криптографический код Signal обеспечивает механизмы защиты, заданные нашими специалистами».
Автоматизация генерации корректных теорем на Lean меняет экономику аудита криптографических систем. Вместо финансирования многолетних экспертных проверок организации могут сосредоточить человеческий надзор исключительно на тех участках, где требуется профессиональное суждение. При оценке внедрения в корпоративном секторе совокупные затраты будут сильно зависеть от лицензионных условий, вычислительных накладных расходов на инференс базовых моделей и привлечения узкопрофильных специалистов для написания исходных формальных спецификаций — до того, как в ближайшие три-пять лет начнется широкое коммерческое развертывание в производственных средах за пределами эталонных тестов протоколов.
Границы контроля со стороны человека
Как система распределила трудозатраты между автономными агентами и профильными специалистами?
В архитектуре реализовано разделение обязанностей: эксперты совместно с моделями формировали формальные параметры, а автоматизированные системы генерировали и проверяли доказательства. Исследователи привлекали набор моделей для перевода требований безопасности Signal в формальные математические спецификации, при этом эксперты вручную рецензировали каждую спецификацию. Опираясь на эту базу, AlphaProof Code проводил аудит сгенерированных доказательств и отмечал зоны, требующие повторной проверки человеком, что составило ровно один процент от всей кодовой базы.
Исследование, авторами которого выступили Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton и Pushmeet Kohli, применило это разделение напрямую к реальным реализациям программного обеспечения. Доказательство того, что рабочий код строго соответствует криптографическому проекту, традиционно требовало ручной формализации. Полученные артефакты математически подтвердили, что сообщения остаются защищенными до и после временной компрометации устройства.
Защита реализации и границы рынка
Чтобы проверить, способны ли мультиагентные системы надежно выявлять уязвимости в исполняемом коде, а не просто подтверждать абстрактные спецификации, исследователи повторно внедрили две реальные, ранее устраненные ошибки в изолированную сборку Signal. В обоих сценариях AlphaProof Code выдал машинное доказательство того, что модифицированная версия кода небезопасна.
«AlphaProof Code — это новая агентная платформа для формальной верификации на беспрецедентную глубину, объединяющая человеческую экспертизу с ИИ-агентами».
Google DeepMind заявила, что верификация базовой криптографии Signal закладывает основу для защиты критической инфраструктуры, включая прошивки медицинского оборудования и программное обеспечение энергосетей. Компания выложила артефакты формальной верификации в открытый доступ. Связка формальной верификации с защитными ИИ-агентами вроде CodeMender позиционируется как инструмент противодействия киберугрозам на базе автономных систем.
Публикация артефактов в опенсорс позволяет предприятиям сократить расходы на ручной аудит. Тем не менее базовая математика по-прежнему требует дорогостоящих профильных исследователей: именно они составляют первичные спецификации и вручную проверяют критические граничные сценарии.
В чём смысл
Ровно один процент кода, потребовавший ручной ревизии экспертами, переводит математическое доказательство безопасности из академической экзотики в прикладной производственный контур. Согласно Google DeepMind, проект занял всего четыре недели вместо обычных для таких криптографических задач многолетних трудозатрат целых команд специалистов. По сути, автономные агенты берут на себя рутинную математическую выкладку доказательств, пока человек удерживает контроль над исходными спецификациями. Машинная генерация доказательств превращает аудит критического софта из бесконечной ручной стройки в контролируемый надзор за моделью.
Источник: Google DeepMind Blog