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

Што покрива ова видео

• АИ агентите произведуваат предлог-докази; кернелот на Lean проверува дали тие го докажуваат човечки одобреното формално тврдење.
• Проверената цел е одредена компајлирана libsignal CLI апликација, со доверлива семантика и криптографски договори.
• Докажувањето на компајлираната бинарна датотека го отстранува компајлерот 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 и неговиот клуч за пораки рачен затегач. Формални анализи веќе ги проучувале тие дизајни. Тврдењето на 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 може да прифати точен доказ за изјава што бара речиси ништо. Невозможните претпоставки можат да ја направат теоремата безвредна. Менувањето на дефиницијата закопана под главната теорема може да ја ослабне целта. Трудот дизајнира проверки против ова. Чуварот на портата чува одвоена одобрена спецификација во која доказните агенти не можат да пишуваат. Тие можат да предложат корекции преку посебен процес на измена. Слабeењето на безбедноста се ескалира како потенцијална грешка. Изјавата за успех на докажувачот нема авторитет овде.

4:00 Луѓето ги решаваат промените на доверливите претпоставки, директно или преку нивната политика, и ги прегледуваат измените по секоја кампања. Експертската проценка останува одговорна. Агентот може да побара друга задача. Не може да си даде проодна оценка.

Што ги фаќа променливите цели?

4:13 Еве ја ветената проверка. Компараторот на Lean ги споредува теоремата и секоја дефиниција од која зависи со таа заштитена одобрена копија. Исто така, ги проверува дозволените аксиоми и го репродуцира доказот во нов кернел. Тивкото ослабнување на помошната дефиниција затоа го менува она што се споредува. Прифатен доказ мора да ја докаже одобрената цел. Тоа сè уште ги остава луѓето одговорни за изборот на силна цел и чесни претпоставки. За вашиот сопствен работен тек со АИ, чувајте ги критериумите за прифаќање надвор од

4:37 дозволите за уредување на работникот и посебно прегледајте ги предложените промени. Резултатот на Google ја прави таа поделба конкретна. Писателот на докази ја врши работата; границата за проверка одлучува дали таа се брои. Ако повеќе сакате да го прочитате ова отколку да ме слушнете како го кажувам, разликата слетува во вашето сандаче секое утро, бесплатно на the daily diff dot dev, линк подолу. Значи, денешната пресуда е SHIP IT.

Дали би го испорачал овој работен тек за докажување?

4:54 Би го испорачал овој проверен работен тек за докажување бидејќи одобреното тврдење останува одвоено од агентот што го произведува одговорот. Би ги задржал опсегот и претпоставките прикачени на секој резултат. Претплатете се, притиснете го ѕвончето и кажете ми во коментари дали би го печатeл поинаку. И тоа е разликата за денес. Јас сум Нико од 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