Моделі та платформи ШІ
Google DeepMind використовує агентів ШІ для верифікації основного машинного коду Signal
Додайте Unite.AI до бажаних джерел у Google
Google DeepMind представила AlphaProof Code 10 листопада 2026 року: команди агентів ШІ створили формальні доведення в Lean, які перевіряються машиною, для визначених властивостей безпеки скомпільованого коду libsignal у Signal. Команда з п’яти дослідників завершила роботу над доведеннями за чотири тижні й оприлюднила специфікації та артефакти верифікації для зовнішньої перевірки.
Робота вийшла за межі абстрактної моделі конструкції протоколу Signal і охопила його скомпільовану реалізацію. Дослідники помістили незмінені пакети libsignal v0.105.4 і SPQR v1.6.0 у невелику оболонку командного рядка, а потім за допомогою стандартного компілятора rustc зібрали статично скомпонований виконуваний файл для Linux на AArch64. У технічній статті цей результат названо першими доказами безпеки на рівні протоколу для незміненого коду широко розгорнутої реалізації криптографічного протоколу.
Як AlphaProof Code розподілив роботу
П’ятеро дослідників протягом чотирьох тижнів працювали над доведеннями, безперервно запускаючи агентів на своїх робочих станціях і паралельно створюючи символічні та обчислювальні доведення. У статті зазначено, що агенти згенерували близько 6,5 мільйона рядків машинно перевірюваного коду доведень Lean, основу якого становили приблизно 26 000 рядків довірених специфікацій і семантики AArch64.
Люди визначали властивості, розв’язували неоднозначності й питання компромісів у сфері безпеки, перевіряли специфікації та зберігали за собою остаточне схвалення. Агенти на базі Gemini 4 Carbon і Claude Opus 5.5 створювали чернетки специфікацій і перевіряли їх, зокрема за допомогою моделі з іншого сімейства. Потім команди агентів Gemini 4 Carbon згенерували весь код доведень; жоден з авторів не писав його самостійно. Типові цикли роботи тривали від 24 до 72 годин і залучали від 40 до 80 агентів на одній машині. Оркестратор і керівники команд координували агентів, що створювали доведення, а архітектори й інтегратори підтримували спільну базу доведень.
Контролер приймав доведення лише після того, як його перевіряло ядро Lean, а компаратор підтверджував його відповідність окремо збереженій специфікації, схваленій людьми, включно з усіма транзитивними визначеннями; при цьому використовувалися лише стандартні аксіоми Lean. Агенти могли пропонувати невеликі зміни, якщо доведення виявляли проблеми у специфікаціях, але зміни до довірених припущень потребували схвалення людини або політики, встановленої користувачем, і реєструвалися з обґрунтуваннями. Цей механізм усуває задокументований ризик, пов’язаний зі створеними агентами доведеннями: специфікацію можна послабити опосередковано через одне з її визначень.
Охоплення безпеки та перевірка на історичних помилках
Верифікований код охоплював сеанси один-на-один, зокрема рукостискання PQXDH і обмін повідомленнями за протоколом Triple Ratchet. Дослідники повідомляють про два незалежні аргументи: десять символічних теорем за ідеалізованих криптографічних припущень і обчислювальне доведення, яке обмежує перевагу зловмисника за допомогою криптографічних припущень і статистичних величин. Серед доведених властивостей — пряма секретність, що захищає попередні повідомлення в разі викрадення поточного стану; автентифікація; безпека після компрометації, яка стосується відновлення після зламу; і секретність рукостискання. Символічний аргумент також охоплює секретність рукостискання після майбутнього зламу алгоритму Діффі—Геллмана.
Щоб перевірити, чи здатні ці специфікації виявляти реальні помилки, команда скасувала виправлення двох раніше усунутих помилок libsignal, відомих як «слабкий стан» і «мала підгрупа», та повторно скомпілювала змінені бінарні файли. В обох випадках команда створила доведення Lean, що символічна теорема безпеки не виконується. У публічному репозиторії для верифікації окремо зібрано обчислювальні, символічні матеріали, спільний бінарний файл і матеріали із семантики AArch64; там також описано, як повторно зібрати й незалежно перевірити доведення.
Технічний директор Signal Ерен Крет зазначив, що ця робота «дає нам ще більшу впевненість у гарантіях конфіденційності нашого коду».
Обмеження та подальші кроки
Ці гарантії аж ніяк не є сертифікацією всіх застосунків Signal. Вони стосуються збірки libsignal-cli, створеної дослідниками й запущеної як новий процес; генерацію ключів не верифікували, групові повідомлення залишили для подальшої роботи, а побічні канали й стан на кількох пристроях не входять до розглянутого сценарію. Низькорівневі криптографічні примітиви, а також окремі процедури виведення даних і бібліотечні процедури представлені довіреними контрактами. Тому результат також залежить від цих контрактів, схвалених специфікацій, ядра Lean, семантики AArch64 і припущень щодо примітивів.
У статті зазначено, що жоден із двох аргументів не доводить постквантового відновлення, яке має забезпечити SPQR: обчислювальна теорема охоплює класичних зловмисників, тоді як у символічних теоремах про рачет зловмисник може вибирати ключі SPQR. Обчислювальна модель також обмежує низку дій зловмисника й за достатньо великої кількості повідомлень і сеансів зводиться до тривіального твердження. Ці межі визначають, які складові зовнішній рецензент має вважати надійними, перш ніж трактувати машинно перевірені доведення як гарантію безпеки для конкретного розгортання.
Заявлені дослідниками подальші кроки — посилити теореми, зменшити довірену базу, верифікувавши більше підключених процедур і пов’язавши криптографічні контракти з верифікованими реалізаціями, а також розширити охоплення на групові повідомлення, запечатаного відправника й серверні протоколи. Їхня мета — верифікувати нові випуски libsignal до їхнього виходу — є дослідницьким завданням, а не оголошенням про впровадження.
Безпосереднє значення цього результату полягає в продемонстрованому розподілі праці: агенти займалися побудовою доведень, тоді як гарантія надійності й далі спирається на специфікації, перевірені людьми, та чітко сформульовані припущення. Опублікування доведень і процедур перевірки дає зовнішнім рецензентам змогу перевірити цю основу, поки дослідники працюють над тим, щоб інтегрувати цей робочий процес у подальшу розробку libsignal.
