AlphaProof Code та Signal: перевірені докази безпеки машинного коду та довірені припущення

Що охоплює це відео

• Агенти ШІ створюють кандидати доказів; ядро Lean перевіряє, чи вони встановлюють формальне твердження, схвалене людиною.
• Перевірена ціль — це певний скомпільований інтерфейс командного рядка libsignal з довіреною семантикою та криптографічними контрактами.
• Доведення скомпільованого бінарного файлу виключає компілятор Rust з довіреної бази для заявлених властивостей цього бінарного файлу.
• Дослідники повідомляють про дві ізольовані повторні появи раніше виправлених помилок, які порушують їхню символічну теорему безпеки.
• Компаратор перевіряє теорему та кожне залежне визначення на відповідність захищеній затвердженій специфікації; зміни проходять окремий процес перегляду.

Перекладена стенограма

Перекладено з оригінальної англійської розповіді. Доступне аудіо та субтитри контролюються YouTube.

Хто перевіряє доказ безпеки ШІ?

0:00 Аудит безпеки ШІ все ще схожий на довіру чат-боту. Новий результат Google щодо Signal поставляється з математичними доказами, які окреме ядро перевіряє. У цьому відео, що довів Google? І як вони не дають агенту пересувати цілі? Ось корисна відповідь. Моделі пишуть кандидати доказів, а Lean перевіряє докази на відповідність схваленій людиною вимозі щодо вибраного скомпільованого коду. Люди все ще володіють вимогою та припущеннями.

0:21 Ви можете перевірити результат, не вірячи переможній промові моделі. Окрема перевірка виявляє тиху зміну питання. Ми прослідкуємо це до визначень. Вівторок, десяте листопада, і це The Daily Diff. AlphaProof Code — це фреймворк Google для написання специфікацій програмного забезпечення з керівництвом людини та генерування перевірених доказів за допомогою агентів ШІ. Це дослідження націлене на libsignal, бібліотеку Rust, що реалізує протокол обміну повідомленнями Signal, всередині конкретної програми командного рядка.

0:45 Google оголосив про цю роботу сьогодні. У його статті сказано, що п'ять дослідників працювали протягом чотирьох тижнів. Агенти писали докази, тоді як люди витратили більшу частину своїх зусиль на специфікації. Вимоги знайшли спосіб стати ще дорожчими зустрічами. Специфікація говорить, що програма повинна робити,

Як претензія стає ціллю доказу?

0:59 що контролює зловмисник, і які припущення потрібні аргументу. Рецензенти запитують, чи вона охоплює безпеку, яка важлива для людей. Чудово перевірена відповідь на слабке питання залишає це питання недоторканим. Команда ґрунтується на попередніх дослідженнях рукостискання Signal та його ключа повідомлень ratchet. Формальні аналізи вже вивчали ці конструкції. Заява Google пов'язує їхні аргументи безпеки з немодифікованою виробничою скомпільованою реалізацією бібліотеки, де дизайн повинен витримати контакт з фактичним кодом. Технічний директор Signal, Ерен Крет,

1:27 описує розширення за межі менших масштабів попередньої верифікації. Деталі реалізації включають невпорядковані повідомлення та заархівовані сесії для відкладених повідомлень. Справжнє програмне забезпечення зберігає квитанції, які ви викинули зі своєї елегантної схеми. Дослідники компілюють незмінену бібліотеку Rust стандартним

Навіщо доводити скомпільований бінарний файл?

1:41 компілятором в Arm 64 Linux виконуваний файл. Їхні теореми описують цей бінарний файл за допомогою формальної моделі інструкцій, перекидаючись через прогалину між вихідним кодом та оптимізованим машинним кодом. Помилка компілятора, яка порушує заявлену властивість, зробила б її теорему хибною. Тому компілятор залишає довірену базу для цього бінарного файлу. Ви все ще довіряєте моделі інструкцій та перевіряльнику Lean. Межа довіри змістилася, і вона має адресу. Близько шести з половиною мільйонів рядків перевіреного доказу ґрунтуються на приблизно двадцяти шести

2:06 тисячах довірених рядків специфікації та семантики інструкцій. Це кількість артефактів. Розглядати їх як показники інтелекту — це все одно, що ранжувати розробників за розміром їхньої папки з модулями node.

