AlphaProof Code и Signal: проверени машинно-кодови доказателства за сигурност и доверени допускания

Какво обхваща този видеоклип

• AI агентите произвеждат кандидат-доказателства; ядрото на Lean проверява дали те установяват одобрената от човека формална претенция.
• Проверената цел е конкретен компилиран команден инструмент на libsignal, с доверена семантика и криптографски договори.
• Доказването на компилирания бинарен файл премахва компилатора Rust от доверената база за посочените свойства на този бинарен файл.
• Изследователите съобщават за две изолирани повторни въвеждания на по-рано отстранени грешки, които нарушават тяхната символична теорема за сигурност.
• Компараторът проверява теоремата и всяка зависима дефиниция спрямо защитена одобрена спецификация; измененията преминават през отделен процес на преглед.

Преведен препис

Преведено от оригиналния английски разказ. Наличните аудио и субтитри се контролират от YouTube.

Кой проверява доказателство за сигурност на AI?

0:00 Одитът за сигурност на AI все още звучи като доверяване на чатбот. Новият резултат на Google за Signal идва с математически доказателства, отделно ядро проверява. В това видео, какво доказа Google? И как спират агент да променя целите? Ето полезния отговор. Моделите пишат кандидат-доказателства, а Lean проверява доказателствата спрямо одобрена от човека претенция за избран компилиран код. Хората все още притежават претенцията и допусканията.

0:21 Можете да проверите резултата, без да вярвате на победната реч на модела. Отделна проверка улавя тихото променяне на въпроса. Ще го проследим до дефинициите. Вторник, десети ноември е, и това е The Daily Diff. AlphaProof Code е рамката на Google за писане на софтуерни спецификации с човешко ръководство и генериране на проверени доказателства с AI агенти. Това проучване цели 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 Не съм преизградил огромния артефакт за този епизод. Ние докладваме публикувания резултат и неговите граници. Външни лица имат път да го инспектират, което е по-важно за мен от още един AI кръг на победа. Сега капанът.

Може ли коректно доказателство да отговори на грешен въпрос?

3:36 Lean може да приеме коректно доказателство на твърдение, което почти нищо не изисква. Невъзможни допускания могат да направят една теорема безсмислена. Променянето на дефиниция, скрита под основната теорема, може да отслаби целта. Документът проектира проверки срещу това. Пазителят поддържа скрита одобрена спецификация, в която агентите за доказване не могат да пишат. Те могат да предлагат корекции чрез отделен процес на изменение. Отслабването на сигурността се ескалира като потенциална грешка. Декларацията за успех на доказващия няма власт тук.

4:00 Хората отсъждат промени в доверени допускания, директно или чрез тяхната политика, и преглеждат измененията след всяка кампания. Експертната преценка остава отговорна. Агентът може да поиска друго назначение. Не може да си даде преминаваща оценка.

Какво улавя променящите се цели?

4:13 Ето обещаната проверка. Компараторът на Lean сравнява теоремата и всяка дефиниция, от която зависи, с това защитено одобрено копие. Той също така проверява разрешените аксиоми и преиграва доказателството в свежо ядро. Тихото отслабване на помощна дефиниция следователно променя това, което се сравнява. Приетото доказателство трябва да установи одобрената цел. Това все още оставя хората отговорни за избора на силна цел и честни допускания. За вашия собствен работен процес на AI, дръжте критериите за приемане извън

4:37 разрешенията за редактиране на работника и преглеждайте предложените промени отделно. Резултатът на Google прави това разделение конкретно. Авторът на доказателството върши работата; границата на проверката решава дали тя се брои. Ако предпочитате да прочетете това, отколкото да ме чуете да го казвам, разликата пристига във вашата входяща кутия всяка сутрин, безплатно на thedailydiff.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