Шифрование Signal проверил ИИ AlphaProof Code от DeepMind

При чём тут WhatsApp и Messenger?

Протокол Signal открыт, и на нём построена защита WhatsApp, Facebook Messenger и Google Messages. Поэтому результат касается шифрования переписки огромного числа людей. Технический директор Signal Эрен Крет сообщил, что прежняя формальная верификация охватывала небольшие части кода, а подход DeepMind позволяет заметно расширить охват.

Вручную это долго: нужно описать свойства программы, превратить описание в формулы и только потом строить доказательство. Пушмит Кохли из DeepMind заметил, что банки и другие компании смогут говорить: «мы можем доказать эти свойства».

Какие у проверки ограничения?

Анализ был узким и не охватывает всё мобильное приложение Signal. Он также опирался на более ранние работы по формальной верификации, которые провёл Signal Foundation, некоммерческая организация, стоящая за мессенджером. Остаётся неясным, можно ли автоматизировать такую проверку в большом масштабе и по разумной цене.

Сварат Чаудхури из DeepMind признал, что до применения метода ко всему программному обеспечению мира ещё далеко. По его словам, в будущем это, скорее всего, будет совместная работа человека и ИИ, а не мир, где ИИ сам ставит цели и сам пишет доказательства. DeepMind опубликует спецификацию и доказательство по Signal, чтобы помочь другим исследователям. Планирует ли компания коммерческий сервис формальной верификации, неизвестно.