АлфаПруф код и сигнал: проверени машинско-кодни безбедносни докази и поуздане претпоставке

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

• АИ агенти производе предложене доказе; Lean-ово језгро проверава да ли они утврђују формалну тврдњу коју су одобрили људи.
• Верификовани циљ је одређени компајлирани libsignal CLI програм, са поузданом семантиком и криптографским уговорима.
• Доказивање компајлираног бинарног кода уклања Rust компајлер из поуздане базе за наведена својства тог бинарног кода.
• Истраживачи извештавају о два изолована поновна уношења претходно исправљених грешака које крше њихову симболичку безбедносну теорему.
• Компаратор проверава теорему и сваку зависну дефиницију у односу на заштићену одобрену спецификацију; измене пролазе кроз посебан прегледани процес.

Преведени транскрипт

Преведено са оригиналне енглеске нарације. Доступни аудио и титлови контролисани су од стране YouTube-а.

Ко проверава доказ АИ безбедности?

0:00 АИ безбедносна ревизија и даље звучи као веровање чет-боту. Гуглов нови Сигнал резултат долази са математичким доказима које посебно језгро проверава. У овом видеу, шта је Гугл доказао? И како спречавају агента да мења циљеве? Ево корисног одговора. Модели пишу предложене доказе, а Lean проверава доказе у односу на тврдњу коју су одобрили људи о одабраном компајлираном коду. Људи и даље поседују тврдњу и претпоставке.

0:21 Можете проверити резултат без веровања у победнички говор модела. Посебна провера хвата тихо мењање питања. Пратићемо то до дефиниција. Уторак је, десети новембар, и ово је The Daily Diff. AlphaProof Code је Гуглов оквир за писање софтверских спецификација са људским вођством и генерисање проверених доказа помоћу АИ агената. Ова студија циља libsignal, Руст библиотеку која имплементира Сигналов протокол за размену порука, унутар одређеног програма командне линије.

0:45 Гугл је данас најавио рад. У његовом раду пише да је пет истраживача радило преко четири недеље. Агенти су писали доказе, док су људи већину свог напора посветили спецификацијама. Захтеви су пронашли начин да постану још скупљи састанци. Спецификација каже шта програм мора да ради,

Како тврдња постаје циљ доказа?

0:59 шта нападач контролише и које претпоставке су потребне за аргумент. Рецензенти питају да ли обухвата безбедност до које је људима стало. Лепо проверен одговор на слабо питање оставља то питање нетакнутим. Тим се ослања на ранија истраживања Сигналовог руковања и његовог кључа за поруке рачета. Формалне анализе су већ проучавале те дизајне. Гуглова тврдња повезује њихове безбедносне аргументе са немодификованом производном компајлираном имплементацијом библиотеке, где дизајн мора да преживи контакт са стварним кодом. Сигналов главни технички директор, Ерен Крет,

1:27 описује проширење изван мањих опсега раније верификације. Детаљи имплементације укључују ванредне поруке и архивиране сесије за одложене поруке. Прави софтвер чува признанице које је ваш елегантни дијаграм бацио далеко. Истраживачи компајлирају немодификовану Руст библиотеку са стандардним

Зашто доказати компајлирани бинарни код?

1:41 компајлером у Арм шездесетчетвороибитни Линукс извршни фајл. Њихове теореме описују тај бинарни код користећи формални модел инструкција, простирући се преко јаза између изворног и оптимизованог машинског кода. Грешка компајлера која нарушава наведено својство учинила би њену теорему лажном. Компајлер стога напушта поуздану базу за овај бинарни код. И даље верујете моделу инструкција и Lean-овом чекеру. Граница поверења се померила и има адресу. Око шест и по милиона редова провереног доказа почива на отприлике двадесет шест

2:06 хиљада поузданих спецификација и редова семантике инструкција. Ово су бројеви артефаката. Третирање њих као оцене интелигенције је као рангирање програмера по величини њиховог фолдера node_modules.

Која су безбедносна својства преживела јаз у имплементацији?

2:16 Аргументи обухватају поверљивост и аутентификацију порука, са прослеђеном тајношћу и сигурношћу након компромитације према наведеним моделима. Ова последња два описују ограничења оштећења украденим кључем и опоравак након свежих размена. Свака гаранција има услове о нападачу и сесији. Криптографски примитиви стоје иза поузданих уговора. Доказ претпоставља да те рутине функционишу како је наведено и ослања се на криптографске безбедносне претпоставке. Један доказ идеализује криптографију; други разматра вероватноће успеха нападача.

2:42 Оба имају ограничења у сценаријима које покривају. Питајте која верзија, које својство и које претпоставке. Овај резултат се односи на командно-линијски програм истраживача. Групно слање порука је будући рад, а рачунски модел искључује статус више уређаја. Називање сваке Сигналове инсталације без грешке излази изван теореме. Истраживачи су поново увели две претходно исправљене Сигналове грешке у

Може ли спецификација одбацити покварени код?

3:02 изоловане копије и компајлирали их. Проверени докази су показали да су ти бинарни кодови кршили симболичку безбедносну теорему. То је тестирало да ли спецификација може одбацити стварне покварене имплементације. Ваша зелена квачица треба црвени тест. Гугл објављује спецификације и доказе са упутствима за проверу. Репозиторијум каже да чиста изградња траје сате и захтева значајну меморију. Читање објаве је знатно лакше на лаптопу. Модел хардвера и поуздани уговори и даље захтевају преглед.

3:26 Нисам поново изградио огроман артефакт за ову епизоду. Извештавамо о објављеном резултату и његовим границама. Спољни субјекти имају пут да то прегледају, што ми је важније од још једне АИ победничке туре. Сада замка.

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

3:36 Lean може прихватити тачан доказ изјаве која не тражи готово ништа. Немогуће претпоставке могу учинити теорему бесмисленом. Мењање дефиниције закопане испод насловне теореме може ослабити циљ. Рад дизајнира провере против овога. Чувар чува одобрену спецификацију коју агенти за доказе не могу да пишу. Они могу предложити исправке кроз посебан процес измене. Безбедносно слабљење се ескалира као потенцијална грешка. Изјава доказивача о успеху овде нема ауторитет.

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

Шта хвата покретне циљеве?

4:13 Ево обећане провере. Lean-ов компаратор упоређује теорему и сваку дефиницију од које она зависи са том заштићеном одобреном копијом. Такође проверава дозвољене аксиоме и понавља доказ у новом језгру. Тихо слабљење помоћне дефиниције стога мења ствар која се упоређује. Прихваћен доказ мора да утврди одобрени циљ. То и даље оставља људе одговорним за избор снажног циља и поштених претпоставки. За ваш сопствени АИ радни ток, држите критеријуме прихватања изван

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

Да ли бих користио овај радни ток доказа?

4:54 Користио бих овај проверени радни ток доказа јер одобрена тврдња остаје одвојена од агента који производи одговор. Задржао бих опсег и претпоставке везане за сваки резултат. Претплатите се, притисните звоно и реците ми у коментарима да ли бисте га другачије оценили. И то је разлика за данас. Ја сам Нико из Аксерисија. Спајајте одговорно.

Извори

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