AlphaProof Code від Google DeepMind математично верифікував криптографічне ядро Signal за чотири тижні

Google DeepMind представила AlphaProof Code — систему штучного інтелекту, яка математично доводить, що програмне забезпечення відповідає своїм специфікаціям безпеки без помилок. Дослідники продемонстрували її на протоколі шифрування Signal, виконавши за чотири тижні роботу, яка зазвичай триває роками. Система перевірила фактичний код криптографічного ядра, що працює на пристроях користувачів, а не лише теоретичний дизайн.

Як працювала перевірка

Після того, як експерти визначили формальні вимоги до безпеки, AI-агенти на базі Gemini Carbon написали понад шість мільйонів рядків мовою доведення Lean. Вони позначили приблизно один відсоток кодової бази для перевірки людиною. Два навмисно посіяні для тестування баги виявили негайно. AI-агенти в AlphaProof Code також допомагають створювати специфікації, а потім незалежно доводять, що програмний код відповідає їм.

Ширші наслідки

Попередні зусилля з перевірки зупинялися на етапі теоретичного проєктування, за словами з блог-посту дослідників DeepMind Pushmeet Kohli та Swarat Chaudhuri. Головний технічний директор Signal Ehren Kret сказав, що цей підхід посилює довіру до приватності даних у міру зростання загроз штучного інтелекту. DeepMind планує розширити метод на електромережі та медичні пристрої за допомогою систем на кшталт CodeMender.

Джерела: The Decoder