AlphaProof Code және Signal: тексерілген машина кодының қауіпсіздік дәлелдері және сенімді болжамдар

Бұл бейне не туралы

• Жасанды интеллект агенттері кандидаттық дәлелдерді шығарады; Lean ядросы олардың адам мақұлдаған ресми талапты белгілейтінін тексереді.
• Тексерілген нысан – сенімді семантикасы және криптографиялық келісімшарттары бар компиляцияланған libsignal CLI гарнитурасы.
• Компиляцияланған бинарлық файлды дәлелдеу сол бинарлық файлдың көрсетілген қасиеттері үшін Rust компиляторын сенімді базадан алып тастайды.
• Зерттеушілер бұрын түзетілген екі қатенің оқшауланған түрде қайта енгізілгенін және олардың символдық қауіпсіздік теоремасын бұзғанын хабарлайды.
• Салыстырғыш теореманы және әрбір тәуелді анықтаманы қорғалған бекітілген спецификацияға қарсы тексереді; түзетулер жеке қаралған процесс арқылы өтеді.

Аударылған транскрипция

Бастапқы ағылшын тіліндегі баяндамадан аударылған. Қолжетімді аудио және субтитрлерді YouTube басқарады.

ЖИ қауіпсіздік дәлелін кім тексереді?

0:00 ЖИ қауіпсіздік аудиті әлі де чатботқа сену сияқты естіледі. Google-дің жаңа Signal нәтижесі жеке ядроны математикалық дәлелдермен бірге келеді тексереді. Бұл бейнеде Google нені дәлелдеді? Олар агенттің мақсаттарды өзгертуін қалай тоқтатады? Міне, пайдалы жауап. Модельдер кандидаттық дәлелдерді жазады, және Lean дәлелдерді келесіге қарсы тексереді адам мақұлдаған таңдалған компиляцияланған код туралы талап. Адамдар әлі де талап пен болжамдарға ие.

0:21 Модельдің жеңіс сөзіне сенбей, нәтижені тексере аласыз. Жеке тексеру сұрақты тыныш өзгертуді ұстайды. Біз оны анықтамаларға дейін қараймыз. Бүгін сейсенбі, қарашаның оны, және бұл The Daily Diff. AlphaProof Code - бұл Google-дің бағдарламалық қамтамасыз ету спецификацияларын жазуға арналған негізі адам басшылығымен және ЖИ агенттерімен тексерілген дәлелдерді жасау. Бұл зерттеу Signal-дің хабар алмасуын іске асыратын Rust кітапханасы libsignal-ді нысанаға алады протоколды, белгілі бір командалық жол бағдарламасының ішінде.

0:45 Google бұл жұмысты бүгін жариялады. Оның мақаласында бес зерттеуші төрт апта бойы жұмыс істегені айтылған. Агенттер дәлелдерді жазды, ал адамдар күш-жігерінің көп бөлігін келесіге жұмсады спецификациялар. Талаптар одан да қымбатқа айналудың жолын тапты кездесулер. Спецификация бағдарламаның не істеуі керектігін айтады,

Талап дәлелдеу нысанына қалай айналады?

0:59 шабуылдаушы нені басқарады және дәлелге қандай болжамдар қажет. Шолушылар оның қауіпсіздікке қатысты адамдарды қызықтыратын мәселелерді қамтитындығын сұрайды. Әлсіз сұраққа тамаша тексерілген жауап сол сұрақты сол күйінде қалдырады. Команда Signal-дің қол алысуына және оның хабар кілтіне қатысты бұрынғы зерттеулерге сүйенеді рачет. Ресми талдаулар бұл дизайнды бұрыннан зерттеген. Google-дің талабы олардың қауіпсіздік дәлелдерін өзгертілмеген өндірістік кітапхананың компиляцияланған іске асыруымен байланыстырады, мұнда дизайн келесімен байланысқа төтеп беруі керек нақты код. Signal-дің бас технологиялар директоры Эрен Крет

1:27 бұрынғы верификацияның кішірек ауқымдарынан тыс кеңейтуді сипаттайды. Іске асыру ерекшеліктеріне ретсіз хабарламалар және архивтелген сессиялар кіреді кешіктірілген хабарламалар. Нақты бағдарламалық қамтамасыз ету сіздің әдемі диаграммаңызды тастаған түбіртектерді сақтайды тастап кетті. Зерттеушілер өзгертілмеген Rust кітапханасын стандартты

Компиляцияланған бинарлық файлды неге дәлелдеу керек?

1:41 компилятормен Arm алпыс төрт Linux орындалатын файлға компиляциялайды. Олардың теоремалары сол бинарлық файлды ресми нұсқаулық моделін пайдаланып сипаттайды, бастапқы код пен оңтайландырылған машина коды арасындағы алшақтықты жабады. Көрсетілген қасиетті бұзатын компилятор қатесі оның теоремасын жалған етеді. Сондықтан компилятор бұл бинарлық файл үшін сенімді базаны тастайды. Сіз әлі де нұсқаулық моделіне және Lean тексерушісіне сенесіз. Сенім шекарасы жылжыды, және оның адресі бар. Шамамен алты жарым миллион жол тексерілген дәлел шамамен жиырма алты

2:06 мың сенімді спецификация және нұсқаулық-семантика жолдарына негізделген. Бұл артефакт саны. Оларды интеллект көрсеткіштері ретінде қарастыру, әзірлеушілерді өлшемі бойынша реттеу сияқты олардың түйін модульдері қалтасы.

Іске асырудағы алшақтықтан қандай қауіпсіздік қасиеттері аман қалды?

