Google расширил доступ к Gemini 4 Carbon и сообщает, что агенты, построенные на этой модели, помогли формально проверить ключевые гарантии безопасности кода протокола Signal.
Разработчики и компании, которые платят, теперь могут использовать Carbon через API Gemini и Gemini for business, доступ есть и у подписчиков Google AI Ultra. Вводные тарифы в размере $2 и $10 за миллион входных и выходных токенов действуют до 30 ноября, после чего они удвоятся. Токен — это единица текста, которую модель обрабатывает для чтения или генерации контента.
До сих пор использовать Carbon могли только некоторые специалисты по кибербезопасности, участвующие в программе Google Fairwind. Они по-прежнему должны быть участниками этой программы для доступа к Carbon for cyber — версии, которую Google позиционирует как лидера по основным бенчмаркам обнаружения, эксплуатации и исправления уязвимостей.
Применение в кибербезопасности
По словам Google, компания Wiz использовала Carbon for cyber для поиска уязвимостей типа «zero-day» у двух крупных поставщиков SaaS за два часа. Команда Google Cloud Vulnerability Research (CVR), со своей стороны, использовала модель, чтобы подтвердить, что две ошибки в популярном open source проекте являются эксплуатируемыми, с уровнем серьезности, сопоставимым с PHP2Shell — парой уже эксплуатируемых уязвимостей в PHP.
«Используя Carbon для создания концептуального подтверждения, CVR помогла сопровождающим переклассифицировать ошибку как критическую и быстро выпустить патч», — сообщает Google.
Проверка кода Signal
Кроме того, Google DeepMind представила AlphaProof Code, которая сочетает экспертов-людей с агентами ИИ для формальной проверки программного обеспечения, то есть математического доказательства соответствия заданным требованиям. Команда применила её к libsignal — эталонной реализации протокола Signal. Версии этого протокола также работают в WhatsApp и Google Messages.
Люди работали с агентами, запущенными на Carbon и Claude Opus 5.5, чтобы составить спецификации, описывающие, что нужно доказать. Затем агенты на основе Carbon сгенерировали все примерно 6,5 миллионов строк доказательств, написанных на Lean — ассистенте доказательств, который отвергает недействительные. По словам Google, доказанные гарантии, включая постоянную секретность (forward secrecy), безопасность после компрометации и аутентификацию, действительны для скомпилированного машинного кода, в то время как большинство проверок протоколов касаются только проектирования.
Пять исследователей выполнили работу по доказательству за четыре недели — работа, которая, по оценке Google, традиционно занимает годы у специалистов. Чтобы проверить, что метод обнаруживает реальные уязвимости, команда вновь внедрила две старые, уже исправленные ошибки в libsignal и доказала, что эти версии больше не соответствуют гарантиям безопасности.
Результаты относятся к версии кода, скомпилированной Google, выполняемой через небольшой инструмент командной строки, а не к «самим приложениям Signal». Некоторые побочные каналы также были исключены из частей анализа. «Результаты позволяют предположить, что ИИ может сделать формальную проверку, исторически слишком дорогую для большинства программ, применимой для реальных систем», — пишут исследователи. Эрен Крет, технический директор Signal, со своей стороны заявил: «В то время как угрозы безопасности, связанные с ИИ, множатся, тщательная проверка реализации протокола Signal даёт нам ещё большую уверенность в гарантиях конфиденциальности нашего кода». Google также публикует спецификации и доказательства.
