ИИ помог проверить код, шифрующий переписку Signal
Signal — мессенджер с шифрованием переписки. По сообщению Google DeepMind, исследователи с помощью ИИ доказали конкретные свойства безопасности кода, который за это шифрование отвечает. Среди них — защита прошлых сообщений при последующей утечке ключей, в рамках заданных условий.
Речь о формальной проверке конкретной сборки библиотеки libsignal на уровне скомпилированного кода. Обычные тесты проверяют поведение на выбранных примерах. Здесь устанавливают, что заявленное свойство следует из кода при оговорённых условиях.
Система называется AlphaProof Code. Люди вместе с ИИ формулируют требования и допущения, затем утверждают постановку. Агенты строят доказательства, а их корректность проверяет ядро Lean — системы для записи и машинной проверки математических доказательств.
В работе получилось около 6,5 миллиона строк доказательств. Для меня интересен именно способ их проверки: человеку не нужно вручную перечитывать каждую строку и решать, убедительно ли рассуждает агент. Логические ошибки в доказательстве должен отклонить проверяющий механизм.
Но остаётся вопрос к самим требованиям. Условный пример: доказываем защиту данных, заранее предположив, что доступ есть только у доверенного пользователя. Такое доказательство не ответит, правильно ли система определяет, кому можно доверять. Важное ограничение можно случайно спрятать в условиях.
В исследовании тоже есть существенные допущения. Базовые криптографические операции заданы контрактами: их свойства принимаются как условия, а реализация самих операций здесь не доказывается. Результат не распространяется на всё приложение Signal и не означает неуязвимость переписки. Возможность автоматически проверить любую программу из него тоже не следует.
Поэтому при оценке такой работы я бы сначала смотрел, какое утверждение доказано и что пришлось принять без доказательства. Миллионы проверенных строк дают ответ на поставленный вопрос. Насколько полно этот вопрос описывает нужную защиту, всё ещё требует отдельной оценки.