2:16 Дәлелдер хабарламаның құпиялылығы мен аутентификациясын қамтиды, алға жылжыту құпиялылығымен және көрсетілген модельдер бойынша компромисстен кейінгі қауіпсіздікпен. Соңғы екеуі ұрланған кілттің зақымдалуының шектерін және жаңа айырбастаудан кейінгі қалпына келтіруді сипаттайды. Әрбір кепілдіктің шабуылдаушыға және сессияға қатысты шарттары бар. Криптографиялық примитивтер сенімді келісімшарттардың артында тұр. Дәлел бұл процедуралар көрсетілгендей әрекет етеді деп болжайды және криптографиялық қауіпсіздік болжамдарына сүйенеді. Бір дәлел криптографияны идеалдайды; екіншісі шабуылдаушының сәттілік ықтималдығы туралы ойлайды.

2:42 Екеуінде де олар қамтитын сценарийлерге шектеулер бар. Қай құрастыру, қай қасиет және қай болжамдар екенін сұраңыз. Бұл нәтиже зерттеушілердің командалық жол гарнитурасына қатысты. Топтық хабар алмасу - болашақ жұмыс, және есептеу моделі келесіні қамтымайды көп құрылғылы күй. Әрбір Signal орнатуын қатесіз деп атау теоремадан тыс кетеді. Зерттеушілер бұрын түзетілген екі Signal қатесін оқшауланған көшірмелерге қайта енгізіп, оларды компиляциялады.

Спецификация бұзылған кодты қабылдамауы мүмкін бе?

3:02 Оқшауланған көшірмелерге қайта енгізіп, оларды компиляциялады. Тексерілген дәлелдер сол бинарлық файлдардың символдық қауіпсіздік теоремасын бұзғанын көрсетті. Бұл спецификацияның нақты бұзылған іске асыруларды қабылдамауын тексереді. Сіздің жасыл құсбелгіңізге қызыл тест қажет. Google спецификацияларды және дәлелдерді тексеру нұсқауларымен жариялайды. Репозиторий таза құрастыру бірнеше сағатты және айтарлықтай жадты алатынын айтады. Хабарландыруды оқу ноутбукта айтарлықтай жеңілірек. Аппараттық модель және сенімді келісімшарттар әлі де шолуды қажет етеді.

3:26 Мен бұл эпизод үшін үлкен артефакты қайта құрған жоқпын. Біз жарияланған нәтижені және оның шекараларын хабарлаймыз. Сырттағылар оны тексеруге мүмкіндігі бар, бұл маған тағы бір ЖИ жеңіс айналымынан гөрі маңызды. Енді қақпан.

Дұрыс дәлел қате сұраққа жауап бере ала ма?

3:36 Lean ештеңе сұрамайтын мәлімдеменің дұрыс дәлелін қабылдай алады. Мүмкін емес болжамдар теореманы босқа шығаруы мүмкін. Тақырыптық теореманың астына көмілген анықтаманы өзгерту мақсатты әлсіретуі мүмкін. Мақала бұған қарсы тексерулерді жобалайды. Қақпашы дәлелдеу агенттері жаза алмайтын сақталған бекітілген спецификацияны сақтайды. Олар жеке түзету процесі арқылы түзетулер ұсына алады. Қауіпсіздікті әлсірету ықтимал қате ретінде эскалацияланады. Дәлелдеушінің сәттілік туралы декларациясының бұл жерде ешқандай өкілеттігі жоқ.

4:00 Адамдар сенімді болжамдарға енгізілетін өзгерістерді шешеді, тікелей немесе өз саясаты арқылы, және әрбір науқаннан кейін түзетулерді қарайды. Сарапшылық пікір жауапкершілікте қалады. Агент басқа тапсырманы сұрай алады. Ол өзіне өтетін баға бере алмайды.

Қозғалатын мақсаттарды не ұстайды?

4:13 Міне, уәде етілген тексеру. Lean салыстырғышы теореманы және оған тәуелді әрбір анықтаманы келесімен салыстырады сол қорғалған бекітілген көшірме. Ол сондай-ақ рұқсат етілген аксиомаларды тексереді және дәлелді жаңа ядрода қайта ойнатады. Көмекші анықтаманы тыныш әлсірету салыстырылып жатқан нәрсені өзгертеді. Қабылданған дәлел бекітілген нысанды белгілеуі керек. Бұл әлі де адамдарды күшті нысанды және адал болжамдарды таңдау үшін жауапты етеді. Өзіңіздің ЖИ жұмыс ағыныңыз үшін, қабылдау критерийлерін жұмысшының

4:37 өңдеу рұқсаттарынан тыс ұстаңыз және ұсынылған өзгерістерді бөлек қараңыз. Google-дің нәтижесі бұл бөліністі нақты етеді. Дәлел жазушы жұмыс істейді; тексеру шекарасы оның маңыздылығын шешеді. Егер сіз мұны менің айтқанымды естігеннен гөрі оқығанды жөн көрсеңіз, diff сіздің кіріс жәшігіңізге күн сайын таңертең тегін келеді, daily diff dot dev сайтында, төмендегі сілтеме. Сонымен бүгінгі үкім SHIP IT.

Мен осы дәлелдеу жұмыс ағынын жіберер ме едім?

4:54 Мен бұл тексерілген-дәлелдеу жұмыс ағынын жіберер едім, өйткені бекітілген талап келесі агенттен бөлек қалады жауапты шығаратын агенттен. Мен ауқымды және болжамдарды әрбір нәтижеге қосып ұстайтын едім. Жазылыңыз, қоңырауды басыңыз және егер сіз оны басқаша белгілеген болсаңыз, пікірлерде айтыңыз. Және бүгінге diff осы. Мен 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