Які властивості безпеки витримали розрив у реалізації?

2:16 Аргументи охоплюють конфіденційність та автентифікацію повідомлень, з прямою секретністю та безпекою після компрометації згідно із заявленими моделями. Ці останні два описують межі шкоди від викраденого ключа та відновлення після свіжих обмінів. Кожна гарантія має умови щодо зловмисника та сесії. Криптографічні примітиви стоять за довіреними контрактами. Доказ припускає, що ці рутини поводяться так, як зазначено, і покладається на криптографічні припущення безпеки. Один доказ ідеалізує криптографію; інший міркує про ймовірності успіху зловмисника.

2:42 Обидва мають обмеження щодо сценаріїв, які вони охоплюють. Запитайте, яка збірка, яка властивість і які припущення. Цей результат стосується інтерфейсу командного рядка дослідників. Групові повідомлення – це майбутня робота, а обчислювальна модель виключає стан кількох пристроїв. Заява про те, що кожна інсталяція Signal без помилок, виходить за рамки теореми. Дослідники повторно ввели дві раніше виправлені помилки Signal у

Чи може специфікація відхилити зламаний код?

3:02 ізольовані копії та скомпілювали їх. Перевірені докази показали, що ці бінарні файли порушували символічну теорему безпеки. Це перевірило, чи може специфікація відхиляти реальні несправні реалізації. Ваш зелений прапорець потребує червоного тесту. Google публікує специфікації та докази з інструкціями з перевірки. У репозиторії зазначено, що чиста збірка займає години та значну кількість пам'яті. Прочитати оголошення на ноутбуці значно легше. Модель апаратного забезпечення та довірені контракти все ще потребують перегляду.

3:26 Я не перекомпілював величезний артефакт для цього епізоду. Ми повідомляємо про опублікований результат та його межі. Сторонні особи мають можливість його перевірити, що для мене важливіше, ніж черговий тріумф ШІ. Тепер пастка.

Чи може правильний доказ відповісти на неправильне питання?

3:36 Lean може прийняти правильний доказ твердження, яке майже нічого не вимагає. Неможливі припущення можуть зробити теорему беззмістовною. Зміна визначення, похованого під заголовком теореми, може послабити ціль. У статті розроблено перевірки проти цього. Сторож зберігає затверджену специфікацію, до якої агенти доказу не можуть записувати. Вони можуть пропонувати виправлення через окремий процес внесення змін. Послаблення безпеки розглядається як потенційна помилка. Декларація успіху доказувача тут не має сили.

4:00 Люди розглядають зміни до довірених припущень, безпосередньо або через свою політику, та переглядають поправки після кожної кампанії. Експертна оцінка залишається відповідальною. Агент може запросити інше завдання. Він не може сам собі поставити прохідну оцінку.

Що ловить рухомі цілі?

4:13 Ось обіцяна перевірка. Компаратор Lean порівнює теорему та кожне визначення, від якого вона залежить, із цією захищеною затвердженою копією. Він також перевіряє дозволені аксіоми та відтворює доказ у новому ядрі. Таким чином, тихе послаблення допоміжного визначення змінює об'єкт порівняння. Прийнятий доказ повинен встановити затверджену ціль. Це все ще залишає людей відповідальними за вибір сильної цілі та чесних припущень. Для власного робочого процесу ШІ тримайте критерії прийняття поза

4:37 правами доступу працівника на редагування та переглядайте запропоновані зміни окремо. Результат Google конкретизує це розділення. Письменник доказів виконує роботу; межа перевірки вирішує, чи це враховується. Якщо ви радше прочитаєте це, ніж почуєте від мене, розбіжність потрапляє до вашої скриньки щоранку, безкоштовно на the daily diff dot dev, посилання нижче. Отже, сьогоднішній вердикт – SHIP IT.

Чи відправив би я цей робочий процес доказу?

4:54 Я б відправив цей робочий процес з перевіреними доказами, тому що затверджена вимога залишається окремою від агента, який надає відповідь. Я б зберігав обсяг та припущення, додані до кожного результату. Підпишіться, натисніть дзвіночок і розкажіть мені в коментарях, чи ви б поставили штамп по-іншому. І це весь розбіжність на сьогодні. Я Ніко з Axrisi. Зливайте відповідально.

Джерела

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub