AlphaProof Code от Google DeepMind формально проверил libsignal

Доказательство вместо тестов

Обычно безопасность ПО проверяют тестами и аудитами: так можно сказать, что проблем не найдено, но не что их нет. Формальная верификация математически доказывает, что код не нарушит определённые свойства, но стоит очень дорого. Проверка ядра seL4 в 2009 году потребовала эквивалента двадцати человеко-лет.

В AlphaProof Code эксперты решают, что доказывать, а агенты выполняют работу. Исследователи сформулировали свойства на основе научных работ о Signal. Агенты на модели Gemini 4 Carbon написали около 6,5 млн строк доказательств на языке Lean, верификатор которого автоматически проверяет каждый шаг. Ни один исследователь не написал ни строки доказательства сам.

Главная цель — механизм «ratchet», постоянно обновляющий ключи шифрования. Согласно технической статье, злоумышленник, укравший ключи с телефона, не сможет прочитать прежние сообщения: каждое шифруется ключом, производным от предыдущего, который затем стирается. Переписка снова становится безопасной, когда собеседники обменялись новыми сообщениями, а выдать себя за одного из них нельзя. Для проверки метода исследователи вернули в libsignal две давно исправленные ошибки, и система показала, что эти версии не дают ожидаемых гарантий.

Ограничения

Технический директор Signal Эрен Крет назвал результат «крупным шагом вперёд». При этом Google оговаривает: доказательство охватывает только переписку двух человек, предполагает идеальную работу базовых криптографических блоков, не проверяя их, и относится к тестовой версии под Linux, а не к мобильным приложениям.

По словам авторов, когда доказательства дешевеют, трудным становится вопрос, что именно доказывать.